Pierre-Alain Bourdil
email: pierre-alain.bourdil@eurogiciel.fr

Bernard Berthomieu
email: bernard.berthomieu@laas.fr

Silvano Dal Zilio
email: silvano.dalzili@laas.fr

François Vernadat
email: francois.vernadat@laas.fr

Silvano Dal

Symmetry Reduction for Time Petri Net State Classes

Keywords: Time Petri Nets, State Classes, Symmetry Reduction

We propose a method to exploit the symmetries of a real-time system represented by a Time Petri net for its verification by model-checking. The method handles both markings and timing constraints; it can be used in conjunction with the widely used state classes abstraction, a construction providing a finite representation of the behavior of a Time Petri net preserving its markings and traces. The approach has been implemented and experiments are reported.

Introduction

Symmetry reduction aims at exploiting the symmetries of a system in order to explore its state space more efficiently. Instead of enumerating all the reachable states, one enumerates equivalence classes of states w.r.t. the symmetry relation. When applications have some symmetric structure-and large applications typically have-this provides an effective way to fight combinatorial explosion.

The idea of exploiting symmetries can be traced back to studies in program verification and analysis of high-level Petri nets. Symmetry reduction has been used since in a variety of contexts and a number of tools support symmetries, whether inferred or structural, including e.g. [START_REF] Ip | Systems with Replicated Components in Murϕ[END_REF][START_REF] Chiola | Manual and Automatic Exploitation of Symmetries in SPN Models[END_REF][START_REF] Sistla | SMC: A Symmetry-Based Model Checker for Verification of Safety and Liveness Properties[END_REF][START_REF] Schmidt | LOLA A Low Level Analyser[END_REF]. Symmetry reduction can be further combined with other reduction techniques, such as stubborn sets or covering steps. Combining symmetries with symbolic analysis based on decision diagrams has been investigated for some models [START_REF] Clarke | Exploiting Symmetry in Temporal Logic Model Checking[END_REF] but, in spite of some results, they seem harder to accommodate with such approaches than with enumerative methods.

In this paper, we propose a symmetry reduction method for a state space abstraction technique for real-time models with dense time semantics, the State Class Graph (SCG) construction for Time Petri nets [3,[START_REF] Berthomieu | Modeling and Verification of Time Dependent Systems Using Time Petri Nets[END_REF]. Time Petri nets [START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF] (TPN for short) are a widely used model for analysis of real-time systems. Time Petri nets enrich Petri nets with time intervals associated with the transitions of the net. These intervals specify the possible time delays between last enabledness of the transitions and their activation. Time Petri nets have been used for a variety of verification tasks, including model checking, scheduling analysis or evaluation [START_REF] Bucci | Compositional validation of time-critical systems using communicating time petri nets[END_REF][START_REF] Vicario | Static Analysis and Dynamic Steering of Time-Dependent Systems[END_REF][START_REF] Lime | Romeo: A parametric model-checker for petri nets with stopwatches[END_REF] in a variety of application domains like communication protocols, real-time systems, biochemical networks, etc. Compared to the prominent model of Timed Automata, bounded TPN have the same expressiveness in terms of timed language acceptance, but are less expressive in terms of timed bisimulation [START_REF] Bérard | Comparison of the expressiveness of timed automata and time petri nets[END_REF], unless enriched with priorities [START_REF] Berthomieu | Bridging the Gap Between Timed Automata and Bounded Time Petri Nets[END_REF]. They benefit of well established analysis methods, based for most on the state class construction of [3], and of several mature tools [START_REF] Berthomieu | The tool TINA -Construction of Abstract State Spaces for Petri Nets and Time Petri Nets[END_REF][START_REF] Gardey | Romeo: A tool for analyzing time petri nets[END_REF][START_REF] Bucci | Oris: a tool for modeling, verification and evaluation of real-time systems[END_REF].

TPN can be interpreted over discrete time or over dense time. While symmetry reduction of discrete Time Petri nets can be seen as a straightforward extension of symmetry reduction of (untimed) Petri nets (it was available in the INA tool [START_REF] Starke | INA: Integrated Net Analyzer[END_REF]), symmetry reduction for dense time Time Petri nets is more challenging. When interpreted over dense time, state spaces are typically infinite and finite representations are obtained through time abstractions. The time information is typically represented by systems of difference constraints with their variables associated with the transitions of the net. Some results are available on symmetry reduction for Timed Automata [START_REF] Hendriks | Adding Symmetry Reduction to Uppaal[END_REF][START_REF] Wang | Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures[END_REF], but none is available so far for dense time Time Petri nets.

Our contributions. We have developed and implemented a symmetry reduction technique for the most commonly used state space abstraction for Time Petri nets, known as the state classes construction. First, we make some technical contributions, with the definition of a total order relation between symmetry equivalent transitions (Section 5) that relies on an invariant on the systems of difference constraints capturing time information. A second, more practical, contribution is a high-level structural approach for declaring the symmetries of a net (see Section 4) in a way enabling efficient (polynomial) computation of canonical representatives for state classes, using the previous ordering.

Outline of the paper. We start with some information on Time Petri nets and their analysis techniques. In Section 3, we extend the symmetry reduction approach for Petri nets to dense-time Time Petri nets. Our approach to symmetry reduction of TPN is presented in Section 4; it describes a compositional method to build large nets from smaller components, together with their symmetries, associated with a method for computing state class representatives. The main technical result of the paper is found in Section 5, a total order between symmetry equivalent state classes. Section 6 presents a preliminary implementation of our method integrated into the Tina toolbox [START_REF] Berthomieu | The tool TINA -Construction of Abstract State Spaces for Petri Nets and Time Petri Nets[END_REF] and some experimental results. Some possible extensions of this work are discussed in the conclusion.

Time Petri nets

A Time Petri net [START_REF] Merlin | A Study of the Recoverability of Computing Systems[END_REF] (or TPN) is a Petri net in which transitions are decorated with time intervals that constrain the time a transition can fire.

Let II be the set of non-empty real intervals with their endpoints in IN∪{∞}. A TPN is a tuple P, T, Pre, Post, m 0 , I s in which:

• P, T, Pre, Post, m 0 is a Petri net, with P the set of places, T the set of transitions, m 0 : P → IN the initial marking, and Pre, Post : T → P → IN the precondition and postcondition functions.

• I s : T → II is a function called the static interval function.

For additional modeling expressiveness, Time Petri nets can be enriched with inhibitor arcs and read arcs (testing absence or presence of tokens in a place, respectively), preemption, priorities or external synchronized data processing.

Semantics

A marking is a function m : P → IN. A transition t ∈ T is enabled at m iff m ≥ Pre(t) (we use the pointwise comparison between functions). We denote E N (m), or simply E(m) when N is clear from context, the set of transitions enabled at m in net N .

A state of a TPN is a pair s = (m, I) in which m is a marking and I : T → II is a partial function, called the (dynamic) interval function, that associates a temporal interval with every transition enabled at m. For i ∈ II, ↓i denotes its left end-point, and ↑i its right end-point or ∞ if i is unbounded. For any θ ∈ IR ≥ , let i .

-

θ = {x -θ|x ∈ i ∧ x ≥ θ}.
Definition 1. The semantics of a TPN P, T, Pre, Post, m 0 , I s is the timed transition system SG = S, s 0 , → where:

• S is the set of states of the TPN;

• s 0 = (m 0 , I 0 ) is the initial state, where m 0 is the initial marking and I 0 is the static interval function restricted to the transitions enabled at m 0 ;

• → ⊆ S × (T ∪ IR ≥ ) × S is the state transition relation; (s, a, s ) ∈ → is written s a -→ s .
For any t ∈ T and θ ∈ IR ≥ , we have:

(i) (m, I) t -→ (m , I ) iff: 1) t ∈ E(m) 2) m = m -Pre(t) + Post(t) 3) 0 ∈ I(t) 4) (∀k ∈ E(m ))((A(k) ∧ I (k) = I(k)) ∨ (¬A(k) ∧ I (k) = I s (k)))
where

