Hanifa Boucheneb
email: hanifa.boucheneb@polymtl.ca

Kamel Barkaoui
email: kamel.barkaoui@cnam.fr

Delay-dependent partial order reduction technique for real time systems

Keywords: Time Petri nets, Partial order techniques, State space abstractions, Contracted state class graph method,

Partial order reduction techniques aim at coping with the state explosion problem by reducing, while preserving the properties of interest, the number of transitions to be fired from each state of the model. For (time) Petri nets, the selection of these transitions is, generally, based on the structure of the (underlying) Petri net and its current marking. This paper proposes a partial order reduction technique for time Petri nets (TPN in short), where the selection procedure takes into account the structure, including the firing intervals, and the current state (i.e., the current marking and the firing delays of the enabled transitions). We show that our technique preserves non-equivalent firing sequences of the TPN. Therefore, its extension to deal with LT L -X properties is straightforward, using the well established methods based on the stuttering equivalent sequences.

delays. Time Petri nets are definitely established as a powerful formalism for formal verification of real time systems. The verification techniques, such as reachability analysis, are based on the so-called state space abstraction, where states reachable by the same firing sequence, but at different dates, are grouped in the same set and considered modulo some relation of equivalence (abstract states, state classes or state zones) [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF][START_REF] Boucheneb | TCTL model checking of time Petri nets[END_REF][START_REF] Boucheneb | CTL* model checking for time Petri nets[END_REF][START_REF] Boucheneb | A more efficient time Petri net state space abstraction useful to model checking timed linear properties[END_REF][START_REF] Yoneda | CTL model checking of time Petri nets using geometric regions[END_REF]. For bounded time Petri nets, state space abstractions, such as the State Class Graph (SCG) [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF] and the Zone Based Graph (ZBG) [START_REF] Boucheneb | TCTL model checking of time Petri nets[END_REF], yield finite representations that preserve marking and firing sequences. However, for highly concurrent systems, these verification techniques face a severe problem of state space explosion.

To alleviate this problem, partial order techniques are proposed in the literature for time Petri nets such as: partial order unfolding [START_REF] Chatain | Complete finite prefixes of symbolic unfoldings of safe time Petri nets[END_REF][START_REF] Delfieu | Parameterized study of a time Petri net[END_REF][START_REF] Semenov | Verification of asynchronous circuits using time Petri net unfolding[END_REF] and partial order reduction [START_REF] Boucheneb | Reducing interleaving semantics redundancy in reachability analysis of time Petri nets[END_REF][START_REF] Boucheneb | Stubborn sets for time Petri nets[END_REF][START_REF] Boucheneb | Delay-dependent partial order reduction technique for time Petri nets[END_REF][START_REF] Godefroid | An approach to the state-explosion problem[END_REF][START_REF] Peled | Stutter invariant temporal properties are expressible without the next-time operator[END_REF][START_REF] Peled | All from one, one for all: on model checking using representatives[END_REF][START_REF] Valmari | Can stubborn set be optimal[END_REF][START_REF] Yoneda | Efficient verification of parallel real-time systems[END_REF]. The idea of the unfolding techniques is to translate a TPN model into an acyclic Petri net with firing time constraints, respecting the partial order of the originate model. The available unfolding techniques are however limited to 1-safe TPNs 1 . The common characteristics of the partial order reduction methods is that they explore a subset of firing sequences (representative firing sequences) from each (abstract) state. These subsets are sufficient to verify the properties of interest.

Among the TPN state space abstractions in the literature, we consider the Contracted State Class Graph (CSCG in short) [START_REF] Boucheneb | A more efficient time Petri net state space abstraction useful to model checking timed linear properties[END_REF] and investigate partial order reduction techniques, which preserve non-equivalent firing sequences of the TPN (i.e., there is no maximal firing sequence2 in the TPN with no equivalent sequence 3 in the reduced space and vice-versa). Since the CSCG preserves markings and firing sequences of the TPN, the purpose is to select a subset of firable transitions to be explored from each state class, so as to cover all and only all non-equivalent firing sequences of the CSCG.

In almost all partial order reduction techniques, the selection procedure of representative transitions is based on an independence relation over transitions. Intuitively, two transitions are independent, if they can neither disable nor enable each other and their firings in both orders lead to the same state. If a transition is selected to be fired from a state, then all its dependent and firable transitions are selected too. Various sufficient conditions, guaranteeing an effective selection of an over-approximation of dependent transitions, are proposed in the literature such as persistent sets [START_REF] Godefroid | An approach to the state-explosion problem[END_REF], ample sets [START_REF] Peled | All from one, one for all: on model checking using representatives[END_REF][START_REF] Peled | Stutter invariant temporal properties are expressible without the next-time operator[END_REF] and stubborn sets [START_REF] Valmari | Can stubborn set be optimal[END_REF].

However, in the context of the TPN state space abstractions such as the CSCG, different interleavings of the same set of transitions lead, in general, to different abstract states and then the relation of independency is difficult to meet. For instance, for the TPN at Fig. 1.a, taken from [START_REF] Boucheneb | Reducing interleaving semantics redundancy in reachability analysis of time Petri nets[END_REF], the firing of the non-conflicting transitions t 1 and t 2 in both orders leads to two state classes with different behaviours (see Fig. 2.a and Table 1). The transition t 3 is not firable from the state class reached by t 2 t 1 but is firable from the successor of the initial state class by t 1 t 2 . To overcome this limitation, two main techniques are used in the literature: the local time semantics [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF][START_REF] Hakansson | Partial order reduction for verification of real-time components[END_REF][START_REF] Minea | Partial order reduction for model checking of timed automata[END_REF] and Partially Ordered Sets (POSETs) of transitions or events [START_REF] Belluomini | Timed state space exploration using POSETs[END_REF][START_REF] Lilius | Efficient state space search for time Petri nets[END_REF][START_REF] Lugiez | A partial order semantics approach to the clock explosion problem of timed automata[END_REF][START_REF] Yoneda | Efficient verification of parallel real-time systems[END_REF].

The local time semantics approaches suppose that the model consists of a set of components, each one is represented by a timed model (timed automaton, TPN, etc.) and has, in addition to its clocks, a reference clock. The reference clocks evolve asynchronously and are synchronized when needed (i.e., when an action of synchronization is executed). Such approaches need additional clocks and the differences between reference clocks may diverge leading to an infinite state space [START_REF] Lugiez | A partial order semantics approach to the clock explosion problem of timed automata[END_REF].

The partial order reduction approaches based on POSETs aim to force the independency relation by fixing partially the firing order of transitions or events [START_REF] Belluomini | Timed state space exploration using POSETs[END_REF][START_REF] Lilius | Efficient state space search for time Petri nets[END_REF][START_REF] Lugiez | A partial order semantics approach to the clock explosion problem of timed automata[END_REF][START_REF] Yoneda | Efficient verification of parallel real-time systems[END_REF]. The idea is to compute, by exploring one sequence of transitions, the convex hull of the abstract states reachable by some of its equivalent sequences. However, unlike timed automata [START_REF] Salah | On interleaving in timed automata[END_REF], for TPNs, including 1-safe TPNs, this convex hull is not necessarily the union of the abstract states reached by equivalent sequences of transitions [START_REF] Boucheneb | Reducing interleaving semantics redundancy in reachability analysis of time Petri nets[END_REF]. As an example, for the TPN at Fig. 1.b taken from [START_REF] Boucheneb | Reducing interleaving semantics redundancy in reachability analysis of time Petri nets[END_REF], the union of state classes reached by different interleavings of transitions t 1 and t 2 from the initial state class is not equal to their convex hull [START_REF] Boucheneb | Reducing interleaving semantics redundancy in reachability analysis of time Petri nets[END_REF]. From its initial state class α 0 , firing sequences t 1 t 2 and t 2 t 1 lead respectively to state classes α 3 and α 5 .Their convex hull is the state class α 35 = (p 3 + p 4 + 2p 5 , -4 ≤ t 3 -t 4 ≤ 3 ∧ -2 ≤ t 3 -t 5 ≤ 5 ∧ 0 ≤ t 4 -t 5 ≤ 4) (see Fig. 2.a and Table 1). The firing schedule (t 3 = 2,t 4 = 2,t 5 = 2) of α 35 belongs neither to α 3 nor to α 5 . The union of α 3 and α 5 is then not equal to their convex hull. Moreover, if we replace state classes α 3 and α 5 by their convex hull α 35 , we preserve neither boundedness nor reachability properties of the model. Fig. 2.b shows a firing sequence that is neither feasible from α 3 nor from α 5 but feasible from α 35 . Indeed, the infinite sequence t 4 t 3 t 6 t 7 t 7 .... is neither firable from α 3 nor from α 5 . It is however firable from α 35 and produces an infinite number of markings. This issue is caused by the fact that the parent of t 5 depends of the firing order of transitions t 1 and t 2 . The transition t 5 is enabled by t 2 , in case t 1 is fired before t 2 . It is enabled by t 1 , otherwise. Since, the firing delay of a transition is relative to the firing date of its parent, the firing intervals of t 5 in α 3 and α 5 have different references.

In [START_REF] Yoneda | Efficient verification of parallel real-time systems[END_REF], to deal with this issue, the authors keep, in each abstract state, in addition to the time constraints of the enabled transitions, those of their parents. All the different possible parents of the enabled transitions are considered when computing successors of the abstract states. Moreover, the selection procedure of independent transitions takes into account neither the static nor the dynamic timing information of the model. In [START_REF] Lilius | Efficient state space search for time Petri nets[END_REF], the authors have defined a state space abstraction where the firing order constraints between non-related transitions 4 are totally ignored when comput-ing successors. The subset of transitions explored from each abstract state is a persistent set [START_REF] Lilius | Efficient state space search for time Petri nets[END_REF]. However, the state space abstraction proposed in [START_REF] Lilius | Efficient state space search for time Petri nets[END_REF] preserve neither markings nor the firing sequences of the TPN. The counterexample is given by the TPN at Fig. 3 [START_REF] Boucheneb | Stubborn sets for time Petri nets[END_REF].

In [START_REF] Boucheneb | Stubborn sets for time Petri nets[END_REF], the authors have revisited, using POSETS, the stubborn method in the context of time Petri nets. This method yields reduced graphs that preserve the nonequivalent firing sequences of time Petri nets. However, its selection procedure of representative transitions is only based on the structure of the untimed underlying Petri nets and markings. In [START_REF] Boucheneb | Delay-dependent partial order reduction technique for time Petri nets[END_REF], the authors have investigated and proposed a selection procedure that takes into account the static and dynamic firing intervals of transitions. These time constraints allow to relax the selection conditions of representative transitions. For instance, the persistency of an enabled transition t is guarantied, if there is no conflicting transition that can fire before t (i.e., t is eventually fired before all conflicting transitions). So, firing delays between transitions allow to weaken the sufficient condition of persistent transitions. The purpose of the present paper is to improve the approach developed in [START_REF] Boucheneb | Delay-dependent partial order reduction technique for time Petri nets[END_REF], so as to achieve further reduction. The idea is to weaken the selection conditions by taking into better account the static and dynamic firing time constraints of time Petri net. We show that the resulting reduced graph preserves non-equivalent sequences of the TPN. So, the extension of the verification approach proposed here to LT L -X 5 properties over markings could be achieved as shown in [START_REF] Valmari | Can stubborn set be optimal[END_REF].

The rest of the paper is organized as follows. Section 2 is devoted to the TPN, its semantics and its CSCG. Section 3 defines the notions of partial order successor and reduced state class graph. Section 4 is devoted to our reduced state class graph and the proof that it preserves the non-equivalent firing sequences of the TPN. Section 5 reports some experimental results. Finally, the conclusions are presented in Section 6. Let P be a nonempty set. A multi-set over P is a function M : P -→ N, N being the set of natural numbers, defined also by the formal sum:

t 3 [3,5] t 5 [0,2] t 4 [3,4] t 6 [0,0] t 7 [1,1] 2 • • • p 1 p 2 p 3 p 4 t 4 [1,1] t 3 [2,2] t 1 [2,2] t 2 [1,3] • •
∑ p∈P M(p) × p 6 .
We denote by P MS and 0 the set of all multi-sets over P and the empty multiset, respectively. Let M 1 ∈ P MS , M 2 ∈ P MS and ≺∈ {≤, =, <, >, ≥}. Operations on multi-sets are defined as usual:

1) ∀p ∈ P, p ∈ M 1 iff M 1 (p) > 0; 2) M 1 + M 2 = ∑ p∈P (M 1 (p) + M 2 (p)) × p; 3) M 1 ≺ M 2 iff ∀p ∈ P, M 1 (p) ≺ M 2 (p); 4) M 1 ≺ M 2 iff not (M 1 ≺ M 2 ); 5) M 1 × M 2 = ∑ p∈P Min(M 1 (p), M 2 (p)) × p; 6) If the multi-sets M 1 and M 2 are s.t. M 1 ≤ M 2 , then M 2 -M 1 is the multi-set de- fined by: ∑ p∈P (M 2 (p) -M 1 (p)) × p.
Let Q + and R + be the sets of non-negative rational and real numbers, respectively, and

INT X = {[a, b]|(a, b) ∈ X × (X ∪ {∞})}, for X ∈ {Q + , R + },
p = {t ∈ T |post(t)(p) > 0} and p • = {t ∈ T |pre(t)(p) > 0}, respectively.
The transition t is structurally in conflict with a transition t ′ of T iff they share at least an input place, i.e., • t ∩ • t ′ = / 0. We denote by CFS(t) = p∈ • t p • the set of transitions structurally in conflict with t.

Note that t ∈ CFS(t).

We denote by NwS(t) = p∈t • p • the set of output transitions of t (the transitions that may be enabled by firing t).

Several semantics are proposed in the literature for the TPN model [START_REF] Bérard | The expressive power of time Petri nets[END_REF][START_REF] Boucheneb | On multi-enabledness in time Petri nets[END_REF][START_REF] Boyer | Multiple-enabledness of transitions in time Petri nets[END_REF]]. An overview and a classification of the TPN semantics can be found in [START_REF] Boucheneb | On multi-enabledness in time Petri nets[END_REF]. They differ mainly in the interpretation of the notion of newly enabled transition, the characterization of states and the server policy. The notion of newly enabled transitions may refer to the intermediate markings (markings resulting from the consumption of tokens) or the markings before and after firings (intermediate or atomic firing semantics) [START_REF] Bérard | The expressive power of time Petri nets[END_REF]. The timing information is either associated with transitions represented by clocks or delays (threshold semantics) or tokens represented by clocks giving their ages (age semantics) [START_REF] Boyer | Multiple-enabledness of transitions in time Petri nets[END_REF]. The service policy specifies whether several enabling instances of the same transition may be handled simultaneously (multiple-server semantics) or not (single-server semantics). For the single-server semantics, the multi-enabledness is not ambiguous, since only one enabling instance of each transition is considered at each state (i.e., sequential management). However, different interpretations can be defined for multiple-server semantics [START_REF] Boucheneb | On multi-enabledness in time Petri nets[END_REF]. We consider here the classical and widely used semantics (i.e., the threshold, intermediate and single-server semantics).