A(k) = k = t ∧ k ∈ E(m -Pre(t)) (ii) (m, I) θ -→ (m, I ) iff: 5) (∀k ∈ T )(m ≥ Pre(k) ⇒ θ ≤ ↑I(k) ∧ I (k) = I(k) . -θ)
The state transitions labeled over T (case (i) above) are the discrete transitions, those labeled over IR ≥ (case (ii)) are the continuous, or time elapsing, transitions. A net transition t may fire from (m, I) if t is enabled at m and firable instantly (0 ∈ I(t)). In the target state, the transitions k that remained enabled while t fired (t excluded) retain their intervals. Such transitions k are said to be persistent (w.r.t. t, m, if not clear from context). The remaining transitions, among those enabled at m , are associated with their static intervals, they are said to be newly enabled (w.r.t. t, m). A continuous transition by θ is possible from (m, I) if and only if θ is not larger than ↑I(k) for any transition k ∈ E(m).

Because there may be an infinite number of continuous transitions, the state spaces of TPN are generally infinite, even when the net is bounded (its set of reachable markings is finite). To model check them, one needs finite abstractions of the state graphs. Definition 1 gives a dense time semantics to Time Petri nets. TPN can also be given a discrete time semantics by enforcing θ ∈ IN in continuous transitions.

Finally, TPN states (whether in dense or discrete time) can be defined in terms of clock functions instead of firing interval functions, the clock of a transition being the time elapsed since it was last newly-enabled. Clock functions γ may be used to denote interval functions, since we have at any state

I(t) = I s (t) .
-γ(t), but the mapping is only surjective: when I s (t) is unbounded, several γ(t) may obey that equation.

The State Class Abstraction

The State Class Graph (SCG for short) is a finite abstraction of the state graph SG that abstracts time elapsing transitions but preserves its markings and traces; the SCG embeds the reachability graph of the TPN.

The temporal information in states can be conveniently seen as firing domains rather than interval functions: the firing domain associated with interval function I is the set of real vectors {φ|(∀i)(φ i ∈ I(i))} (φ i is the coordinate of φ associated with transition i).