Each marking of N is a multi-set over P. Let M be a marking of N and t ∈ T a transition. The transition t is enabled at marking M, denoted by M[t> iff all required tokens for firing t are present in M, i.e., M ≥ pre(t). In case t is enabled at M, its firing leads to the marking M ′ = Mpre(t) + post(t). The notation M[t>M ′ means that t is enabled at M and M ′ is the marking reached from M by t. We denote by En(M) the set of transitions enabled at M, i.e.,

En(M) = {t ∈ T | M ≥ pre(t)}.
For t ∈ En(M), we denote by CF(M,t) the set of transitions enabled at M but in conflict with t, i.e., CF(M,t)

= {t ′ ∈ En(M) | t ′ = t ∨ M ≥ pre(t) + pre(t ′ )}. Note that CF(M,t) ⊆ CFS(t).
For any sequence t 1 t 2 ...

t n ∈ T + , the usual notation M[t 1 t 2 ...t n > means that there are markings M 1 , ..., M n so that M 1 = M and M i [t i >M i+1 , for i ∈ [1, n -1] and M n [t n >. The notation M[t 1 t 2 ...t n >M ′
gives, in addition, the marking reached by the sequence.

Let M ′ be the successor marking of M by t. We denote by Nw(M,t) the set of transitions newly enabled at the marking M ′ reached from M by firing t. Formally, Nw(M,t) contains t, if t is enabled at M ′ , and also all transitions enabled at the marking M ′ but not enabled at the intermediate marking

M -pre(t), i.e., Nw(M,t) = {t ′ ∈ En(M ′ ) | t ′ = t ∨ M -pre(t) ≥ pre(t ′ )}. Note that Nw(M,t) ⊆ NwS(t).
Starting from the initial marking M 0 , the marking of N evolves by firing transitions at irregular intervals of time. When a transition t is newly enabled, its firing interval is set to its static firing interval. Bounds of its interval decrease synchronously with time until it is fired or disabled by a conflicting firing. Transition t is firable, if the lower bound of its firing interval reaches 0. It must fire immediately, without any additional delay, when the upper bound of its firing interval reaches 0, unless it is disabled by another firing. The firing of a transition takes no time but leads to a new marking.

Syntactically, in the context of N , a state is defined as a pair s = (M, I), where M is a marking and I is a firing interval function (I:

En(M) → INT R + ). The initial state of N is s 0 = (M 0 , I 0 ), where I 0 (t) = Is(t), for all t ∈ En(M 0 ). Let S = {(M, I) | M ∈ P MS ∧ I: En(M) → INT R + }
be the set of all syntactically correct states, s = (M, I) and s ′ = (M ′ , I ′ ) two states of S , dh ∈ R + a nonnegative real number, t ∈ T a transition and → the transition relation defined by: • s dh → s ′ (s ′ is also denoted by s + dh) iff the state s ′ is reachable from state s by dh time units, i.e., ∀t ∈ En(M), dh ≤ ↑ I(t), M ′ = M and

∀t ′ ∈ En(M ′ ), I ′ (t ′ ) = [Max(0, ↓ I(t ′ ) -dh), ↑ I(t ′ ) -dh]. • s t → s ′ iff
t is immediately firable from s and its firing leads to s ′ , i.e., t ∈ En(M), ↓ I(t) = 0, M ′ = Mpre(t) + post(t), and

∀t ′ ∈ En(M ′ ), I ′ (t ′ ) = Is(t ′ ) if t ′ ∈ Nw(M,t) I(t ′ ) otherwise.
The semantics of N is defined by the transition system (S, →, s 0 ), where S ⊆ S is the set of all states reachable from the initial state s 0 by * → (the reflexive and transitive closure of →).

A run in (S, →, s 0 ), starting from a state s 1 of S, is a maximal sequence ρ = s 1 dh i , where |ρ| is the length of the firing sequence of ρ.

dh 1 → s 1 + dh 1 t 1 → s 2 dh 2 → s 2 + dh 2 t 2 → s 3 ....
An infinite run ρ is diverging if time(ρ) = ∞, otherwise it is said to be zeno. Runs of N are all runs of the initial state s 0 . A TPN model is said to be non-zeno if all its runs are non-zeno. We consider here only non-zeno TPNs. This restriction ensures that each enabled transition will eventually become firable in the future, unless it is disabled by a conflicting transition. The timed language of N is the set of its timed traces. A marking M is reachable in N iff ∃s ∈ S s.t. the marking of s is M.

Contracted state class graph

Let N = (P, T, pre, post, M 0 , Is) be a TPN. Several state space abstractions have been proposed in the literature for N : the State Class Graph (SCG) [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF], the Contracted State Class Graph (CSCG) [START_REF] Boucheneb | A more efficient time Petri net state space abstraction useful to model checking timed linear properties[END_REF], the Geometric Region Graph (GRG) [START_REF] Yoneda | CTL model checking of time Petri nets using geometric regions[END_REF], the Strong State Class Graph (SSCG) [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF], the Zone Based Graph (ZBG) [START_REF] Boucheneb | TCTL model checking of time Petri nets[END_REF] and the Atomic State Class Graphs (ASCGs) [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF][START_REF] Boucheneb | CTL* model checking for time Petri nets[END_REF][START_REF] Yoneda | CTL model checking of time Petri nets using geometric regions[END_REF]. In such abstractions, all states grouped in the same node share the same marking and the union of their time domains is represented by a consistent conjunction of atomic constraints 7 .

From a practical point of view, every conjunction of atomic constraints is represented by means of a Difference Bound Matrix (DBM) [START_REF] Bengtsson | Clocks, DBMs and States in Timed Systems[END_REF]. Although the same nonempty domain may be encoded by different conjunction of atomic constraints, their DBMs have a canonical form. The canonical form of a DBM is the representation with tightest bounds on all differences between variables, computed by propagating the effect of each entry through the DBM. Two conjunctions of atomic constraints are equivalent (i.e., represent the same domain) iff their DBMs have the same canonical form. Canonical forms make operations over formulas much simpler [START_REF] Bengtsson | Clocks, DBMs and States in Timed Systems[END_REF].

Among these abstractions, we consider the CSCG. The CSCG is the quotient graph of the SCG [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF] w.r.t. some relation of equivalence over state classes of the SCG [START_REF] Boucheneb | A more efficient time Petri net state space abstraction useful to model checking timed linear properties[END_REF]. Intuitively, this relation groups together all state classes, which have the same marking and triangular constraints 8 , but not necessarily the same simple atomic constraints 9 . The CSCG and SCG have the same reachable markings and firing sequences [START_REF] Boucheneb | A more efficient time Petri net state space abstraction useful to model checking timed linear properties[END_REF]. In other words, the CSCG preserves markings and firing sequences of the SCG, which, in turn, preserves markings and firing sequences of N [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF]. The CSCG of N is finite iff N is bounded (i.e. has a finite number of reachable markings).

Syntactically, a CSCG state class is defined as a pair α = (M, F), where M is a marking and F is a consistent conjunction of triangular atomic constraints over firing delays of transitions enabled at M. The formula F characterizes the union of firing time domains of all states within α. By convention, F = true if the number of enabled transitions at M is less than 2 (i.e., there is no triangular atomic constraint in F). A state s ′ = (M ′ , I ′ ) belongs to α iff M = M ′ and its firing time domain (i.e.,

t∈En(M ′ ) ↓ I ′ (t) ≤ t ≤ ↑ I ′ (t)
) is included in the firing time domain of α (i.e., F).

The CSCG initial state class is α 0 = (M 0 , F 0 ), where

F 0 = t,t ′ ∈En(M 0 ) s.t. t =t ′ t -t ′ ≤ ↑ Is(t) -↓ Is(t ′ ),
t and t ′ being real-valued variables representing firing delays of transitions t and t ′ , respectively. It keeps only the triangular atomic constraints of the SCG initial state class.

Let C S be the set of all syntactically correct CSCG state classes and succ a successor function from C S × T to C S ∪ { / 0} defined by: ∀α ∈ C S , ∀t f ∈ T, succ(α,t f ) = / 0 (i.e., t f is firable from α) iff t f ∈ En(M) and the following formula is consistent (its domain is not empty):

F ∧ ( t∈En(M) t f -t ≤ 0).
Intuitively, this formula, called the firing condition of t f from α, means that t f is firable from α before all other transitions enabled at M. In other words, there is at least a valuation of firing delays in F s.t. t f has the smallest firing delay.

-If succ(α,t f ) = / 0 then succ(α,t f ) = (M ′ , F ′ ), where:

M ′ = M -pre(t f ) + post(t f ) and F ′ is computed in three steps: 1) Set F ′ to F ∧ t∈En(M) t f -t ≤ 0 ∧ t ′ ∈Nw(M,t f ) ↓ Is(t ′ ) ≤ t ′ f -t f ≤↑ Is(t ′ ) (Variables t ′ f for t ′ ∈ Nw(M,t f
) are new variables introduced for representing the firing delays of the newly enabled transitions. The notation t ′ f allows to deal with the situation where t ′ is enabled before firing t f and newly enabled by t f (i.e.

t ′ ∈ CF(M,t f ) ∩ Nw(M,t f )). The new instance of t ′ is temporally represented by t ′ f , in this step);
2) Put F ′ in canonical form 10 and eliminate all transitions of CF(M,t f );

3) Rename each t ′ f into t ′ . Let α = (M, F) ∈ C S . We denote by Fr(α) = {t ∈ T | succ(α,t) = /
0} the set of transitions firable from α. The function succ is extended to sequences of transitions as follows: ∀ω ∈ T * , succ(α, ω) = succ(succ(α, ω 1 ), ω 2 ), where ω = ω 1 ω 2 and, by convention, succ(α, ε) = α, ε being the empty sequence. We denote by ||ω|| ⊆ T the set of transitions appearing in ω.

The CSCG of N is the structure C = (C , succ, α 0 ), where α 0 is the initial CSCG state class of N and C is the set of state classes accessible from α 0 by applying re- peatedly the successor function succ, i.e.,

C = {α ∈ C S |∃ω ∈ T * , α = succ(α 0 , ω) = / 0}. A sequence ω ∈ T + is a firing sequence of C iff succ(α 0 , ω) = / 0. p 1 p 2 p 3 p 4 t 1 [1,2] t 2 [2,3] t 3 [2,2] t 4 [1,1] • •
α 0 = (p 1 + p 2 , -1 ≤ t 1 -t 2 ≤ 1)
. There are two enabled transitions t 1 and t 2 , which are also firable from α 0 , since their firing conditions

-1 ≤ t 1 -t 2 ≤ 1 ∧ t 1 ≤ t 2 and -1 ≤ t 1 -t 2 ≤ 1 ∧ t 2 ≤ t 1 are consistent.
For instance, let us compute the successor of α 0 by t 1 . The firing of t 1 leads to the state class α 1 = (p 2 + p 3 , -2 ≤ t 2 -t 3 ≤ -1). Its marking is computed as usual. Its formula is computed in three steps: 1) Set the formula to the firing condition of t 1 from α 0 augmented with time con- straints of transition t 3 newly enabled by t 1 :

-1 ≤ t 1 -t 2 ≤ 1 ∧ t 1 ≤ t 2 ∧ t 1 3 -t 1 = 2; 2) Put the formula in canonical form and eliminate t 1 : -2 ≤ t 2 -t 1 3 ≤ -1; 3) Rename t 1 3 in t 3 : -2 ≤ t 2 -t 3 ≤ -1. Following the same procedure, we get succ(α,t 1 t 2 ) = (p 3 + p 4 , 0 ≤ t 3 -t 4 ≤ 1) and succ(α,t 2 t 1 ) = (p 3 + p 4 , 1 ≤ t 3 -t 4 ≤ 2).
3 Partial order reduction based on POSETs

Partial order successors and reduced state class graphs

The idea of partial order successors is to relax the firing condition of a transition by eliminating some firing order constraints when computing successors of state classes. The aim is to handle concisely the equivalent sequences of transitions, obtained by permuting some independent transitions (i.e., partially ordered sets of transitions). As a result, the union of state classes reached by all these sequences is computed by exploring only one of them.

Definition 2 Let α = (M, F) be a state class of C S , t f ∈ T a transition and X ⊆ T a subset of transitions. The partial order successor of α by t f w.r.t. X, denoted by succ X (α,t f ), is either equal / 0 or a state class of C S defined by:

succ X (α,t f ) = / 0 iff X ∩ En(M) = / 0 ∧ succ(α,t f ) = / 0.
If succ X (α,t f ) = / 0 then the state class α ′ = succ X (α,t f ) is computed as succ(α,t f ), except that the firing condition, used in step 1, is replaced with:

F ∧ t∈X∩En(M) t f ≤ t. Formally, if succ X (α,t f ) = / 0 then succ X (α,t f ) = (M ′ , F ′ ), where M ′ = M -pre(t f ) + post(t f ) and F ′ is computed in three steps: 1) Set F ′ to F ∧ t∈X∩En(M) t f ≤ t ∧ t ′ ∈Nw(M,t f ) ↓ Is(t ′ ) ≤ t ′ f -t f ≤↑ Is(t ′ );
2) Put F ′ in canonical form and eliminate all transitions of CF(M,t f ); 3) Rename each t ′ f in t ′ . The formula used in step 1, called the processing formula of succ X (α,t f ), does not impose any firing order between t f and transitions of En(M) -X. Therefore, it holds that ∀t f ∈ T, succ(α,t f ) ⊆ succ X (α,t f ) and succ En(M) (α,t f ) = succ(α,t f ).

Example 2 Consider the model T PN2 at Fig. 1.b and its initial state class α 0 = (p 1 + p 2 , -1 ≤ t 1 -t 2 ≤ 1). Transitions t 1 and t 2 are both enabled and firable from α 0 . Therefore, succ {t 1 } (α 0 ,t 1 ) = / 0 and succ {t 2 } (α 0 ,t 2 ) = / 0. Let α ′ 1 = succ {t 1 } (α 0 ,t 1 ). Let us show how to compute the firing domain formulas of α ′ 1 and α ′ 2 = succ {t 2 } (α ′ 1 ,t 2 ). For the state class α ′ 1 = (p 2 + p 3 , F ′ 1 ), its firing domain formula F ′ 1 is computed in three steps as follows:

1) Set F ′ 1 to -1 ≤ t 1 -t 2 ≤ 1 ∧ t n 3 -t 1 = 2; 2) Put the formula in canonical form and eliminate t 1 : -3 ≤ t 2 -t n 3 ≤ -1; 3) Rename t n 3 in t 3 : -3 ≤ t 2 -t 3 ≤ -1. For the state class α ′ 2 = (p 3 + p 4 , 0 ≤ t 3 -t 4 ≤ 2)
, its firing domain formula F ′ 2 is computed in three steps as follows:

1) Set F ′ 2 to -3 ≤ t 2 -t 3 ≤ -1 ∧ t n 4 -t 2 = 1;
2) Put the formula in canonical form and eliminate t 1 : 0 ≤ t 3t n 4 ≤ 2; 3) Rename t n 4 in t 4 : 0 ≤ t 3t 4 ≤ 2. Note that succ {t 2 } (succ {t 1 } (α 0 ,t 1 ),t 2 ) = succ(α 0 ,t 1 t 2 ) ∪ succ(α 0 ,t 2 t 1 ).

Therefore, succ(succ {t 2 } (succ {t 1 } (α 0 ,t 1 ),t 2 ),t 3 ) gives the union of state classes reached by sequences t 1 t 2 t 3 and t 2 t 1 t 3 . The union of these sequences can be represented by the partially ordered set ({t 1 ,t 2 ,t 3 },t 1 ≤ t 3 ∧ t 2 ≤ t 3 ).

We provide, in the following, some relationships between successors and partial order successors of state classes, which will be helpful to establish a partial order reduction technique and prove that it preserves the non-equivalent firing sequences of the TPN. Let us first define the notion of effect-independent transitions used in our partial order reduction technique (instead of the notion of truth parent [START_REF] Yoneda | Efficient verification of parallel real-time systems[END_REF]).

Definition 3 Let t i ,t j ∈ T be two transitions. Transitions t i and t j are structurally effect-independent, denoted by t i ||t j iff their effects are independent of their firing order from any marking, i.e.,