The State Class Graph construction of [3,[START_REF] Berthomieu | Modeling and Verification of Time Dependent Systems Using Time Petri Nets[END_REF] defines inductively a set of classes C σ , where σ ∈ T * is a sequence of discrete transitions firable from the initial state. Intuitively, the class C σ collects the states reachable after firing the sequence σ, abstracting delays. State classes are represented by pairs (m, D), where m is a marking and the firing domain D is described by a finite system of linear inequalities. We say that two Algorithm 1 (Construction of the SCG [3]). The SCG is the set of classes (C σ ) σ∈T * obtained as follows:

• The initial class C is (m 0 , D 0 ), where D 0 is the domain defined by the set of inequalities {↓I s (t)

≤ φ t ≤ ↑I s (t) | t ∈ E(m 0 )}.
• If σ is firable and C σ = (m, D), then:

-σ.t is firable iff:

1. m ≥ Pre(t) (t is enabled at m) 2. system D ∧ F is satisfiable, where F = {φ t ≤ φ i | i = t ∧ i ∈ E(m)} -C σ.t = (m , D ) where m = m -Pre(t) + Post(t)
D is obtained from D in three steps:

1. The above conditions F are added to D; 2. For each k enabled at m a new variable φ k is introduced, obeying:

φ k = φ k -φ t if k persistent w.r.t. t, m ↓I s (k) ≤ φ k ≤ ↑I s (k) otherwise 3.
Variables φ i are eliminated (using e.g. Fourier-Motzkin elimination).

The firing domains obtained by Algorithm 1 can be represented by systems of difference constraints, or difference systems for short, that is sets of inequalities of the form α i ≤ x i , x i ≤ β i or x i -x j ≤ γ i,j , where α i , β i and γ i,j are bounds, associating a rational constant with a comparison operator in {≤, <, ≥, >}. Such systems, often represented by Difference Bound Matrices, admit canonical forms that can be computed in polynomial time (see e.g. [START_REF] Ramalingam | Solving Difference Constraints Incrementally[END_REF]).

The SCG is certainly the best known and most widely used state space abstraction for Time Petri nets. It is finite if and only if the TPN admits a finite number of reachable markings, and it preserves both the markings and traces of the net [3,[START_REF] Berthomieu | Modeling and Verification of Time Dependent Systems Using Time Petri Nets[END_REF] and so is suitable for Linear Time Temporal Logic (LT L) model checking.

If only marking reachability properties are of interest, instead of the SCG one may use a typically coarser abstraction referred to here as SCG ⊆ [START_REF] Berthomieu | State Space Abstractions for Time Petri Nets. Handbook of Real-Time and Embedded Systems[END_REF]. Let us say that class (m, D) is included in class (m , D ) when m = m and the solution set of D is included in that of D . The SCG ⊆ is built like the SCG, except that classes related by inclusion are merged; this coarser construction preserves markings but over-approximates traces.

In the remainder of the text, we simply use the name of the transition, say t, as a shorthand for the firing domain variable φ t associated with transition t.

Symmetry Reduction of TPN

Symmetries in state classes graphs

This section defines symmetries on Time Petri nets and state class graphs. The terminology and Theorem 1 are straightforwardly adapted from [START_REF] Starke | Reachability Analysis of Petri Nets using Symmetries[END_REF][START_REF] Schmidt | How to Calculate Symmetries of Petri Nets[END_REF]. Definition 2. A symmetry of a TPN P, T, Pre, Post, m 0 , I s is a permutation π of P ∪ T that preserves node types, preconditions, postconditions and static intervals. That is:

1. (∀x)(x ∈ P ⇔ π(x) ∈ P ) 2. (∀t, p)(Pre(t)(p) = Pre(π(t))(π(p))) 3. (∀t, p)(Post(t)(p) = Post(π(t))(π(p))) 4. (∀t)(I s (t) = I s (π(t)))
The set S N of all symmetries of TPN N forms a group under function composition. Recall that TPN states are pairs (m, I) where m is a marking and I is an interval function. Given a symmetry π of a TPN, let us define:

• the action π(m) of π on m by (∀p ∈ P )(π(m)(p) = m(π -1 (p)))
• the action π(I) of π on I by (∀t ∈ T )(π(I)(t) = I(π -1 (t)))

• the action π(m, I) of π on a state (m, I) by π(m, I) = (π(m), π(I)).

The symmetries of a TPN induce symmetries of its state space: Lemma 1. Let N be a TPN and SG = S, s 0 , → its state graph. Let π be some symmetry of N . Then for all t, θ, m, m , I, I :

1. (m, I) t -→ (m , I ) ⇔ π(m, I) π(t) -→ π(m , I ) 2. (m, I) θ -→ (m , I ) ⇔ π(m, I) θ -→ π(m , I ) Proof.
1. We have to prove that conditions 1 to 4 in Def. 1 are preserved by application of a net symmetry. For conditions (1) and (2), this is proved in [START_REF] Starke | Reachability Analysis of Petri Nets using Symmetries[END_REF] (Lemma 1). For (3) and (4), similarly, this is straightforward from the definitions of actions. 2. From [START_REF] Starke | Reachability Analysis of Petri Nets using Symmetries[END_REF] we have: (∀k)(m ≥ P re(k) ⇔ π(m) ≥ P re(π(k))), and then from the definition of actions, π(I)(π(k)) = I(k) for any I and k. Hence (2) holds.

Two states s and s are equivalent with respect to S N , written s ≈ s , iff there is a symmetry π ∈ S N such that π(s) = s . Relation ≈ is an equivalence relation; the equivalence class of any s by ≈ is finite and is called the orbit of s. Orbits of places and orbits of transitions are defined similarly.

For model checking purposes, defining symmetry reduction on states would be of little help since TPN typically have an infinite number of states. Fortunately, Lemma 1 carries over to the state class abstraction of TPN.

If π is a TPN symmetry, we define π(D) as the set of solutions of D in which each variable t is replaced by π

(t). Likewise the action π(m, D) of π on a class (m, D) is defined by π(m, D) = (π(m), π(D)) and state class equivalence by (m, D) ≈ (m , D ) ⇔ (∃π ∈ S N )(π(m, D) = (m , D )).
Let SCG ≈ denote the state class graph built like the SCG in Algorithm 1, but retaining only one state class per orbit. A marking m is symmetric iff (∀π ∈ S N )(π(m) = m). The following theorem shows how symmetries help reachability analysis of TPN by the state classes method: Theorem 1. Assume π is a symmetry of a TPN. Then for all t, m, m , D, D :

1. (m, D) t -→ (m , D ) ⇔ π(m, D) π(t) -→ π(m , D ) 2. if m 0 is symmetric, then for any state class C: C ∈ SCG ⇔ (∃C * ∈ SCG ≈ )(C ≈ C * )
Proof.

(1) directly follows from the definition of actions on state classes. ( 2) is proved by induction on the firing sequences of the SCG.

Applying Symmetry Reduction

There are two main issues to be solved when trying to put symmetry reduction to work: identifying the symmetries of the model (the TPN here) and deciding when two states (state classes here) are equivalent. Detecting symmetries: detecting net symmetries amounts to compute all net automorphisms, a problem known to be at least as hard as the graph isomorphism problem [START_REF] Schmidt | How to Calculate Symmetries of Petri Nets[END_REF]. For this reason, many implementations of symmetry reduction rely on some static symmetry information provided by the user. Murϕ [START_REF] Ip | Systems with Replicated Components in Murϕ[END_REF], for instance, makes use of a dedicated "scalarset" type, also used in [START_REF] Hendriks | Adding Symmetry Reduction to Uppaal[END_REF]. In high level Petri nets, symmetries are deduced from the syntax of inscriptions. On the other hand, some tools [START_REF] Schmidt | LOLA A Low Level Analyser[END_REF] compute these automorphisms from nets automatically with acceptable performances on average.

In our implementation, described in Sections 4 and 6, nets are described hierarchically as compositions of smaller nets, the composition operators specifying both the architecture of the net and a symmetry. Checking state equivalence: There are basically two methods for checking equivalence ≈ on states (or state classes here): comparing a new state for ≈ pairwise with all computed states, or computing from the state a representative state and storing only these.

In [START_REF] Schmidt | How to Calculate Symmetries of Petri Nets[END_REF][START_REF] Schmidt | Integrating Low Level Symmetries into Reachability Analysis[END_REF], three implementations of equivalence checking are discussed. All assume that the symmetry group is available, but no particular structure is assumed for it; all symmetries are handled uniformly. The first method, referred to as "iterating the symmetries", amounts to applying all possible symmetries to the new state and to check if the result state has been stored yet. The set of symmetries to be applied is reduced thanks to particular representations of symmetries and of the set of stored states. The second method, "iterating the states", amounts to find a symmetry such that applying it to some stored state yields a state equal to the new state. The method relies on so-called symmetrypreserving hash functions. A third method relies on state representatives; it takes advantage of the same representation of symmetries as the first method to find a minimal form for the new state. The minimal states computed are not necessarily canonical though; there may be several representatives per state orbits. The work presented in [START_REF] Junttila | New Canonical Representative Marking Algorithms for Place/Transition-Nets[END_REF] builds upon these algorithms and proposes some improvements. The experiments discussed in [START_REF] Junttila | New Canonical Representative Marking Algorithms for Place/Transition-Nets[END_REF] suggest that the third algorithm typically yields the best results.

On the other hand, the methods relying on scalarsets [START_REF] Ip | Systems with Replicated Components in Murϕ[END_REF][START_REF] Hendriks | Adding Symmetry Reduction to Uppaal[END_REF] or similar structural techniques trade generality for efficiency. Scalarsets may only express particular groups of symmetries, typically full symmetries in systems of processes (those resulting from all process permutations). As a consequence, canonical representatives can be efficiently computed for states.

Among the methods proposed in [START_REF] Schmidt | How to Calculate Symmetries of Petri Nets[END_REF][START_REF] Schmidt | Integrating Low Level Symmetries into Reachability Analysis[END_REF], the first two would be applicable to state classes as well since they only require to be able to compare states for equality; this is yet unclear for the third method which relies on a total ordering of states. But these methods do not obviously lead to efficient implementations; this is substantiated by our experimental data in Section 6. Though technically different, our reduction technique is closer to those relying on scalarsets; the symmetries are declared, and restricted to those admitting a polynomial time algorithm for computing canonical representatives (see e.g. [START_REF] Donaldson | On the Constructive Orbit Problem[END_REF]). The approach is presented in the next section.

Describing symmetries compositionally

Large systems are typically built by assembling components, possibly replicated. Replication typically induces symmetries of their state spaces [START_REF] Miller | Symmetry in temporal logic model checking[END_REF][START_REF] Wahl | Replication and abstraction: Symmetry in automated formal verification[END_REF]. We wish to take advantage of the structure of a net, made explicit by construction, to compute and handle the symmetries of its state space.

In our approach, nets are described hierarchically as compositions of smaller nets. Symmetries are introduced by adhoc composition operators. Each builds a net from a replicated component and simultaneously specifies a component symmetry. The approach is presented in this section and illustrated in Section 6.

Decomposition and composition of TPN

Petri nets based models admit several natural decomposition into subnets. Nets can be decomposed from a partition of their places, or of their transitions, or of their arcs. We use the first form; from a partition of places: the subnet, or component, defined by block b of the partition is constituted of the places in b, their adjacent arcs, and the transitions connected to these arcs. Transitions may occur in several components (with their Pre and Post functions spread among these) while each place may only occur in a single component;

The corresponding composition operator is the synchronized product of nets, reviewed in the sequel. Synchronized products are pervasive in the study of formal models for concurrency (e.g. Process calculi, networks of automata, etc); for Petri nets, it was introduced in [START_REF] Hack | Petri net languages[END_REF]. For easing the specification of synchronizations among components, the transitions of nets are assumed to be labeled over an alphabet of actions Σ = Σ ∪ { }, with ∈ Σ. Σ is the set of visible, or observable, actions; is the silent, or internal, action.

Definition 3 (Labeled Petri net).

A labeled Petri net is a tuple P, T, Pre, Post, m 0 , Σ , L in which:

• P, T, Pre, Post, m 0 is a Petri net, • Σ = Σ ∪ { } is a finite alphabet of actions, with ∈ Σ.
• L : T → Σ is a function called the Labeling function.

Definition 4 (Synchronized product). Consider two labeled Petri nets not sharing any place or transition:

N 1 = P 1 , T 1 , Pre 1 , Post 1 , m 0 1 , Σ 1 , L 1 and N 2 = P 2 , T 2 , Pre 2 , Post 2 , m 0 2 , Σ 2 , L 2 .
Their synchronized product N 1 | N 2 is the net N = P, T, Pre, Post, m 0 , Σ , L obtained as follows:

• P = P 1 ∪ P 2 • m 0 (p) = if p ∈ P 1 then m 0 1 (p) else m 0 2 (p) • Σ = Σ 1 ∪ Σ 2 • For each i ∈ {1, 2}, T contains all transitions t ∈ T i such that L i (t) ∈ Σ 1 ∩ Σ 2 , with:
For each p ∈ P :

Pre(t)(p) = if p ∈ P i then Pre i (t)(p) else 0 Post(t)(p) = if p ∈ P i then Post i (t)(p) else 0 L(t) = L i (t) For each (t 1 , t 2 ) ∈ T 1 × T 2 such that L 1 (t 1 ) = L 2 (t 2 ) =
, T contains a transition, referred to as (t 1 , t 2 ), with:

For each p ∈ P :

Pre((t 1 , t 2 ))(p) = if p ∈ P 1 then Pre 1 (t 1 )(p) else Pre 2 (t 2 )(p) Post((t 1 , t 2 ))(p) = if p ∈ P 1 then Post 1 (t 1 )(p) else Post 2 (t 2 )(p) L((t 1 , t 2 )) = L 1 (t 1 )
T contains no other transitions than those specified above.

Product | is commutative and associative; it is also compositional (the semantics of a product of nets is obtained from the semantics of its constituents). It can be extended to TPN [START_REF] Berthomieu | Bridging the Gap Between Timed Automata and Bounded Time Petri Nets[END_REF].

A language for building nets from components. A net with no particular structure made explicit, holding at least a place and its connected edges and transitions, or a single transition, is called a basic net. Our nets will be built, hierarchically, as synchronized products (denoted |) from basic nets. For convenience, a relabeling operator allowing to hide or change the label of some transitions may be provided (as in the CCS process calculus, for instance), as well as derived product forms like free products or iterated products replicating a component before composing the copies.

Such a language of net expressions has been available for a long time in the tool Tina [START_REF] Berthomieu | The tool TINA -Construction of Abstract State Spaces for Petri Nets and Time Petri Nets[END_REF]. Examples of nets built this way will be given in Section 6. We discuss now the introduction of symmetries in our language of components.

Describing nets together with their symmetries

Nets built from replicated components typically exhibit symmetries. Consistently with our structural description of nets, we want to declare component symmetries when building nets rather than computing net symmetries afterwards. This will be done by enriching our language of net operators by specific operators for the most common kind of symmetries (full symmetries, circular symmetries, cube symmetries, for instance). These operators will work as iterators replicating a component, and simultaneously enforcing a symmetry among the copies, resulting in a net together with a description of its symmetries.

The approach is discussed in [START_REF] Bourdil | Contribution à la modélisation et la vérification formelle par model-checking-Symétries pour les Réseaux de Petri Temporels[END_REF] in a general setting. In this paper, and for the purpose of illustrating our symmetry reduction method for Time Petri nets, we will use here a simplified version. The simplification consists of limiting the symmetry declarations to full symmetries and cyclic symmetries and, for full symmetries, preventing synchronizations between the components involved. An additional restriction on products will be made precise shortly.

The previous net expressions are enriched with two operators: P ool and Ring. Both take an arity n and a net C as parameters: P ool(n, C) stands for the free product of n independent copies of net C with the symmetries resulting from transpositions of the pool components -Ring(n, C) stands for the synchronized product of n copies of C after a conventional renaming of transitions ensuring synchronization of a ring element with its neighbors. The symmetries are those resulting from cyclic permutations of the ring components.

Our enriched language of net expressions is thus (|| || || stands for the free product and Θ Θ Θ is an unspecified family of relabeling operators): Such expressions simultaneously describe a net and its group of symmetries, compositionally. In synchronized products of nets, we will assume the additional restriction, easily checked statically, that one transition at least in each pair of transitions synchronized must be invariant under the action of the symmetries of its component. Then, the group described can be built in terms of cyclic groups, symmetric groups, disjoint products of groups and wreath products of groups. These group constructions all belong to the so-called easy groups [START_REF] Clarke | Symmetry Reductions in Model Checking[END_REF]; computing canonical representatives for their elements can be done in polynomial time.

Compared to the treatment of Lola [START_REF] Schmidt | LOLA A Low Level Analyser[END_REF], for instance, our nets will only exhibit the symmetries declared, while Lola will compute all symmetries. But Lola fails to capture the structure of the group of symmetries, which prevents application of efficient reduction techniques known for some particular groups. The benefits of the knowledge of the group structure will be clear from the experiments presented in Section 6, which include a comparison of our reduction results with those obtained by Lola.

Checking marking equivalence in Petri nets

Our approach for checking state equivalence relies on canonical representatives for states, and specifically in computing the lexicographically least elements of state orbits [START_REF] Clarke | Symmetry Reductions in Model Checking[END_REF]. For the Petri nets described as in Section 4.2, we could proceed as follows; the treatment is extended to Time Petri nets afterward.

The states of a Petri net are its markings; transitions express state changes but do not contribute themselves to the state information. Computing canonical representatives for marking, modulo the symmetries considered, can be done in polynomial time; canonization of a marking m is performed recursively from the group description derived for the net:

-For symmetric groups (pools): By construction, components are disjoint (do not interact) and isomorphic since obtained by replication. All place and transition orbits are of size n (the number of components involved in the pool). Clearly then, the pool marking m can be represented by a matrix in which column i holds the markings of the places in component i and line j holds the markings of all places in some place orbit j.

Then, the canonical representative for marking m represented this way is obtained by sorting its columns lexicographically (that is by sorting the local states [START_REF] Clarke | Symmetry Reductions in Model Checking[END_REF]). The component permutation that sorts the columns defines a symmetry π of the net; the canonical representative of m is π(m). One can always find an ordering on the places of the net such that the representatives are the least markings in their orbits.

-For cyclic groups (rings): Even though the ring components interact, they are still isomorphic, so we can use for markings the same matrix representation used for symmetric groups. Then, a cyclic permutation ρ of components (of the columns of the matrix M representing marking m) is computed that minimizes lexicographically the vector of columns of matrix M. The canonical representative of m is π(m), where π is the symmetry of the net corresponding with component permutation ρ.

-For products: Wreath products appear when a net with some symmetries declared is iterated in a pool or ring construction. With the hypotheses of Section 4.2, the symmetries of a product of nets, whether free or synchronized, results in a disjoint product of groups. Classically [START_REF] Clarke | Symmetry Reductions in Model Checking[END_REF], canonical representatives for elements of such groups are built from the canonical representatives of their constituents.

Checking state class equivalence in Time Petri nets

Time Petri nets are built using the same language of net expressions presented in Section 4.2. The information in state classes is richer than that captured by markings in Petri nets; states here are pairs (m, D), where m is a marking and D is a firing domain. Firing domains can be classically represented by so-called Difference Bound Matrices (DBM for short). The DBM of class (m, D) has size (n + 1) × (n + 1), where n is the number of transitions enabled at marking m.

A naive way to compute the canonical representative of a state class (m, D) would be to compute first a canonical representative for the marking and then one for the firing domain, represented by a DBM. For the marking, one can proceed as explained in Section 4.3. For the DBM, the problem is discussed in [START_REF] Hendriks | Enhancing uppaal by exploiting symmetry[END_REF] for the clock DBM of Timed Automata: DBM can be seen as adjacency matrices of some complete labeled digraphs; sorting DBM amounts to sort such graphs, a problem known to be equivalent to the graph isomorphism problem. So there is no hope to obtain an efficient canonization of state classes along this path.

Fortunately, we can abstract the information conveyed by firing domains in a way that allows computing representatives for state classes by a simple extension of the method used in Section 4.3 for markings. The method relies on a total order D between transitions that are equivalent by symmetry (are in the same orbit) and enabled at state class (m, D). A suitable order is developed in the next section; the idea is inspired by [START_REF] Hendriks | Adding Symmetry Reduction to Uppaal[END_REF] in which clocks of Timed Automata zones are compared using their last reset date. The handling of time in TA is quite different from that in TPN, however, and the zone constructions of TA significantly differ from the state class constructions of TPN, so we cannot reuse the clock order of [START_REF] Hendriks | Adding Symmetry Reduction to Uppaal[END_REF] and had to investigate a specific one for state classes.

Computing canonical representative for state classes. Given such an order, D , one can compute the canonical representative of class (m, D) as follows.

Recall that, in Section 4.3, markings were presented as matrices M such that column i is the local marking of component i and line j holds the marking of all the places in orbit j. Similarly, and for the same reasons (the components of a pool or ring are isomorphic), the set e of transitions enabled at some marking m (the time information in a state class is associated with these transitions only) can always be represented by a matrix E in which column i holds the transitions of component i, and all transitions in line j are in the same transition orbit.

Then, instead of simply comparing the columns of M as in Section 4.2, we compare lexicographically pairs (m i , e i ) in which m i (resp. e i ) is the i th column of M (resp. E). If the marking elements differ then we are done, otherwise we must compare the transition elements; these are compared with the lexicographic order on D . Sorting a state class (m, D) abstracted this way yields a permutation π of the net; the canonical representative of the class is π(m, D).

We now focus on the development of the total order D for a class (m, D).

Ordering State Classes

First, for any state class (m, D), we define a total order relation D between transitions enabled at m and equivalent by symmetry (≈). Afterwards, this relation is used to define a total order between equivalent state classes.

Intuitively, we will have t D t if the transition t stayed enabled longer than t (since their last enabling date) in the execution that led to class (m, D). However, the information on the last enabling date of a transition cannot be reconstructed from the firing domain of a class, which mandates several technical results to define the ordering relation. Ultimately, the definition of D will be based on an invariant on firing domains. This is the goal of Section 5.2.

Closure Form of Firing Domains

The firing domains computed during the SCG construction (see Algorithm 1) can always be written in a standard form, as follows. For every pair of transitions t, t that are enabled in a class (m, D), we have the following inequalities in D:

α t ≤ t ≤ β t and t -t ≤ γ t,t (t = t )
The bounds α t , β t and γ t,t exactly define the domain D (a class with n enabled transitions has n • (n + 1) bounds). Also, by construction, when t is newly enabled in the class (m, D), we have α t = ↓I s (t) and β t = ↑I s (t). These are the static timing constraints for t; we use the notation α s t and β s t for these values afterward.

We can improve the standard form of D by choosing in the above representation the tightest possible bounds preserving the associated solutions set. In this case we say that D is in closure form. The closure form provides a normal form for firing domains. Indeed, two domains are equal if and only if they have the same closure form. Another advantage of using closure forms for representing class domains is that they can be computed incrementally with O(n 2 ) complexity; Lemma 2 below is proved in [START_REF] Boucheneb | Analyse des Réseaux Temporels: Calcul des Classes en O(n 2 ) et des Temps de Chemin en O(m × n)[END_REF].

β i = β s i if i newly enabled, β i = γ i,t otherwise α i = α s i if i newly enabled, α i = max(0, -min k∈E(m) (γ k,i )) otherwise γ i,j = β i -α j if i or j newly en., γ i,j = min(γ i,j , β i -α j ) otherwise
We can use this incremental construction to derive invariants on the coefficients of the firing domains when in closure form. Lemma 3. For any class C = (m, D) with D in closure form, and for any transitions i, j, k enabled at m, we have:

1. γ i,j ≤ β i -α j 4. γ i,j ≤ γ i,k + γ k,j 2. β i ≤ γ i,j + β j 5. 0 ≤ α i ≤ α s i 3. α i ≤ γ i,j + α j 6. 0 ≤ β i ≤ β s i 7. if C = (m , D ) is obtained from C by firing some transition, then β i ≤ β i
Proof. 1-4 follow from the fact that D is in closure form (bounds are tight). 5-7 are proved by induction on firing sequences using Lemma 2.

A Total Order on Equivalent Transitions

We prove a general invariant on firing domains in closure form, obtained during the SCG construction. This property makes explicit a relation between transitions that have the same static timing constraints (α s and β s ), which is necessarily the case for equivalent transitions (symmetries must preserve static intervals).

We say that two transitions i and j are equivalent for D, denoted i = D j, if and only if, when transposing the transitions i and j in the system of difference constraints D, we obtain a system D that has the same solution set. Lemma 4. If D is in closure form then i = D j if and only if α i = α j , β i = β j , γ i,j = γ j,i and for all transitions k distinct from i, j,

(γ i,k = γ j,k ∧ γ k,i = γ k,j ).
Our next property states a similar result for an ordering relation instead of an equivalence. Assuming i = j, we say that i is before j, written i D j, as follows:

i D j = def γ i,j ≤ γ j,i ∧ (∀k = i, j)(γ i,k ≤ γ j,k ) ( -DEF)
Lemma 5. Assume (m, D) is a class obtained in the SCG construction and i, j are two transitions with the same static time interval ( I s (i) = I s (j)). Then i D j implies α i ≤ α j , β i ≤ β j and for all transitions k distinct from i, j, γ k,j ≤ γ k,i .

Proof. (full proof in Appendix) Lemma 5 is pictured in Figure 1 on a domain represented by a DBM. It says that if i and j have equal static intervals then the circled relations imply the boxed relations. The proof is by case analysis and induction on the firing sequence leading to (m, D), using Lemmas 2 and 3.

A simple corollary of Lemma 5 is that the relation D is antisymmetric for every pair of equivalent transitions: we have that i D j and j D i implies i = D j. Next, we show that the relation is also total. We can extend the D relation to the whole set of transitions (not only the enabled ones) by defining that i D j whenever i is not enabled. Lemma 6. Assume (m, D) is a class obtained in the SCG construction and i, j are two transitions enabled at m with the same static time interval ( I s (i) = I s (j)). Then either i D j or j D i .

Proof. (full proof in Appendix) By case analysis. We have three cases to consider. The first is when both transitions i and j are newly-enabled in (m, D) (they were introduced simultaneously). It directly follows from Lemma 2. The second is when one is persistent and the other is newly-enabled. It directly follows from Lemmas 3 and 2. The last case is when both are persistent. It is proved by induction by showing that the ordering between i and j is preserved whatever the transition introduced next as long as both i and j stay persistent.

k j i l 0 β k β j β i β l × 0 γ k,l γ j,l γ i,l × -α l l γ k,i γ j,i × γ l,i -α i i γ k,j × γ i,j γ l,j -α j j × γ j,k γ i,k γ l,k -α k k ≥ ≥ ≥ ≥ ≥ ≥ ≥

A Total Order on Equivalent State Classes

Our results from Section 5.2 show that the relation D totally orders equivalent transitions. Checking i D j at a state class (m, D) has quadratic time complexity in the number of transitions enabled at m.

We take advantage of this relation to derive an order between equivalent state classes. We say that a symmetry π is stable for a marking m (resp. for a class (m, D)) if π(m) = m. Let C = (m, D) be some state class of the SCG. If π is stable for C, then the class π(C) = (m, π(D)) is also a class of the net and the firing domain π(D) has the same "variables" as D, but each transition i in D is changed into π(i).

By definition of the relation D (see equation -DEF), it is easy to see that i D j if and only if π(i) π(D) π(j). We use this property to define an order relation T between the firing domains obtained as the result of applying some symmetry to domain D (such domains will be said to have the form π(D)).

We assume an arbitrary, total ordering ≤ T over the transitions in T . For any given permutation π stable for m we say that D T π(D) if and only if D = π(D) (that is t = D π(t) for all t in E(m)) or for the first transition t such that t = D π(t), we have t D π -1 (t):

D T π(D) = def (D = π(D)) ∨ (∃t) t ≺ D π -1 (t) ∧ (∀k < T t)(k = D π(k))
The relation T is analog to the lexicographic order built from ≤ T and D , but our definition has the advantage to work with any domains of the form π(D). Relation T is a total order between equivalent firing domains.

Next, assuming a total ordering ≤ P over places P , we can easily build a total order P over markings.

From T and P we now define a total order between equivalent classes. Two classes C and C are equivalent if there is a symmetry π of the net such that C = π(C). We say that (m, D) π(m, D) if m P π(m) or m = π(m) ∧ D T π(D) (that is is a lexicographic order). We can observe that comparing firing domains is conceptually far more complex than comparing markings, because relation D is tied to a particular domain whereas for markings we can merely use the comparison between integer tuples. Theorem 2. Let C = (C σ ) σ∈T * be the set of classes in the SCG construction of a TPN. Then relation is a total order between state classes equivalent for ≈ in C.

We have been very careful in our definitions of T and to avoid any reference to a particular implementation of symmetries. Hence our results can hold for different design choices.

6. An implementation

Computing experiments

The symmetry reduction method described in Section 4, relying on the ordering defined Section 5 when applied to TPN, has been implemented in an extension of Tina2 , an existing toolbox for analysis of Time Petri nets and various extensions [START_REF] Berthomieu | The tool TINA -Construction of Abstract State Spaces for Petri Nets and Time Petri Nets[END_REF].

We report some experiments on a train-gate controller model, in both timed and untimed versions, and on an example with compound symmetries. The nets are built with the language of net expressions with symmetries introduced in Section 4. The timed version of the train-gate controller model is taken verbatim from [START_REF] Berthomieu | State Class Constructions for Branching Analysis of Time Petri Nets[END_REF]. The untimed version is a slightly simplified version of a model found in [START_REF] Pommereau | Algebras of coloured Petri nets[END_REF]. In both cases the net models a level crossing: a number of tracks cross a road, protected by a gate; when approaching and leaving the road the trains trigger a signal sent to a controller that raises or lowers the gate as necessary. The safety property to be ensured is, of course, that the gate is closed whenever a train is crossing the road. In the timed version, this is ensured by time constraints on the relevant events, while the untimed versions makes use of signal acknowledgments and a shared green flag. In each case, the model is obtained by synchronizing a gate model (right), a controller (middle) and a pool of tracks. The timed model is represented in Figure 3 and the untimed one in Figure 2. The unit of time in all tables is the second of CPU time on a typical workstation. The results on the untimed models are shown in Figure 2. Columns R holds the sizes of reachability sets, omitting symmetries, and their computing times, for the models with the number of tracks specified in the first column. Column R ≈ (our) shows the sizes and computing time of the symmetry reduced reachability sets computed by our tool. As can be observed, we obtain the expected gains in size, as well as considerable gains in computing times. The numbers in grey font have been obtained "analytically" by summing the sizes of orbits of the symmetry reduced markings as building spaces of such sizes are beyond the capabilities of our tool (which is based on enumerative approaches).

The last column shows the results of computing the symmetry reduced reachability sets by the latest available version of tool LoLA (V2.0), which relies upon the techniques of [START_REF] Schmidt | LOLA A Low Level Analyser[END_REF]. As can be seen, LoLA typically computes several representatives per orbit. As a consequence, the gain on the number of states obtained by symmetry reduction is much smaller than what we obtain with our treatment. On the other hand, LoLA can extract more symmetries from nets than we are able to express, and computes symmetries automatically from bare nets. We have not been able to compare our results with those of [START_REF] Junttila | New Canonical Representative Marking Algorithms for Place/Transition-Nets[END_REF].

The results on the timed models are shown in the table of Figure 3, for two state class graph constructions. As in the untimed case, the grey numbers have been obtained by summing the sizes of orbits of the symmetry reduced classes.

For the same number of tracks, the number of state classes of the timed model (columns SCG and SCG ≈ ) is much larger than the number of markings in the untimed model. The gain obtained by symmetry reduction of state classes is however similar to that obtained for markings in the untimed version, both in terms of size of state spaces and computing times. It can also be observed that the coarser construction of "state classes under inclusion" (columns SCG ⊆ and SCG ⊆ ≈ ), only preserving markings (cf. Section 2) benefits of similar gains.

We conclude our experiments with a timed example featuring embedded symmetries. The TPN considered is made of 6 copies of the net represented Figure 4, with various symmetry declarations specified in the left column.

Omitting time information, the nets have factorized marking graphs of the sizes indicated in column R ≈ . Columns SCG ≈ and SCG ⊆ ≈ show the effects of symmetry reduction on the graphs of state classes for the various symmetry descriptions. The last line shows the figures when no symmetries are specified: omitting time information, the net has then 64 markings and 384 transitions; taking time information into account it admits 1 973 488 state classes and 11 285 976 transition(s) for the standard SCG construction and 1957 classes for the coarser SCG ⊆ construction, These experiments, and many others conducted over the last months, confirm that reduction by symmetry, when applicable, is an effective way of fighting combinatorial explosion. They are even more important for real-time models since alternative abstractions like partial order methods, unfolding methods or logic-based symbolic methods appear more difficult to apply on such models. Symmetry reduction allows one to perform verification of TPN faster and with much less computing resources (a laptop may suffice where a large server was required).

Towards richer symmetries

The preliminary implementation presented in the previous section forbids interactions between components of a pool, which can be limiting. That restriction can be relaxed: [START_REF] Bourdil | Contribution à la modélisation et la vérification formelle par model-checking-Symétries pour les Réseaux de Petri Temporels[END_REF] introduces a construction that given a group specification on component identifiers, an arity n, a component TPN N and an interaction pattern between components, builds the net resulting from the synchronization of n copies of N following the interaction pattern, with the symmetries arising from the group specification on component identifiers.

Our component language for nets can be enriched to handle such constructions. This would allow one to build richer models, such as the well known Fischer protocol in which all components are in a full symmetry, but interact with each others though a lock variable. However, if pool components are allowed to interact, then it would not be true in general that the length of all transition orbits are equal to the number of components in the pool, which prevents to use the sorting method of Section 4.4 to compute canonical representatives. Alternative, sub-optimal, methods could be used though. Note that, since the lock variable in that protocol holds a process identifier, the Timed Automata model of the Fischer protocol in [START_REF] Hendriks | Adding Symmetry Reduction to Uppaal[END_REF] does not fulfill either the conditions ensuring that the canonization algorithm used in that work produces canonical representatives.

Related work and Conclusion

In the context of Petri nets, symmetry reduction methods have been mostly applied to Colored Petri Nets (and the problem of symmetries on data values). The problem that we address in this paper is quite different. Concerning symmetries for real-time models, the only works we are aware of are on Uppaal [START_REF] Hendriks | Adding Symmetry Reduction to Uppaal[END_REF] and RED [START_REF] Wang | Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures[END_REF]. The latter combines logic-based symbolic exploration with symmetries and relies on over-approximations of the state space; so it uses different methods than those discussed here. The treatment of symmetries for Timed Automata [START_REF] Hendriks | Adding Symmetry Reduction to Uppaal[END_REF] is closer in spirit to our work.

We developed a symmetry reduction method for the State Class Graph construction of Time Petri nets. That, as far as we know, had never been attempted. As appears from Section 5, the technical treatment differs significantly from that of [START_REF] Hendriks | Adding Symmetry Reduction to Uppaal[END_REF]. Actually the difference is not surprising since (going beyond the difference between the models) the abstraction method for Timed Automata is based on clock domains-that is on the time elapsed since a transition firedrather that on firing domains-that capture the time, in the future, when a transition can fire. For TPN, the firing domain approach is more interesting in practice since it yields smaller abstractions. Though not discussed in this paper, our symmetry reduction approach can be applied as well to the alternative Strong SCG construction introduced in [START_REF] Berthomieu | State Class Constructions for Branching Analysis of Time Petri Nets[END_REF], based on clock domains rather than firing domains. This abstraction yields larger state spaces in general but is required for handling some extensions of TPN, like priorities. The ordering required for the Strong SCG construction is significantly simpler than that derived in Section 5 for the SCG and, as one may expect, close to the ordering used in [START_REF] Hendriks | Adding Symmetry Reduction to Uppaal[END_REF].

We have several opportunities for extending our work. The pragmatic reduction approach proposed in Section 4 is useful in many cases, but forbidding interactions between components of a pool is limiting. As mentioned in Section 6.2, we could relax this restriction in our component language, but this may prevent to compute canonical representatives with the optimal algorithm discussed in Section 4.

There is room in our method, however, for integrating alternative algorithms for computing representatives if required by some component. In our treatment, the canonization algorithm used for pool components could depend on the features of the net described, using the optimal algorithm of Section 4 if components do not interact, or some sub-optimal algorithm when they do.

In the same vein, we could add to our language of components other operators, for other commonly found symmetries like dihedral or cube symmetries, each handled with their own algorithm for computing representatives. Finally, it is tempting to investigate some combination of the techniques of [START_REF] Schmidt | Integrating Low Level Symmetries into Reachability Analysis[END_REF] with our. For components in which symmetries are not easily expressed in our language, they could be computed from the component; a dedicated algorithm would be used for computing representatives for their states.

These aspects are largely orthogonal to the real-time concerns which were the main focus of the work presented here; we hope to investigate them in the future.

3. γ k,i = β k -α i and γ k,j = γ k,j : Since α i ≤ α j (shown above) and β k , α i and α j are non-negative (Lemma 3), we have β k -α i ≥ β k -α j then γ k,j ≤ β k -α j ≤ β k -α i = γ k,i , hence γ k,j ≤ γ k,i 4. γ k,i = β k -α i and γ k,j = β k -α j : then γ k,i ≥ γ k,j since α i ≤ α j (by above)

k is newly-enabled by Lemma 2 γ k,i = β s k -α i , γ k,j = β s k -α j it was proved above that α i ≤ α j , and Lemma 3 says that alpha's and beta's are non-negative hence β s k -α i ≥ β s k -α j and consequently γ k,i ≥ γ k,j

Proof of Lemma 6, Page 14

Assume (m, D) is a class obtained in the SCG construction and i, j are two transitions enabled by m with the same static time interval (I s (i) = I s (j)). Then either i D j or j D i.

We consider the following three possible cases. Informally, the first case is when transitions i and j are introduced simultaneously in system D (they have the same "age"), the second is when they are introduced at different times (one is older than the other), and the last case asserts that the relationships between i and j is preserved whatever the transition introduced next as long as i and j stay persistent.

Both i and j are newly-enabled at (m, D):

Then γ i,j = β s i -α s j , γ j,i = β s j -α s i and thus γ i,j = γ j,i since I s (i) = I s (j). for any k = i, j, γ i,k = β s i -α k , γ j,k = β s j -α k and thus γ i,k = γ j,k since I s (i) = I s (j). So i = D j; both i D j and j D i hold.

i is persistent and j is newly-enabled (or the converse, symmetrically):

γ i,j ≤ γ j,i
since j is newly-enabled, we have γ i,j = β i -α s j and γ j,i = β s j -α i so γ i,j ≤ γ j,i ⇔ β i + α i ≤ β s j + α s j but I s (i) = I s (j) by hypothesis, so γ i,j ≤ γ j,i ⇔ β i + α i ≤ β s i + α s i by Lemma 3 we have α i ≤ α s i and β i ≤ β s i hence β i + α i ≤ β s i + α s i and γ i,j ≤ γ j,i

  state classes C = (m, D) and C = (m , D ) are equal, denoted C ∼ = C , if m = m and D ⇔ D (i.e. D and D have equal solution sets).

N

  ::= B | N| | |N | N|| || ||N | NΘ Θ Θ | P ool P ool P ool (n, N ) | Ring Ring Ring (n, N ) For example, the expression (Ring Ring Ring(8, P ) | | | Q | | | P ool P ool P ool(3, R)) denotes the net obtained by synchronizing a ring of 8 instances of component P with component Q and a pool of 3 instances of component R.

Lemma 2 (

 2 Computing firing domains). Assume C = (m, D) is a class with D in closure form. Then for every transition t in E(m) there is a unique class C = (m , D ) obtained from C by firing t such that D is also in closure form. Moreover D obeys the following constraints, for each distinct transitions i, j ∈ E(m ):

Figure 1 :

 1 Figure 1: Illustration of Lemma 5: ≥ imply ≥ .

2 .

 2 Canonical representatives for markings in the untimed examples and for state classes in the timed examples are computed exactly as explained in Sections 4.3 and 4.4, respectively.

  sym.) R≈ (our) R≈ (lola)

Figure 2 :

 2 Figure 2: Untimed level crossing example.

Figure 3 :

 3 Figure 3: Timed level crossing example.

Figure 4 :

 4 Figure 4: Component N and example symmetries.

Tina is available at http://www.laas.fr/tina, its experimental extension supporting symmetries is available at http://www.laas.fr/tina/symmetries.

Proof of Lemma 5, Page 14

Lemma 5 is pictured in Figure 1. Assume C = (m, D) is a class obtained in the SCG construction and i, j are two transitions with the same static time interval (I s (i) = I s (j)). We show that if i D j, then (i) α i ≤ α j , (ii) β i ≤ β j , and (iii) for all transition k distinct from i, j, γ k,j ≤ γ k,i . (In the remainder of the proof, we use the name F to denote part (iii) of this conjunction).

The proof is by case analysis on i, j.

If both i and j are newly-enabled:

i , α j = α s j , and α s i = α s j by hypothesis

and α s i = α s j by hypothesis hence i = D j and consequently F holds If i persistent and j newly-enabled (or the converse, symmetrically):

since j is newly-enabled, we have α j = α s j , so α i > α j ⇔ α i > α s j , which is impossible since α s j = α s i by hypothesis and 0 ≤ α i ≤ α s i by Lemma 3.

similarly, since j is newly-enabled, we have β j = β s j , so

Otherwise consider any sequence (C x ) 0≤x≤p of classes from the initial class ending at class C (i.e. C p = C); we denote α x i , β x i , γ x k,i the bounds in class C x . Let C n be the last class in that sequence in which γ n k,i = β n k -α n i . By Lemma 2, C n necessarily exists and, for any u ∈]n, p], i and k are persistent in class C u and