(CFS(t i ) ∪ NwS(t i )) ∩ (CFS(t j ) ∪ NwS(t j )) = / 0
Let α = (M, F) ∈ C S be a state class, t i ∈ Fr(α) and t j ∈ Fr(α) two transitions firable from α. Let M i and M j be the successor markings of M by t i and t j , respectively (i.e., M[t i > M i and M[t j > M j ). Transitions t i and t j are effect-independent from α, denoted by t i || α t j iff their effects from α are independent of their firing order, i.e.,

CF(M,t

i ) = CF(M j ,t i ) ∧ CF(M,t j ) = CF(M i ,t j ) ∧ Nw(M,t i ) = Nw(M j ,t i ) ∧ Nw(M,t j ) = Nw(M i ,t j ).
In other words, from M, each of transitions t i and t j will disable (enable) the same set of transitions no matter of which transition is fired first.

Note that relations || α and || are symmetric (i.e., t i || α t j iff t j || α t i and t i ||t j iff t j ||t i ).

Lemma 1 Let α = (M, F) ∈ C S , t i ∈ Fr(α), M i the successor marking of M by t i , and X a subset of transitions s.t. CF(M,t

i ) ⊆ X. (i) ∀t j ∈ Fr(α), t i ||t j ⇒ t i || α t j . (ii) ∀t j ∈ En(M i ) -Fr(α), succ(succ X (α,t i ),t j ) = succ(α,t i t j ). (iii) ∀t j ∈ X ∩ En(M i ), succ(succ X (α,t i ),t j ) = succ(α,t i t j ). (iv) ∀t j ∈ Fr(α) -X, s.t. X ⊆ En(M) ∧ X ∩ CF(M,t j ) = / 0 ∧ t i || α t j , succ(succ X (α,t i ),t j ) = succ(α,t i t j ) ∪ succ X (succ(α,t j ),t i ).
Proof By assumption, the transition t i ∈ Fr(α) and CF(M,t i ) ⊆ X. Therefore, X ∩ En(M) = / 0, succ(α,t i ) = / 0 and succ X (α,t i ) = / 0. Proof of (i): Suppose that t i || α t j does not hold and let us show that t i ||t j does not hold too. By definition, ¬t i || α t j implies that at least one of the following statements holds CF(M,t i ) = CF(M j ,t i ), CF(M,t j ) = CF(M i ,t j ), Nw(M,t i ) = Nw(M j ,t i ) or Nw(M,t j ) = Nw(M i ,t j ). Therefore, one of the transitions t i and t j may disable / enable a transition in conflict with the other or an output transition of the other. It means that (CFS(t i ) ∪ NwS(t i )) ∩ (CFS(t j ) ∩ NwS(t j )) = / 0. Therefore, ¬(t i ||t j ). Proof of (ii) and (iii): The processing formula of succ(succ X (α,t i ),t j ), denoted by φ , is:

(F ∧ t∈X∩En(M) t i ≤ t ∧ t ′ ∈Nw(M,t i ) ↓ Is(t ′ ) ≤ t i -t i ≤↑ Is(t ′ )) ∧ ( t∈En(M i )-Nw(M,t i ) t j ≤ t ∧ t ′ ∈Nw(M,t i ) t j ≤ t ′i ∧ t ′ ∈Nw(M i ,t j ) ↓ Is(t ′ ) ≤ t ′ j -t j ≤↑ Is(t ′ )).
By assumption, t j ∈ En(M i ) -Fr(α) or t j ∈ X ∩ En(M i ). We consider three cases: t j ∈ Nw(M,t i ) (i.e., t j is newly enabled M i ), t j ∈ (En(M) -CF(M,t i )) ∩ X (i.e., t j is not newly enabled in M i and belongs to X) or t j ∈ En(M) -Fr(α) (i.e., t j is neither newly enabled in M i nor firable in α). In all cases, it holds that (φ ∧ t i ≤ t j ) ≡ φ . By definition, En(M i ) = (En(M) -CF(M,t i )) + Nw(M,t i ). Therefore, the following constraints of φ : t i ≤ t j ∧t j ≤ t, for t ∈ En(M)-CF(M,t i ) imply t i ≤ t for t ∈ En(M)-CF(M,t i ). Adding these redundant constraints to φ does not affect its domain. Since CF(M,t i ) ⊆ X, it follows that En(M) = (En(M)∩X)∪(En(M)-CF(M,t i )) and then φ is equivalent to:

(F ∧ t∈En(M) t i ≤ t ∧ t ′ ∈Nw(M,t i ) ↓ Is(t ′ ) ≤ t ′i -t i ≤↑ Is(t ′ ))∧ ( t∈En(M i )-Nw(M,t i ) t j ≤ t ∧ t ′ ∈Nw(M,t i ) t j ≤ t ′i ∧ t ′ ∈Nw(M i ,t j ) ↓ Is(t ′ ) ≤ t ′ j -t j ≤↑ Is(t ′ )).
Therefore, succ(succ X (α,t i ),t j ) = succ(α,t i t j ).

Proof of (iv): By assumption, t i ∈ Fr(α), t j ∈ Fr(α)-X ⊆ En(M) and CF(M,t i ) ⊆ X. Then, X = En(M)∩X, succ(α,t i t j ) = / 0 and succ(α,t i t j ) ⊆ succ(succ X (α,t i ),t j ) = / 0. Consider now the processing formula above φ of succ(succ X (α,t i ),t j ). It holds that φ ≡ ((φ ∧ t i ≤ t j ) ∨ (φ ∧ t j ≤ t i )). Following the same steps as in the proof of (ii) and (iii), we show that (φ ∧t i ≤ t j ) is equivalent to the firing condition of succ(α,t i t j ). For (φ ∧ t j ≤ t i ), by definition, En(M i ) = (En(M) -CF(M,t i )) + Nw(M,t i ) and, by assumption, X ∩CF(M,t j ) = / 0. Therefore, the following constraints of φ : t j ≤ t i ∧t i ≤ t, for t ∈ X ∪ Nw(M,t i ) imply t j ≤ t for t ∈ X ∪ Nw(M,t i ). Adding the redundant constraints t j ≤ t for t ∈ X to φ ∧ t j ≤ t i does not affect its domain. Moreover, the constraint t j ≤ t for t ∈ Nw(M,t i ) are redundant in φ ∧ t j ≤ t i . So, they can be eliminated from φ ∧ t j ≤ t i without affecting its domain. Since CF(M,t i ) ⊆ X, it follows that En(M) = (En(M) -CF(M,t i )) ∪ X. Therefore, we can state that φ ∧ t j ≤ t i is equivalent to:

(F ∧ t∈X t i ≤ t ∧ t ′ ∈Nw(M,t i ) ↓ Is(t ′ ) ≤ t ′i -t i ≤↑ Is(t ′ ))∧ ( t∈En(M) t j ≤ t ∧ t ′ ∈Nw(M i ,t j ) ↓ Is(t ′ ) ≤ t ′ j -t j ≤↑ Is(t ′ )).
Let M j be the successor marking of M by t j . By definition, En(M j ) = En(M) -CF(M,t j ) + Nw(M,t j ). Since by assumption X ∩CF(M,t j ) = / 0, it follows that X ⊆ En(M j ) and then X = En(M j ) ∩ X. By assumption, t i || α t j , which imply Nw(M,t i ) = Nw(M j ,t i ) and Nw(M,t j ) = Nw(M i ,t j ). Then, φ ∧t j ≤ t i is equivalent to the processing formula of succ X (succ(α,t j ),t i ). Consequently, succ(succ X (α,t i ),t j ) = succ(α,t i t j ) ∪ succ X (succ(α,t j ),t i ).

⊓ ⊔

Intuitively, given a selection procedure (over state classes) of the representative transitions, a reduced state class graph based on POSETs is generated by first computing the partial order successors of the initial state class, by its selected transitions, and then repeating the procedure for each computed but not processed state class.

, α ′ ∈ C S , ∀t f ∈ T, α t f -→ G α ′ iff t f ∈ G(α) ∧ succ(α,t f ) = / 0 ∧ α ′ = succ G(α) (α,t f ). Let α ∈ C G and ω = t 1 t 2 ...t n be a sequence of transitions. We write α ω -→ G α n iff ∃α 1 , α 2 , ..., α n ∈ C G s.t. α t 1 -→ G α 1 t 2 -→ G α 2 ... t n -→ G α n , with α n = succ G (α, ω).
The RSCG R preserves the non-equivalent sequences of the CSCG C iff for each maximal sequence of R, there is an equivalent sequence in C and vice-versa.

RSCG preserving non-equivalent sequences of N

We propose, in the following, a partial order generator G and show that it results in a RSCG preserving non-equivalent sequences of the CSCG. The proposed generator takes into account the structure of the TPN, including the static firing intervals of transitions, the marking and the firing domain of the current state class. The timing information derived from the structure of the TPN is captured in a matrix called the delay lower bound matrix.

Static delay lower bound matrix of N

According to the TPN semantics, when a transition t j is fired, the conflicting transitions are disabled and new transitions may be enabled. The firing delay interval of each newly enabled transition t i refers to its enabling date (i.e., the firing date of t j ). The lower bound of the firing delay of transition t i relatively to the firing date of t j is ↓ Is(t i ). We define the delay lower bound matrix L as a square matrix over the set of transitions T , where: ∀t i ,t j ∈ T,

l i j =      0 if t i = t j ↓ Is(t i ) if t i = t j ∧ t i ∈ NwS(t j ) ∞ otherwise.
We denote by L the canonical form of L obtained by applying the Floyd-Warshall's shortest path algorithm. This algorithm converges, as the lower bounds of the static firing intervals are non-negative finite rational numbers. Intuitively, li j is a lower bound of the firing delay of t i , relatively to the firing date of t j , for the case where t i is not enabled when t j is fired. Note that li j = ∞ means that there is no path connecting t j to t i and then t i cannot be enabled directly or indirectly by t j .

Table 2 Firing delay lower bound matrix of TPN3 at Fig. 3 and its canonical form

L t 1 t 2 t 3 t 4 t 1 0 ∞ ∞ 1 t 2 ∞ 0 ∞ 2 t 3 1 ∞ 0 ∞ t 4 2 2 ∞ 0 L t 1 t 2 t 3 t 4 t 1 0 2 ∞ 1 t 2 2 0 ∞ 1 t 3 2 4 0 3 t 4 1 1 ∞ 0 Example 3

Computing a partial order generator G

Several algorithms have been proposed in the literature to compute partial order generator G for the RSCG preserving different kinds of properties such as deadlocks and LT L -X properties. In general, these algorithms infer G from the static structure of the model, without taking into account the timing information.

This section proposes an algorithm for computing G inspired from the stubborn sets method [START_REF] Valmari | Can stubborn set be optimal[END_REF][START_REF] Yoneda | Efficient verification of parallel real-time systems[END_REF], but does not use the notion of truth parent [START_REF] Yoneda | Efficient verification of parallel real-time systems[END_REF]. As in [START_REF] Boucheneb | Delay-dependent partial order reduction technique for time Petri nets[END_REF], it uses the notion of effect-independent transitions and the (static and dynamic) timing information of the model. Its purpose is to weaken, by considering firing order time constraints, the selection conditions provided in [START_REF] Boucheneb | Delay-dependent partial order reduction technique for time Petri nets[END_REF], so as to achieve further reductions. The proof that G preserves the non-equivalent firing sequences of N is stated in Theorem 1. It is based on some useful properties established in Lemma 2. The notation

G |= SC is an abbreviation of ∀α ∈ C S , G(α) |= SC. Lemma 2 (i) G |= SC ⇒ ∀α ∈ C S , ∀ω ∈ (T -(G(α) ∩ Fr(α))) + , succ(α, ω) = / 0 ⇒ ∃t i ∈ G(α) ∩ Fr(α), (i) succ(α, ωt i ) = / 0 ∧ (ii) succ(α,t i ω) = / 0. (ii) G |= C1 ⇒ ∀α ∈ C S , ∀ω ∈ T + , succ G (α, ω) = / 0 ⇒ ∃ω ′ ≡ ω, succ(α, ω ′ ) = / 0.
Proof (i): By C3, there is at least a transition t i of G(α) ∩ Fr(α) s.t. t j / ∈ CFS(t i ) ∨ d i j < 0, for each t j ∈ G(α) -Fr(α). Let us show that for such a transition t i , it holds that:

∀ω ∈ (T -(G(α) ∩ Fr(α))) + , succ(α, ω) = / 0 ⇒ (i) succ(α, ωt i ) = / 0 ∧ (ii) succ(α,t i ω) = / 0.
Each transition t j of ω belongs T -(G(α) ∩ Fr(α)). Let us consider four cases: t j ∈ Fr(α) -G(α), t j ∈ G(α) -Fr(α), t j ∈ (En(M) -Fr(α)) -G(α) and t j ∈ T -En(M). a) if t j ∈ Fr(α) -G(α) then, by C1, t i ||t j , which implies that t j / ∈ CFS(t i ). b) If t j ∈ G(α) -Fr(α) then d i j ≥ 0, as t j can be fired before t i . By assumption, t j / ∈ CFS(t i ). c) If t j ∈ (En(M) -Fr(α)) -G(α) then d i j ≥ 0. By C1, t j / ∈ CFS(t i ). d) If t j ∈ T -En(M) then t j is enabled directly or indirectly by some transition of Fr(α) -G(α) before firing t i . By C2, t j / ∈ CFS(t i ). All transitions of ω are not structurally in conflict with t i . Therefore, succ(α, ω) = / 0 implies that succ(α, ωt i ) = / 0 and succ(α,t i ω) = / 0. (ii) (by induction on the length of ω):

a) For ω = t 1 , by definition, succ G(α) (α,t 1 ) = / 0 iff succ(α,t 1 ) = / 0. b) For ω = t 1 t 2 , succ G (α,t 1 t 2 ) = / 0 iff succ(succ G(α) (α,t 1 ),t 2 ) = / 0. If t 2 ∈ G(α) or t 2 /
∈ Fr(α), by Lemma 1, succ(succ G(α) (α,t 1 ),t 2 ) = succ(α,t 1 t 2 ) = / 0. Otherwise, from C1 of SC and Lemma 1, it follows that t 1 ||t 2 , sequences t 1 t 2 and t 2 t 1 are firable from α, and succ(succ

G(α) (α,t 1 ),t 2 ) = succ(α,t 1 t 2 ) ∪ succ G(α) (succ(α,t 2 ),t 1 ). c) For ω = t 1 ...t n of length n > 2, succ G (α, ω) = / 0 iff succ(succ G (α,t 1 ...t n-1 ),t n ) = / 0. Let α n-1 = succ G (α,t 1 ...t n-2 ). If t n ∈ G(α n-1 ) or t n / ∈ Fr(α n-1 ), according to Lemma 1, succ(succ G (α,t 1 ...t n-1 ),t n ) = succ(succ G (α,t 1 ...t n-2 ),t n-1 t n ).
Otherwise, using C1 of SC and Lemma 1, we can state that t n-1 ||t n , sequences t n-1 t n and t n t n-1 are firable from succ G (α,t 1 ...t n-2 ), and succ(succ G (α,t 1 ..

.t n-1 ),t n ) = succ(succ G (α,t 1 ...t n-2 ),t n-1 t n ) ∪ succ G(α n-1 ) (succ(succ G (α,t 1 ...t n-2 ),t n ),t n-1
). Now, it suffices to repeat the same process for succ(succ G (α,t 1 ...t n-2 ),t n-1 ) and all derived terms, until reaching terms where succ is directly applied on α. As G |= C1, each time two adjacent transitions are permuted, they are firable in both order and effect-independent. Otherwise, they are at least firable in one order. Therefore,

succ G (α, ω) = / 0 ⇒ ∃ω ′ ≡ ω, succ(α, ω ′ ) = / 0. ⊓ ⊔ Theorem
= (M, F) ∈ C S , (i) ∀ω ∈ Ω (M), succ(α, ω) = / 0 ⇒ ∃ω ′ ∈ T + , ω ≡ ω ′ ∧ succ G (α, ω ′ ) = / 0 and (ii) ∀ω ∈ Ω (M), succ G (α, ω) = / 0 ⇒ ∃ω ′ ∈ T + , ω ≡ ω ′ ∧ succ(α, ω ′ ) = / 0. (i):
By assumption, ω is a maximal sequence of M and succ(α, ω) = / 0. Then, Fr(α) = / 0. By C0 of SC, G(α) ∩ Fr(α) = / 0. From the fact that the TPN has no unbounded intervals, the non-zenoness, assumed here, guarantees that each enabled transition will eventually fire in the future, unless it is disabled by another firing. Conditions C1 and C2 ensure that the transitions outside G(α) cannot disable any transition of G(α). By C3 and Lemma 2,

∃t f ∈ G(α) ∩ Fr(α), ∃ω 1 ∈ (T - (G(α) ∩ Fr(α))) * , ∃ω 2 ∈ T * , ω = ω 1 t f ω 2 ∧ succ(α, ω 1 ) = / 0 ∧ succ(α, ω 1 t f ) = / 0 ∧ succ(α,t f ω 1 ) = / 0. Since succ(α,t f ω 1 ) ⊆ succ(succ G(α) (α,t f ), ω 1 ), it follows that succ(succ G(α) (α,t f ), ω 1 ω 2 ) = / 0. Let α 1 = succ G(α) (α,t f ) = (M 1 , F 1 )
. The sequence ω 1 ω 2 is a maximal sequence of M 1 . We repeat the same process for α 1 and ω 1 ω 2 until reaching a deadlock or a state class already processed. Therefore, ∃ω ′ ∈ T + , ω ′ ≡ ω ∧ succ G (α, ω ′ ) = / 0. (ii): is immediate from Lemma 2.