If both i and j are persistent: by induction on firing sequences.

Assuming we have

and both i and j are persistent in D , we have

we have α i = -min k γ k,i and α j = -min k γ k,j by Lemma 2, γ i,j ≤ γ j,i and (∀l = i, j)(γ li ≥ γ lj ) by induction hypothesis, so -min k γ k,i ≤ -min k γ k,j and thus α i ≤ α j β i ≤ β j we have β i = γ i,f and β j = γ j,f by Lemma 2, γ i,f ≤ γ j,f by induction hypothesis, so

we have four cases to consider:

since j is newly-enabled, we have

Both i and j are persistent and i D j (or j D i, symmetrically): by induction using Lemma 2:

initially: if j is newly-enabled in D, in which i is persistent, then i D j holds (see the previous case) induction step: assume i and j are persistent in (m, D) and (m , D ),

Lemma 2 yields γ i,j = min(γ i,j , β i -α j ) = min(γ i,j , γ i,f -α j ) γ j,i = min(γ j,i , β j -α i ) = min(γ j,i , γ j,f -α i ) we have four cases to consider:

1. γ i,j = γ i,j and γ j,i = γ j,i : γ i,j ≤ γ j,i by hyp., so γ i,j ≤ γ j,i 2. γ i,j = γ i,j and γ j,i = γ j,f -α i : γ i,f ≤ γ j,f by ind. hyp. and α j ≥ α i by Lemma 5 so γ i,j ≤ γ i,f -α j ≤ γ j,f -α i = γ j,i , that is γ i,j ≤ γ j,i 3. γ i,j = γ i,f -α j and γ j,i = γ j,i : then by ind. hyp.

γ i,j ≤ γ i,j ≤ γ j,i = γ j,i , hence γ i,j ≤ γ j,i 4. γ i,j = γ i,f -α j and γ j,i = γ j,f -α i : then by ind. hyp. and Lemma 5:

γ j,k = min(γ j,k , β j -α k ) = min(γ j,k , γ j,f -α k ) we have four cases to consider:

1. γ i,k = γ i,k and γ j,k = γ j,k : γ i,k ≤ γ j,k by hyp. thus γ i,k ≤ γ j,k 2. γ i,k = γ i,k and γ j,k = γ j,f -α k : γ i,f ≤ γ j,f by ind.

hyp. so γ i,k ≤ γ i,f -α k ≤ γ j,f -α k = γ j,k , hence γ i,k ≤ γ j,k