⊓ ⊔

For a TPN with unbounded firing intervals, the non-zenoness, assumed here, guarantees that each enabled transition will become firable in the future, unless it is disabled by another firing. However, the firing of a transition, with an unbounded static firing interval, may be delayed indefinitely to lead in the reduced graph to some cycle such that the transition is firable from all state classes of the cycle but does not belong to their G (unfair sequence). The fairness criterion (we must not indefinitely neglect some transition) is not guaranteed by SC. To deal with the fairness criterion, G has to satisfy, in addition to SC, the Cycle closing condition, i.e., for every cycle in the reduced state class graph, there is at least one state class s.t. its G is equal to its set of firable transitions (fully expanded node) considered in [START_REF] Peled | Stutter invariant temporal properties are expressible without the next-time operator[END_REF] to address the same problem. With this additional condition, Theorem 1 is also valid for TPNs with unbounded static firing intervals. t p 1 e [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF][START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF] tredo3 [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF][START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF] t 11 [START_REF] Belluomini | Timed state space exploration using POSETs[END_REF][START_REF] Bengtsson | Clocks, DBMs and States in Timed Systems[END_REF] t p 1 j [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF][START_REF] Bérard | The expressive power of time Petri nets[END_REF] tok3 [START_REF] Bengtsson | Clocks, DBMs and States in Timed Systems[END_REF][START_REF] Bengtsson | Clocks, DBMs and States in Timed Systems[END_REF] t 12 [START_REF] Bengtsson | Clocks, DBMs and States in Timed Systems[END_REF][START_REF] Bengtsson | Partial order reductions for timed systems[END_REF] t p 2 j [START_REF] Belluomini | Timed state space exploration using POSETs[END_REF][START_REF] Belluomini | Timed state space exploration using POSETs[END_REF] tback3 [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF][START_REF] Bérard | The expressive power of time Petri nets[END_REF] t 13 [START_REF] Belluomini | Timed state space exploration using POSETs[END_REF][START_REF] Belluomini | Timed state space exploration using POSETs[END_REF] t p 2 e [START_REF] Belluomini | Timed state space exploration using POSETs[END_REF][START_REF] Belluomini | Timed state space exploration using POSETs[END_REF] tin4 [START_REF] Belluomini | Timed state space exploration using POSETs[END_REF][START_REF] Bengtsson | Partial order reductions for timed systems[END_REF] t 14 [START_REF] Belluomini | Timed state space exploration using POSETs[END_REF][START_REF] Belluomini | Timed state space exploration using POSETs[END_REF] t p 1 s [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF][START_REF] Bengtsson | Partial order reductions for timed systems[END_REF] tredo4 [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF][START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF] t 15 [START_REF] Belluomini | Timed state space exploration using POSETs[END_REF][START_REF] Belluomini | Timed state space exploration using POSETs[END_REF] t p 12 [START_REF] Bengtsson | Clocks, DBMs and States in Timed Systems[END_REF][START_REF] Bengtsson | Clocks, DBMs and States in Timed Systems[END_REF] tok4[2,2] t 16 [START_REF] Belluomini | Timed state space exploration using POSETs[END_REF][START_REF] Bengtsson | Clocks, DBMs and States in Timed Systems[END_REF] t p 2 s [START_REF] Bérard | The expressive power of time Petri nets[END_REF][START_REF] Bérard | The expressive power of time Petri nets[END_REF] tback4 [START_REF] Bengtsson | Partial order reductions for timed systems[END_REF][START_REF] Bérard | The expressive power of time Petri nets[END_REF] t 17 [START_REF] Belluomini | Timed state space exploration using POSETs[END_REF][START_REF] Belluomini | Timed state space exploration using POSETs[END_REF] tm 3 [1,2] t 18 [START_REF] Belluomini | Timed state space exploration using POSETs[END_REF][START_REF] Bérard | The expressive power of time Petri nets[END_REF] t p 12 m 3 [1,1] t p 12 s [START_REF] Bengtsson | Clocks, DBMs and States in Timed Systems[END_REF][START_REF] Bengtsson | Clocks, DBMs and States in Timed Systems[END_REF] tx [START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF][START_REF] Berthomieu | State class constructions for branching analysis of time Petri nets[END_REF] 5 Experimental results

We have tested the partial order technique, proposed here, on several small TPNs, the extension with static firing intervals of three models taken from the MCC (Model Checking Contest) held within Petri Nets 2013 11 : HouseConstruction (HC in short), FMS and Kanban (KB in short) (see Table 3 for their static firing intervals). Table 4 reports the number of state classes (NSC), the number of computed state classes (NCSC) and the CPU time in seconds of the RSCG, RSCG' and CSCG for HC and FMS and KB. The column RSCG' is the reduced graph of the approach proposed in [START_REF] Boucheneb | Delay-dependent partial order reduction technique for time Petri nets[END_REF]. Note that for a state class α, G(α) is computed by choosing randomly a firable transition t f from Fr(α), then applying recursively, C1, C2 and C3 until a fix point is reached. Its size is dependent on the first selected transition.

The models HC(n) and KB(n) are free-choice and connected TPNs 12 . For HC(n), n is the initial marking of the source place p 1 . For KB(n), n is the initial marking of places p 1 , p 2 , p 3 and p 4 . The model FMS(n) is a strongly-connected TPN 13 , n being the initial marking of places p 1 , p 2 and p 3 .

For all tested models, the RSCG shows a significant reduction in time and number of computed state classes, compared to the CSCG and the RSCG'. The gain (in time and space) of the RSCG over the CSCG and RSCG' is much more significant for the connected TPNs (HC(n)) and (KB(n)) than the strongly-connected TPN (FMS(n)). The reason is that in the strongly-connected TPN, several transitions are in conflict or not effect-dependent. Furthermore, we obtain further reduction, when we increase the marking, as it results in increasing the number of concurrent enabled transitions.

Conclusion

In this paper, we have considered the TPN model and proposed, using its CSCG, a partial order reduction technique, which preserves non-equivalent firing sequences of the TPN.

Our technique is inspired from the stubborn sets [START_REF] Valmari | Can stubborn set be optimal[END_REF][START_REF] Yoneda | Efficient verification of parallel real-time systems[END_REF] but is based on the notion of effect-independent transitions, instead of the notion of truth parent used in [START_REF] Yoneda | Efficient verification of parallel real-time systems[END_REF]. The notion of truth parent involves to keep, in each abstract state, in addition to time constraints of the enabled transitions, those of their parents. All possible parents of the enabled transitions are considered separately when computing successors of abstract states. Moreover, as in [START_REF] Boucheneb | Delay-dependent partial order reduction technique for time Petri nets[END_REF], our technique takes into account the (static and dynamic) timing information of the model.

For the tested models, our technique allows a significant gain in time and space, in comparison with the RSCG of [START_REF] Boucheneb | Delay-dependent partial order reduction technique for time Petri nets[END_REF] and the CSCG.

Fig. 1

 1 Fig. 1 Time Petri nets used to illustrate features of the interleaving

  t

Fig. 3 TPN3Example 1

 31 Fig.3 TPN3

Definition 4

 4 Let C = (C , succ, α 0 ) be the CSCG of a TPN N and G a function from C S to 2 T called a partial order generator. The reduced state class graph (RSCG for short) generated by G is the tuple R = (G, C G , succ G , α 0 ), where C G = {α|α 0 * -→ G α} is the set of reachable state classes in R and * -→ G is the reflexive and transitive closure of the transition relation -→ G defined by: ∀α

Fig. 4

 4 Fig.4Condition C2 of SC: lk j ≤ d i j for t i ∈ G(α),t j ∈ En(M),t k ∈ CFS(t i )

  the set of intervals whose lower and upper bounds are in X and X ∪ {∞}, respectively. Definition 1 A time Petri net is a tuple N = (P, T, pre, post, M 0 , Is) where -P and T are finite and nonempty sets of places and transitions s.t. P ∩ T = / 0; pre and post are the backward and forward incidence functions (pre, post : T -→ P MS ); -M 0 ∈ P MS is the initial marking; Is is the static firing function (Is : T → INT Q + ). 0} denote the sets of input and output places of t, respectively. Similarly, for p ∈ P, the sets of input and output transitions of p are denoted by•

	↓ Is(t) and ↑ Is(t) denote the lower and upper bounds of the static firing interval
	of transition t.

For t ∈ T , • t = {p ∈ P|pre(t)(p) > 0} and t • = {p ∈ P|post(t)(p) >

  By convention, for any state s i , relation → s i holds. Sequences dh 1 t 1 dh 2 t 2 ... and t 1 t 2 ... are called the timed trace and firing sequence (untimed trace) of ρ, respectively. The total elapsed time during the run ρ, denoted by time(ρ), is ∑

	s i	0
		i=1,|ρ|

  Table2reports the matrices L and L of the model TPN3 at Fig.3. For instance, the value 2 of l21 is a lower bound of the firing delay of t 2 , relatively to the firing date of t 1 , in case t 2 is not enabled when t 1 is fired. It corresponds to the potential situation where t 1 enables t 4 , which, in turn, enables t 2 (i.e., l21 = l 24 + l 41 = ↓ Is(t 2 ) + ↓ Is(t 4 )). Note that a lower bound of the enabling delay of t 2 relatively to the firing date of t 1 , in case t 2 is not enabled when t 1 is fired, is l21 -↓ Is(t 2 ) = 1.

  [START_REF] Belluomini | Timed state space exploration using POSETs[END_REF] Let N be a TPN with no unbounded static firing intervals. Then: G |= SC ⇒ the RSCG preserves non-equivalent sequences of the CSCG.Proof Let M be a marking and ω a firing sequence of M (i.e., M[ω >). The sequence ω of M is maximal iff it is infinite or leads to a deadlock marking. Let Ω (M) be a set of maximal firing sequences of M. The RSCG preserves the non-equivalent firing sequences of the CSCG if: ∀α

Table 3

 3 Some experimental results

	TPN	RSCG	RSCG'	CSCG	TPN	RSCG	RSCG'	CSCG
	KB(1)				KB(2)
	NSC	32	40	61	NSC	102135	? > 236977	? > 207685
	NCSC	38	54	107	NCSC	133764	> 457101	> 551187
	CPU (s)	0	0	0	CPU (s)	269	> 3600	> 3600
	HC(1)				HC(2)
	NSC	19	31	70	NSC	133	289	1743
	NCSC	18	33	110	NCSC	165	455	4603
	CPU (s)	0	0	0	CPU (s)	0	0	0
	HC(3)				HC(4)
	NSC	497	1714	23299	NSC	2895	11524	? > 138335
	NCSC	682	2633	84184	NCSC	4362	17279	> 590080
	CPU (s)	0	0	45	CPU (s)	0	14	> 3600
	HC(5)				HC(6)
	NSC	10239	75251	?	NSC	16846	? > 221731	?
	NCSC	16831	112606		NCSC	27210	> 338461
	CPU (s)	3	381		CPU (s)	9	> 3600
	FMS(2)				FMS(3)
	NSC	928	12668	82665	NSC	84176	? > 284319	? > 227052
	NCSC	1201	19337	233208	NCSC	109930	> 430854	> 618528
	CPU (s)	0	8	413	CPU (s)	170	> 3600	> 3600

Table 4

 4 Static firing intervals of HC,F MS and KB

	Is of HC	Is of FMS	Is of KB
	t 1 [1,2]	t p 1 [1,2]	tsynch4 -23[1,3]
	t 2 [2,3]	t p 2 [1,2]	tsynch1 -23[3,5]
	t 3 [3,3]	t p 3 [1,2]	tredo1[2,2]
	t 4 [1,1]	tm 1 [1,1]	tok1[3,4]
	t 5 [1,2]	tm 2 [3,4]	tback1[1,3]
	t 6 [1,2]	t p 3 m 2 [4,4]	tout1[3,5]
	t 7 [3,3]	t p 3 s[1,2]	tredo2[2,2]
	t 8 [2,2]	t p 1 m1[1,1]	tok2[3,4]
	t 9 [1,1]	t p 2 m 2 [3,3]	tback2[1,3]
	t 10 [1,1]

A 1-safe time Petri net is a 1-bounded time Petri net (i.e., each place can contain at most one token).

A maximal firing sequence is either infinite or finite ending up in a deadlock state (i.e., a state with no enabled transitions).

Two sequences ω and ω ′ are equivalent (denoted by ω ≡ ω ′ ) iff ω ′ can be obtained from ω by successive permutations of its transitions. By convention, it holds that ω ≡ ω ′ .

Transitions are non-related if no one is enabled by the others (i.e., no one is the parent of the others).

The symbol × is an optional separator between elements of M and their occurrence numbers.

An atomic constraint is a constraint of the form x ≺ c,-x ≺ c or xy ≺ c, where x,y are real-valued variables, ≺∈ {<,=,≤,≥,>} and c ∈ Q ∪ {∞,-∞} is a rational number

A triangular atomic constraint is an atomic constraint of the form xy ≺ c.

A simple atomic constraint is an atomic constraint of the form x ≺ c or -x ≺ c.

The canonical form of F ′ is the formula corresponding to the canonical form of its DBM.

http://mcc.lip6.fr

A free-choiceTPN is a TPN, where for every transition t, pre(t) ≤ P and post(t) ≤ P and the sets of input places of any pair of transitions are either equal or disjoint. In a strongly-connected TPN, there is a directed path between every two nodes (places or transitions).

In a connected TPN, there is an undirected path between every two nodes.

Formally, let α = (M, F) be a state class, D the canonical form of F (i.e., d i j = Max(t it j |F), for t i ,t j ∈ En(M)). The set G(α) is the smallest set of transitions of En(M) that satisfies all the following conditions: C0:

∈ CFS(t i ) ∨ d i j < 0. We denote by SC the conjunction C0 ∧C1 ∧C2 ∧C3.

Intuitively, C0 ensures that G(α) is empty only for deadlock state classes. This condition is necessary to preserve the deadlock property. Note that, for t i ,t j ∈ En(M), d i j ≥ 0 means that for some delay valuation of F, the firing delay of t i is larger or equal to the firing delay of t j . So, t j can be fired before t i from α or from a successor (direct / indirect) of α. In case d i j < 0, it means that t j cannot be fired before t i from α or from a successor (direct / indirect ) of α, unless t i is disabled by a conflicting transition. Condition C1 means that all firable transitions of G(α) are effect-independent of transitions Fr(α) -G(α) and not structurally in conflict with the transitions of En(M) -Fr(α) -G(α). Therefore, the firing of any transition of G(α) will not disable the transitions of En(M) -G(α) and vice-versa.

Condition C2 ensures that during the enabledness of any firable transition t i of G(α), no transition t j outside G(α) may enable directly/indirectly a transition t k that is structurally in conflict with t i and firable before t i (see Fig. 4). The precondition lk j ≤ d i j means that the firing delay of transition t k relatively to the firing date of t j can be smaller ou equal to the maximal delay between the firing dates of transitions t j and t i . In other words, after firing t j , t k can occur before t i . In case this precondition is not satisfied, it means that, after firing t j , t k cannot occur as long as t i is enabled. Conditions C1 and C2 imply that the enabledness of t i will not be affected by firing the transitions outside G(α).

Condition C3 prevents to loose sequences with no equivalent sequence starting with a transition of G(α) ∩ Fr(α). For instance, suppose that there is a maximal sequence ωt j of α s.t. all transitions of ω do not belong to G(α), t j belongs to G(α) -Fr(α) and is in conflict with all transitions of G(α). The firing of t j after ω disables all transitions of G(α). In case G(α) does not satisfy Condition C3, no sequence equivalent to ωt j is represented in the reduced graph. Otherwise, if t j is fired after ω, at least a transition t i of G(α) ∩ Fr(α) is still firable and not in conflict with t j . Therefore, sequences ωt j t i and ωt i t j are both firable from α. Conditions C1, C2 and C3 ensure that t i ωt j is also firable from α. As we will show, they also ensure that succ G handles all equivalent sequences resulting from permuting transitions of G(α) with the other firable transitions.