Nicolas Amat
email: nicolasamat@laas.fr

Bernard Berthomieu

Silvano Dal

A Polyhedral Abstraction for Petri nets and its Application to SMT-Based Model Checking

We define a new method for taking advantage of net reductions in combination with a SMT-based model checker. Our approach consists in transforming a reachability problem about some Petri net, into the verification of an updated reachability property on a reduced version of this net. This method relies on a new state space abstraction based on systems of constraints, called polyhedral abstraction.

We prove the correctness of this method using a new notion of equivalence between nets. We provide a complete framework to define and check the correctness of equivalence judgements; prove that this relation is a congruence; and give examples of basic equivalence relations that derive from structural reductions.

Our approach has been implemented in a tool, named SMPT, that provides two main procedures: Bounded Model Checking (BMC) and Property Directed Reachability (PDR). Each procedure has been adapted in order to use reductions and to work with arbitrary Petri nets. We tested SMPT on a large collection of queries used in the Model Checking Contest. Our experimental results show that our approach works well, even when we only have a moderate amount of reductions.

Introduction

A significant focus in model checking research is finding algorithmic solutions to avoid the "state explosion problem", that is finding ways to analyse models that are out of reach using current verification methods. To overcome this problem, it is often useful to rely on symbolic representation of the state space (like with decision diagrams) or on an abstraction of the problem, for instance with the use of logical approaches like SAT solving. We can also benefit from optimizations related to the underlying model. When analysing Petri nets, for instance, a valuable technique relies on the transformation and decomposition of nets, a method pioneered by Berthelot [START_REF] Berthelot | Transformations and Decompositions of Nets[END_REF] and known as structural reduction.

We recently proposed a new abstraction technique based on reductions [START_REF] Berthomieu | Petri net reductions for counting markings[END_REF][START_REF] Berthomieu | Counting Petri net markings from reduction equations[END_REF]. The idea is to compute reductions of the form (N, E, N ), where: N is an initial net (that we want to analyse); N is a residual net (hopefully much simpler than N ); and E is a system of linear constraints. The idea is to preserve enough information in E so that we can rebuild the reachable markings of N knowing only the ones of N . In a nutshell, we capture and abstract the effect of reductions using a set of linear constraints between the places of N and N .

In this paper, we show that this approach works well when combined with SMT-based verification. In particular, it provides an elegant way to integrate reductions into known verification procedures. To support this statement, we provide a full theoretical framework based on the definition of a new equivalence relation between Petri nets (Sect. 3) and show how to use it for checking safety and invariant properties (Sect. 4). Our method does not impose restrictions on the syntax of nets, such as constraints on the weights of arcs or bounds on the marking of places.

We have previously applied this technique in a symbolic model checker, called TEDD, that uses Set Decision Diagrams [START_REF] Thierry-Mieg | Hierarchical set decision diagrams and regular models[END_REF] in order to generate an abstract representation for the state space of a net N . In practice, we can often reduce a Petri net N with n places (from a high dimensional space) into a residual net N with far fewer places, say n (in a lower-dimensional space). Hence, with our approach, we can represent the state space of N as the "inverse image", by the linear system E, of a subset of vectors of dimension n . This technique can result in a very compact representation of the state space. We observed this effect during the recent editions of the Model Checking Contest (MCC) [START_REF] Amparore | Presentation of the 9th Edition of the Model Checking Contest[END_REF], where our tool finished at the first place for three consecutive years in the State Space category. In this paper, we show that we can benefit from the same "dimensionality reduction" effect when using automatic deduction procedures. Actually, since we are working with (possibly unbounded) vectors of integers, we need to consider SMT instead of SAT solvers. We show that it is enough in our case to use solvers for the theory of Quantifier-Free formulas on Linear Integer Arithmetic, what is known as QF-LIA in SMT-LIB [START_REF] Barrett | The SMT-LIB Standard: Version 2[END_REF].

To adapt our approach with the theory of SMT solving, we define an abstraction based on Boolean combinations of linear constraints between integer variables (representing the marking of places). This results in a new relation N E N , which is the counterpart of the tuple (N, E, N ) in a SMT setting. We named this relation a polyhedral abstraction in reference to "polyhedral models" used in program optimization and static analysis [START_REF] Besson | Polyhedral analysis for synchronous languages[END_REF][START_REF] Feautrier | Automatic parallelization in the polytope model[END_REF]. Indeed, like in these works, we propose an algebraic representation of the relation between a model and its state space based on the sets of solutions to systems of constraints. We should also often use the term E-abstraction equivalence to emphasize the importance of the linear system E. One of our main results is that, given a relation N E N , we can derive a formula Ẽ such that F is an invariant for N if and only if Ẽ ∧ F is an invariant for the net N . Since the residual net may be much simpler than the initial one, we expect that checking the invariant Ẽ ∧ F on N is more efficient than checking F on N .

Our approach has been implemented and computing experiments show that reductions are effective on a large benchmark of queries. We provide a prototype tool, called SMPT, that includes an adaptation of two procedures, Bounded Model Checking (BMC) [START_REF] Biere | Symbolic Model Checking without BDDs[END_REF] and Property Directed Reachability (PDR) [START_REF] Bradley | SAT-Based Model Checking without Unrolling[END_REF][START_REF] Bradley | Understanding IC3. In: Theory and Applications of Satisfiability Testing (SAT)[END_REF]. Each of these methods has been adapted in order to use reductions and to work with arbitrary Petri nets. We tested SMPT on a large collection of queries (13 265 test cases) used during the 2020 edition of the Model Checking Contest and participated, with our tool, in the two reachability competitions in the MCC'2021. Our experimental results show that our approach works well, even when we only have a moderate amount of reductions.

Outline and contributions. The paper is organized as follows. We start by defining the notations used in our work in Sect. 2, where we rely on a presentation of Petri net semantics that emphasizes the relationship with the QF-LIA theory. In Sect. 3, we define our notion of polyhedral abstraction and prove several of its properties. We give a description of some of the structural reductions used in our approach and show how they correspond to axioms of our polyhedral abstraction equivalence. We also prove that polyhedral abstractions are preserved by composition and transitivity, which gives a simple way to check the equivalence between two complex nets. We use these results in Sect. 4 and 5 to describe an adaptation of two SMT-based, model checking algorithms for Petri nets that can take advantage of reductions and prove their correctness. Before concluding, we report on experimental results on an extensive collection of nets and queries. Our results are quite promising. For example, on our benchmark, we observe that we are able to compute twice as many results using reductions than without.

Many results and definitions were already presented in a shorter version of the paper [START_REF] Amat | On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets[END_REF]. This extended version contains several additions that improve on the two main contributions of our work.

Concerning our definition of a polyhedral abstraction for Petri nets, we describe more precisely the reduction rules used in our approach and give more detailed proofs and definitions about the properties of our equivalence. With these additions, we give a stand-alone definition of E-abstraction equivalence that provides a more algebraic (and therefore less monolithic) approach than the one used previously in our work about computing the number of reachable states [START_REF] Berthomieu | Counting Petri net markings from reduction equations[END_REF]. We believe that our equivalence could be reused in other settings.

Concerning our application to SMT-based model checking. We give a detailed description of our adaptation of the PDR procedure for model checking Petri nets in the case of coverability properties.

Petri nets and linear arithmetic constraints

Some familiarity with Petri nets is assumed from the reader. We recall some basic terminology. Throughout the text, comparison (=, ) and arithmetic operations (-, +) are extended pointwise to functions and tuples. Definition 2.1. A Petri net N is a tuple (P, T, Pre, Post) where:

• P = {p 1 , . . . , p n } is a finite set of places,

• T = {t 1 , . . . , t k } is a finite set of transitions (disjoint from P ),

• Pre : T → (P → N) and Post : T → (P → N) are the pre-and post-condition functions (also called the flow functions of N ).

States

A state m of a net, also called a marking, is a mapping m : P → N which assigns a number of tokens, m(p), to each place p in P . A marked net (N, m 0 ) is a pair composed from a net and an initial marking m 0 .

A marking m is k-bounded when each place has at most k tokens; property p∈P m(p) ≤ k is true. Likewise, a marked Petri net (N, m 0 ) is bounded when there is k such that all reachable markings are k-bounded. A net is safe when it is 1-bounded. In our work, we consider generalized Petri nets (in which net arcs may have weights larger than 1) and we do not restrict ourselves to bounded nets.

Behaviour

A transition t ∈ T is enabled at marking m ∈ N P when m(p) ≥ Pre(t, p) for all places p in P . (We can also simply write m Pre(t), where stands for the component-wise comparison of markings.) A marking m ∈ N P is reachable from a marking m ∈ N P by firing transition t, denoted m t -→ m , if: (1) transition t is enabled at m; and (2) m = m -Pre(t) + Post(t).

By extension, we say that a firing sequence = t 1 . . . t n ∈ T * can be fired from m, denoted m = ⇒ m , if there exist markings m 0 , . . . , m n such that m = m 0 , m = m n and m i t i+1 --→ m i+1 for all i in the range 0..n -1.

We denote R(N, m 0 ) the set of markings reachable from m 0 in N :

R(N, m 0 ) {m | ∃ . m 0 = ⇒ m} (1)
The semantics of a marked net is the Labeled Transition System (LTS), with nodes in R(N, m 0 ) and edges between states (m, m ) whenever m t -→ m . We focus mostly on reachable states in our work and will therefore seldom refer to the LTS of the net.

Labels and observations

In the following, we will often consider that each transition is associated with a label (a symbol taken from an alphabet Σ). In this case, we assume that a net is associated with a labeling function l : T → Σ ∪ {τ }, where τ is a special symbol for the silent action name. Every net has a default labeling function l N such that Σ = T and l N (t) = t for every transition t ∈ T .

We can extend the notion of labels to sequences of transitions in a straightforward way. Given a relabeling function, l, we can extend it into a function from T into Σ such that l( ) = , l(τ ) = and l( t) = l( ) l(t). Given a sequence of labels σ in Σ , we write (N, m) σ = ⇒ (N, m ) when there is a firing sequence in T such that (N, m) = ⇒ (N, m ) and σ = l( ). We say in this case that σ is an observation sequence of the marked net (N, m).

E M (p 5 = p 4 ) ∧ (a 1 = p 1 + p 2 ) ∧ (a 2 = p 3 + p 4 ) ∧ (a 1 = a 2 ).

Graphical notations

We use the standard graphical notation for nets, where places are depicted as circles and transitions as squares. For marking, we use the notation p * k to state that place p has k tokens and we omit empty places. With the net displayed in Fig. 1 (left), and with our convention, the initial marking is m 0 p 0 * 5 p 6 * 4 (only 5 and 4 tokens in places p 0 and p 6 ). We have m 0 = ⇒m 0 with t 0 t 0 t 1 t 1 t 2 t 3 t 4 and m 0 p 0 * 3 p 2 * 1 p 3 * 1 p 6 * 3; and therefore m 0 a a b c ===⇒ m 0 when we only look at (observable) labels.

Properties

We can define many properties on the markings of a net N using Boolean combinations of linear constraints with integer variables. Assume that we have a marked net (N, m 0 ) with set of places P = {p 1 , . . . , p n }. We can associate a marking m over P to the formula m(x 1 , . . . , x n ), below. In this context, an equation x i = k means that there must be k tokens in place p i . Formula m is obviously a conjunction of literals, what is called a cube in [START_REF] Bradley | SAT-Based Model Checking without Unrolling[END_REF].

m(x 1 , . . . , x n ) (x 1 = m(p 1 )) ∧ • • • ∧ (x k = m(p k )) (2)
In the remainder, we use the notation φ( x) for the declaration of a formula φ with variables in x, instead of the more cumbersome notation φ(x 1 , . . . , x n ). We also simply use φ( v) instead of φ{x 1 ← v 1 } . . . {x n ← v n }, for the substitution of x with v in φ. We often use place names as variables (or parameters) and use p for the vector (p 1 , . . . , p n ). We also often use m instead of m( p).

Definition 2.2. (Model of a formula)

We say that a marking m is a model of (or m satisfies) property φ, denoted m |= φ, when formula φ( x) ∧ m( x) is satisfiable. In this case φ may use variables that are not necessarily in P .

We can use this approach to reframe many properties on Petri nets. For instance the notion of safe markings, described previously: a marking m is safe when m |= BND 1 ( x), where BND k is a predicate in QF-LIA defined as:

BND k ( x) i∈1..n (x i k) (3)
Likewise, the property that transition t is enabled corresponds to the predicate ENBL t below, in the sense that t is enabled at m when m |= ENBL t ( x).

ENBL t ( x) i∈1..n (x i Pre(t, p i )) (4)
Another example is the definition of deadlocks, which are characterized by formula DEAD( x)

t∈T ¬ENBL t ( x). We give other examples in Sect. 5, when we encode the transition relation of a Petri net using formulas.

In our work, we focus on the verification of safety properties on the reachable markings of a marked net (N, m 0 ). Examples of the properties that we want to check include: whether some transition t is enabled (commonly known as quasi-liveness); whether there is a deadlock; whether some invariant between place markings is true; . . .

Definition 2.3. (Invariant and reachable properties)

Property φ is an invariant on (N, m 0 ) if and only if we have m |= φ for all m ∈ R(N, m 0 ). We say that φ is reachable when there exists m ∈ R(N, m 0 ) such that m |= φ.

In our experiments, we consider the two main kinds of reachability formulas used in the MCC: AG φ (true only when φ is an invariant), and EF φ (true when φ is reachable), where φ is a Boolean combination of atomic properties (it has no modalities). At various times, we will use the fact that φ is invariant if and only if its negation is not reachable: EF ¬φ is false.

Polyhedral abstraction and E-equivalence

We define a new notion, called E-abstraction, that is used to state a correspondence between the set of reachable markings of two Petri nets "modulo" some system of linear constraints E. Basically, we have that (N 2 , m 2 ) is an abstraction of (N 1 , m 1 ) when, for every sequence m 1

σ 1 = ⇒ m 1 in N 1 , there must exist a sequence m 2 σ 2 = ⇒ m 2 in N 2 such that E ∧ m 1 ∧ m 2 is
satisfiable. We also ask that there exists such sequence for every marking m 2 such that E ∧ m 1 ∧ m 2 is satisfiable. Therefore, knowing E, we can compute the reachable markings of N 1 from those of N 2 .

We also ask for the observation sequences, σ 1 and σ 2 in this case, to be equal. With the addition of this constraint, we prove that the reflexive and symmetric closure of an E-abstraction is also a congruence, which we call an E-equivalence (defined formally in Sect. 3.1).

We can illustrate these notions using the two nets M 1 , M 2 in Fig. 1 and the linear constraint

E M (p 5 = p 4 ) ∧ (a 1 = p 1 + p 2 ) ∧ (a 2 = p 3 + p 4 ) ∧ (a 1 = a 2 ). Recall that marking m 1 p 0 * 3 p 2 * 1 p 3 * 1 p 6 * 3 is reachable in M 1 . We also have that E M ∧ m 1 entails (p 0 = 3) ∧ (p 6 = 3) ∧ (a 2 = 1). Hence, if we prove that (M 1 , m 1 ) is E M -equivalent to (M 2 , m 2 ), we can conclude that the marking m 2 a 2 * 1 p 0 * 3 p 6 * 3 is reachable in M 2 .
Conversely, we have several markings (exactly 4) in M 1 that correspond to the constraint E M ∧ m 2 ≡ (p 5 = p 4 ) ∧ (p 1 + p 2 = 1) ∧ (p 3 + p 4 = 1) ∧ m 2 . All these markings are reachable in M 1 using the same observation sequence a a b c. More generally, each marking m 2 of N 2 can be associated to a convex set of markings of N 1 , defined as the set of positive integer solutions of E ∧ m 2 . Moreover, these sets form a partition of R(N 1 , m 1 ). This motivates our choice of calling this relation a polyhedral abstraction.

While our approach does not dictate a particular method for finding pairs of equivalent nets, we rely on an automatic approach based on the use of structural net reductions. When the net N 1 can be reduced, we will obtain a resulting net (N 2 ) and a condition (E) such that N 2 is a polyhedral abstraction of N 1 . In this case, E will always be expressed as a conjunction of equality and inequation constraints between linear combinations of integer variables (the marking of places). This is why we should often use the term reduction constraints when referring to E. Our goal is to transform any reachability problem on the net N 1 into a reachability problem on the (reduced) net N 2 , which is typically much easier to check.

Solvable systems and E-equivalence

Before defining our equivalence more formally, we need to introduce some constraints on the condition, E, used to correlate the markings of two different nets. We say that a pair of markings (m 1 , m 2 ) are compatible (over respective sets of places P 1 and P 2 ) when they have the same number of tokens on their shared places, meaning m 1 (p) = m 2 (p) for all p in P 1 ∩ P 2 . This is a necessary and sufficient condition for formula m 1 ∧ m 2 to be satisfiable. When this is the case, we denote m 1 m 2 the unique marking in (P 1 ∪ P 2 ) defined by:

(m 1 m 2 )(p) = m 1 (p) if p ∈ P 1 , m 2 (p) otherwise. (5)
Equipped with this notion, we can say that two markings m 1 , m 2 (defined over the set of places P 1 , P 2 of two nets N 1 and N 2 ) are "a solution" of constraints E when they are compatible with each other and E ∧ m 1 m 2 is satisfiable.

This leads to the notion of solvable system, such that every reachable marking of N 1 can be paired with at least one reachable marking of N 2 to form a solution of E; and reciprocally. Definition 3.1. (Solvable system of reduction constraints) A system of linear constraints, E, is solvable for N 1 , N 2 if and only if for all reachable markings m 1 in N 1 there exists at least one marking m 2 of N 2 , compatible with m 1 , such that m 1 m 2 |= E, and vice versa for every reachable marking m 2 in N 2 .

In the following, when we use an E-abstraction equivalence between two marked nets (N 1 , N 2 ), we ask that condition E be solvable for N 1 , N 2 (see condition A2). While this property is not essential for most of our results, it simplifies our presentation and it will always be true for the reduction constraints generated with our method. On the other hand, we do not prohibit to use variables in E that are not in P 1 ∪ P 2 . Actually, such a situation will often occur in practice, when we start to chain several reductions.

We define our notion of E-abstraction as an equivalence relation between the markings reached using equal "observation sequences". An E-abstraction equivalence (shortened as E-equivalence) is an abstraction in both directions.

Definition 3.2. (E-abstraction and E-abstraction equivalence)

Assume N 1 = (P 1 , T 1 , Pre 1 , Post 1 ) and N 2 = (P 2 , T 2 , Pre 2 , Post 2 ) are two Petri nets with respective labeling functions l 1 , l 2 , over the same alphabet Σ, and E a system of linear constraints. We say that the marked net (N 2 , m 2 ) is an E-abstraction of (N 1 , m 1 ), denoted (N 1 , m 1 ) E (N 2 , m 2 ), if and only if:

(A1) the initial markings are compatible with E, meaning m 1 m 2 |= E.

(A2) for all firing sequences (N 1 , m 1 )

1 = ⇒ (N 1 , m 1 ) in N 1 ,
∈ T 2 such that (N 2 , m 2 ) 2 = ⇒(N 2 , m 2 ) and l 1 ( 1 ) = l 2 ( 2 ). We say that (N 1 , m 1 ) is E-equivalent to (N 2 , m 2 ), denoted (N 1 , m 1 ) E (N 2 , m 2 ), when we have both (N 1 , m 1 ) E (N 2 , m 2 ) and (N 2 , m 2 ) E (N 1 , m 1 ).
Notice that condition (A2) is defined only for observation sequences starting from the initial marking of N 1 . Hence the relation is usually not true on every pair of matched markings; it is not a bisimulation. Also, condition (A2) can be defined in an alternative way using observation sequences.

(A2) for all observation sequences σ such that (N 1 , m 1 ) σ = ⇒ (N 1 , m 1 ), there is at least one marking m 2 over P 2 such that m 1 m 2 |= E, and for all markings m 2 over P 2 such that m 1 m 2 |= E we must have (N 2 , m 2 )

σ = ⇒ (N 2 , m 2 ).
By definition, relation E is symmetric. We deliberately use a "comparison symbol" for our equivalence, , in order to stress the fact that we expect the fact that N 2 is a reduced version of N 1 .

In particular, we expect that |P 2 | ≤ |P 1 |.

Basic properties of polyhedral abstraction

We prove that we can use E-equivalence to check the reachable markings of N 1 simply by looking at the reachable markings of N 2 . We give a first property that is useful in the context of bounded model checking, when we try to find a counter-example to a property by looking at firing sequences with increasing length. Our second property is useful for checking invariants, and is at the basis of our implementation of the PDR method for Petri nets.

Lemma 3.3. (Reachability checking) Assume (N 1 , m 1 ) E (N 2 , m 2 ). Then for all m 1 in R(N 1 , m 1 ) there is m 2 in R(N 2 , m 2 ) such that m 1 m 2 |= E.

Proof:

Since m 1 is reachable, there must be a firing sequence 1 in N 1 such that (N 1 , m 1 )

1 = ⇒ (N 1 , m 1 )
. By condition (A2), there must be some marking m 2 over P 2 , compatible with m 1 , such that m 1 m 2 |= E and (N 2 , m 2 ) 2 = ⇒ (N 2 , m 2 ) (for some firing sequence 2 ). Therefore we have m 2 reachable in N 2 such that m 1 m 2 |= E. Lemma 3.3 can be used to find a counter-example m 1 , to some property F in N 1 , just by looking at the reachable markings of N 2 . Indeed, it is enough to find a marking m 2 reachable in N 2 such that m 2 |= E ∧ ¬F . This is the result we use in our implementation of the BMC method.

Our second property can be used to prove that every reachable marking of N 2 can be traced back to at least one marking of N 1 using the reduction constraints. (While this mapping is surjective, it is not a function, since a state in N 1 could be associated with multiple states in N 2 .)

Lemma 3.4. (Invariance checking) Assume (N 1 , m 1 ) E (N 2 , m 2 ). Then for all pairs of markings m 1 , m 2 of N 1 , N 2 such that m 1 m 2 |= E and m 2 ∈ R(N 2 , m 2 ) it is the case that m 1 ∈ R(N 1 , m 1 ). Proof: Take m 1 , m 2 a pair of markings in N 1 , N 2 such that m 1 m 2 |= E and m 2 ∈ R(N 2 , m 2 ). Hence there is a firing sequence 2 such that (N 2 , m 2 ) 2 = ⇒ (N 2 , m 2 ). By condition (A2), since m 1 m 2 |= E, there must be a firing sequence in N 1 , say 1 , such that (N 1 , m 1 ) 1 = ⇒ (N 1 , m 1 ). Hence m 1 ∈ R(N 1 , m 1 ).
Using Lemma 3.4, we can easily extract an invariant on N 1 from an invariant on N 2 . Basically, if property E ∧ F is an invariant on N 2 (where F is a formula whose variables are in P 1 ) then we can prove that F is an invariant on N 1 . This property (the invariant conservation theorem of Sect. 4) ensures the soundness of the model checking technique implemented in our tool.

Composition laws

We prove that polyhedral abstraction is a transitive relation (Th 3.5) that is also closed by synchronous composition (Th 3.7) and relabeling (Th 3.8). These results can be used as a set of "algebraic laws" allowing us to derive complex equivalence assertions from much simpler instances, or axioms, inside arbitrary contexts. We give an example of such reasoning in Sect. 3.5.

Before defining our composition laws, we start by describing sufficient conditions in order to safely compose equivalence relations. The goal here is to avoid inconsistencies that could emerge if we inadvertently reuse the same variable in different reduction constraints.

The fresh variables in an equivalence statement EQ : (N 1 , m 1 ) E (N 2 , m 2 ) are the variables occurring in E but not in P 1 ∪ P 2 . (These variables can be safely "alpha-converted" in E without changing any of our results.) We say that a net N 3 is compatible with respect to EQ when (P 1 ∪ P 2 ) ∩ P 3 = ∅ and there are no fresh variables of EQ that are also places in P 3 . Likewise we say that the equivalence statement EQ : (N 2 , m 2 ) E (N 3 , m 3 ) is compatible with EQ when P 1 ∩ P 3 ⊆ P 2 and the fresh variables of EQ and EQ are disjoint.

The composition laws stated in the following theorems are useful to build larger equivalences from simpler axioms (reduction rules). We show some examples of reductions in the next section and how they occur in the example of Fig. 1.

Preservation by chaining

We prove that we can chain equivalences together in order to derive more general reduction rules. When doing so, we need to combine constraints together. Theorem 3.5. Assume we have two compatible equivalence statements

(N 1 , m 1 ) E (N 2 , m 2 ) and (N 2 , m 2 ) E (N 3 , m 3 ), then (N 1 , m 1 ) E∧E (N 3 , m 3 ).
Proof: First, we use the fact system E ∧ E is solvable for N 1 , N 3 . This is a consequence of the compatibility assumption, since no fresh variable in E can clash with a fresh variable in E . For similar reason, we have that

m 1 m 2 |= E and m 2 m 3 |= E entails m 1 m 3 |= E ∧ E . Indeed we even have the stronger property that m 1 ∧ m 2 ∧ m 3 ∧ E ∧ E is satisfiable.
From this, we obtain condition (A1) and the first constraint of condition (A2).

For the second constraint of condition (A2), we assume that σ is an observation sequence such that (N 1 , m 1 )

σ = ⇒ (N 1 , m 1 ). Hence, using the fact that (N 1 , m 1 ) E (N 2 , m 2 ), we have (N 2 , m 2 ) σ = ⇒ (N 2 , m 2 ) for every marking m 2 of N 2 such that m 1 m 2 |= E. Using a similar property from (N 2 , m 2 ) E (N 3 , m 3 ), we have (N 3 , m 3 ) σ = ⇒ (N 3 , m 3 ) for every marking m 3 of N 3 such that m 2 m 3 |= E.
The result follows from the observation that, since E and E are both solvable and the nets are compatible, for all markings m 1 of N 1 , if a marking m 3 of N 3 satisfies m 1 m 3 |= E ∧ E then there must be a marking m 2 of N 2 such that both m 1 m 2 |= E and m 2 m 3 |= E .

Preservation by synchronous composition

Our next result relies on the classical synchronous product operation between labeled Petri nets [START_REF] Lloret | Compositional design and verification of communication protocols, using labelled Petri nets[END_REF]. Assume N 1 = (P 1 , T 1 , Pre 1 , Post 1 ) and N 2 = (P 2 , T 2 , Pre 2 , Post 2 ) are two labeled Petri nets with respective labeling functions l 1 and l 2 on the respective alphabets Σ 1 and Σ 2 . We can assume, without loss of generality, that the sets P 1 and P 2 are disjoint.

We introduce a new symbol, •, used to build (structured) names for transitions that are not synchronized. The synchronous product between N 1 and N 2 , denoted as N 1 N 2 , is the net (P 1 ∪ P 2 , T, Pre, Post) with labelling function l where T is the smallest set containing:

• transition (t, •) if l 1 (t) ∈ Σ 2 , such that l((t, •)) = l 1 (t); • transition (•, t) if l 2 (t) ∈ Σ 1 , such that l((•, t)) = l 2 (t); • and transition (t 1 , t 2 ) if l 1 (t 1 ) = l 2 (t 2 ), such that l((t 1 , t 2 )) = l 1 (t 1 ).
The flow functions of N 1 N 2 are such that Pre((t 1 , t 2 ), p) = Pre 1 (t 1 , p) if p ∈ P 1 and t 1 = •, or Pre 2 (t 2 , p) if p ∈ P 2 and t 2 = • (and 0 in all the other cases). Similarly for Post.

To simplify our proofs, we define a notion of projection over firing sequences of Projections can be used to extract from a firing sequence of N 1 N 2 , the transitions that were fired from the left (•1) and right (•2) components of the synchronous product.

N 1 N 2 , that is two functions • 1 and • 2 such that • i = and ( t) • i = ( • i) (t • i) for all i ∈ 1..2, where (t 1 , •) • 1 = t, and (•, t 2 ) • 1 = , and (t 1 , t 2 ) • 1 = t 1 (
We also need to define a dual relation, denoted 1 2 , that defines the (potential) "zip merge" of firing sequences in T 1 ×T 2 into firing sequences of N 1 N 2 , when the two sequences can synchronize. When defined, 1 2 is the smallest set of sequences of N 1 N 2 satisfying the following inductive rules. In particular, we say that 1 and 2 can be synchronized when 1 2 = ∅.

• = { } • (t 1 1 ) = {(t 1 , •) | ∈ ( 1 )} if all the transitions in t 1 1 have labels in Σ 1 \ Σ 2 , ∅ otherwise. • (t 2 2 ) = {(•, t 2 ) | ∈ ( 2 )} if all the transitions in t 2 2 have labels in Σ 2 \ Σ 1 , ∅ otherwise. • (t 1 1 ) (t 2 2 ) =            {(t 1 , t 2 ) | ∈ ( 1 2 )} if l 1 (t 1 ) = l 2 (t 2 ), {(t 1 , •) | ∈ 1 (t 2 2 )} if l 1 (t 1 ) ∈ Σ 1 \ Σ 2 , {(•, t 2 ) | ∈ (t 1 1 ) 2 } if l 2 (t 2 ) ∈ Σ 2 \ Σ 1 , ∅ otherwise.
We can also project the reachable markings of a synchronous product over reachable markings of each of its components. Since the places in N 1 and N 2 are disjoint, we can always see a marking m in N 1 N 2 as the disjoint union of two (necessarily compatible) markings m 1 , m 2 from N 1 , N 2 . In this case we simply write m = m 1 m 2 .

More generally, we extend this product operation to marked nets and write (N 1 , m 1 ) (N 2 , m 2 ) for the marked net (N 1 N 2 , m 1 m 2 ). The following result underscores the equivalence between the semantics (the Labeled Transition System) of N 1 N 2 and the product of the LTS of its components. Lemma 3.6. (Projection and product of sequences) Assume there is a firing sequence

(N 1 N 2 , m 1 m 2 ) = ⇒(N 1 N 2 , m 1 m 2 ) on the synchronous product N 1 N 2 .
Then the projections • 1 and • 2 are firing sequences of their respective components,

(N i , m i ) •i = ⇒ (N i , m i ) for all i ∈ 1..2, such that • 1 and • 2 can be synchronized: • 1 • 2 = ∅. Conversely, if (N i , m i ) i = ⇒ (N i , m i ) for all i ∈ 1..2 and ∈ ( 1 2 ) then (N 1 N 2 , m 1 m 2 ) = ⇒ (N 1 N 2 , m 1 m 2 ).
Proof: See for instance Proposition 2.1 in [START_REF] Lloret | Compositional design and verification of communication protocols, using labelled Petri nets[END_REF].

We can now prove that E-abstraction equivalence is stable by synchronous composition. Note that it is enough to prove the results on E-abstraction, since the equivalence is symmetric.

Theorem 3.7. (Composability) Assume (N 1 , m 1 ) E (N 2 , m 2 )
and that (M, m) is compatible with respect to this equivalence, then

(N 1 , m 1 ) (M, m) E (N 2 , m 2 ) (M, m).
Proof: By hypothesis system E is solvable for N 1 , N 2 . Hence, since M is compatible, no place in the net M can occur in one of the constraints of E. Therefore E is also solvable for the pair of nets (N 1 M ) and (N 2 M ). Likewise, the initial markings (m 1 m) and (m 2 m) are compatible together and (m 1 m) (m 2 m) |= E (the constraints in m have no effect on the constraints of E). Therefore condition (A1) is valid for the marked nets (N 1 , m 1 ) (M, m) and (N 2 , m 2 ) (M, m), and we obtain the first constraint of condition (A2).

We are left with proving the second constraint of condition (A2). Assume we have a firing sequence in N 1 M . By our projection property (Lemma 3.6) it must be the case that

(N 1 M, m 1 m) = ⇒ (N 1 M, m 1 m ) with (N 1 , m 1 ) •1 =⇒ (N 1 , m 1 ). We also have that (M, m) •2 =⇒ (M, m ) such that ( • 1) ( • 2) = ∅.
By condition (A2) on the abstraction between N 1 and N 2 , it must be the case that (N 2 , m 2 )

2 = ⇒ (N 2 , m 2 ), for some firing sequence 2 of N 2 , for all markings m 2 of N 2 such that m 1 m 2 |= E.
Moreover the observable sequence obtained from 2 and • 1 are the same:

l 1 ( • 1) = l 2 ( 2 ) ( ),
which means also that ( 2 ) ( • 2) = ∅. Hence, using the second direction in Lemma 3.6, we can find a firing sequence in 2 ( • 2), say , such that

(N 2 N 3 , m 2 m 3 ) = ⇒ (N 2 M, m 2 m ). Like in the proof of condition (A1), we obtain that (m 1 m ) (m 2 m ) |= E from the fact that m 1 m 2 |= E,
and E is solvable, and M is compatible.

We are left to prove that and have the same observation sequences. This is a consequence of the fact that l 1 ( • 1) = l 2 ( 2 ) (property above); and the fact that, by construction of , we have Relabeling has no effect on the marking of a net. The relabeling law is true even in the case where b is the silent action τ . In this case we say that we hide action a from the net. We prove that E-abstraction equivalence is also preserved by relabeling and hiding.

• 1 = 2 and • 2 = • 2.
Theorem 3.8. If (N 1 , m 1 ) E (N 2 , m 2 ) then (N 1 [a/b], m 1 ) E (N 2 [a/b], m 2 ).
Proof:

Assume (N 1 , m 1 ) E (N 2 , m 2 )
. Condition (A1) does not depend on the labels and therefore it is also true between

N 1 [a/b], E and N 2 [a/b].
For condition (A2), we simply use the fact that for any firing sequences 1 and 2 , l

1 ( 1 ) = l 2 ( 2 ) implies l 1 [a/b]( 1 ) = l 2 [a/b]( 2 ).

Reduction rules

We define a simplified set of relations that can act as "axioms" in a system for deriving E-abstraction equivalences. Each of these axioms derives from a standard structural reduction rule (see e.g [START_REF] Berthelot | Transformations and Decompositions of Nets[END_REF][START_REF] Berthomieu | Counting Petri net markings from reduction equations[END_REF]), where labeled transitions play the role of interfaces with a possible outside "context".

Each rule is defined by a triplet (N 1 , E, N 2 ) such that (N 1 , m 1 ) E (N 2 , m 2 ). A rule also defines possible values for the initial markings, which can be expressed using integer parameters, and may also include a condition that should be true initially.

Each of our rules corresponds to instances of the reduction system that was defined in our previous work on "counting reachable markings" [START_REF] Berthomieu | Counting Petri net markings from reduction equations[END_REF] (we give a precise reference in each case). Hence they also correspond to instances of reduction rules implemented in our tool, called REDUCE, that can automatically find occurrences of reductions in Petri nets and apply them recursively. We give more information about this tool and the relation with our approach in Sect. 3.5. This section also contains an example showing how to apply our reduction rules to derive the equivalence stated in Fig. 1.

We consider four general families of reductions: first rules for agglomerating places (like [CON-CAT] and [AGG]); then rules based on a "place invariant" over the initial net (what we call a redundancy rule like [RED] and [SHORTCUT]); rules for garbage collecting dead places or transitions (like [DEADT] and [REDT]); and finally rules that can be used to abstract constant or "closed" places (like [CONSTANT] and [SOURCE]).

We give a detailed proof of correctness for our first "reduction axiom", rule [CONCAT], since it is representative of the complexity of checking simple instances of E-abstraction equivalence. We do not prove similar results for all the rules defined in this section but will only give one other example, for the redundancy rule [RED]. All the correctness proofs for the reduction rules given in this section are very similar to one of these two examples.

Rule [CONCAT]

Our first example is the prototypical example of net reduction, as defined in [START_REF] Berthelot | Transformations and Decompositions of Nets[END_REF]. It also corresponds to the simplest example of agglomeration rule (see the rule for chaining in Fig. 6 of [START_REF] Berthomieu | Counting Petri net markings from reduction equations[END_REF]).

Rule [CONCAT], Fig. 2, can be used to fuse together two places "connected only through a deterministic transition" (modeled as a silent transition in our approach). The constraints imposed for applying this rule is that place y 2 , in the initial net, must be initially empty. We also have the condition that no transition with an observable label (hence no transition that can potentially be merged with an outside context with a synchronous composition) can add a token directly to place y 2 . This condition is necessary to ensure the correctness of this rule, see Proposition 3.9.

Note that nets N 1 and N 2 are not bounded, since transition a can always be fired to increase the marking of places y 1 and x. Which means that we need to consider an unbounded number of firing sequences. Therefore it may not be possible to prove this result using an automatic verification method, such as model checking. Actually, we are working on the definition of an automatic proof method for certifying the correctness of reduction rules, which would be an interesting addition to our approach.

Proposition 3.9. (Correctness of rule [CONCAT])

We have (N 1 , m 1 ) E (N 2 , m 2 ), with E the system containing the single equation x = y 1 + y 2 , and N 1 , N 2 the nets depicted in Fig. 2.

Proof:

The constraints on the initial marking of the nets are such that m 1 (y 1 ) = m 2 (x) = K 0 and m 1 (y 2 ) = 0. To ease the presentation, we should use τ, a, b, c as the name of the transitions, and not only as labels.

We start by proving condition (A1) and the first constraint of condition (A2). By construction, we have m 1 m 2 |= E and E is solvable for N 1 , N 2 . Indeed, equation x = y 1 + y 2 is always satisfiable when we fix either the values of variables y 1 , y 2 , or the value of x.

We now prove the second constraint of condition (A2) for the relation

(N 1 , m 1 ) E (N 2 , m 2 ). Assume that (N 1 , m 1 ) 1 = ⇒ (N 1 , m 1 )
and that m 1 m 2 |= E. By definition of E, when m 1 is fixed, there is a unique solution for m 2 such that m 1 m 2 |= E; which is m 2 (x) = m 1 (y 1 ) + m 1 (y 2 ). Take 2 the unique firing sequence of N 2 such that l 1 ( 1 ) = l 2 ( 2 ) (basically 2 is obtained from 1 by erasing all occurrences of the silent transition). It is the case that (N 2 , m 2 ) 2 = ⇒ (N 2 , m 2 ), as needed. We are left to prove the same constraint for the relation

(N 2 , m 2 ) E (N 1 , m 1 ). Assume we have (N 2 , m 2 ) 2 = ⇒ (N 2 , m 2 ).
We prove that there is a firing sequence 1 such that (N 1 , m 1 )

1 = ⇒ (N 1 , m 1 ) and l 1 ( 1 ) = l 2 ( 2 )
, where m 1 is the marking defined by m 1 (y 1 ) = m 2 (x) and m 1 (y 2 ) = 0 (all the tokens are in y 1 ). We define 1 as the (unique) sequence obtained from 2 by adding one occurrence of the τ -transition before each occurrence of c in 2 . Intuitively, we always keep all the tokens in place y 1 of N 1 , except before firing a c; in which case we add a token to place y 2 . We can prove, using an induction on the size of 2 , that 1 is a legitimate firing sequence of (N 1 , m 1 ) and that (N 1 , m 1 )

1 = ⇒ (N 1 , m 1 ).

Rule [AGG]

Our second example of rule is for the agglomeration of places, see Fig. 3, that can be used to simplify a "cluster of places" between which tokens can move freely from y 2 to y 1 . This is an instance of the general "loop agglomeration" rule given in Fig. 7 of [START_REF] Berthomieu | Counting Petri net markings from reduction equations[END_REF].

We could easily define a family of reduction rules similar to [AGG] and [CONCAT] but for longer "loops" or "chains" of places, or with the addition of weights on the arcs. For the sake of brevity, we only list one archetypal instance of each rule in this section.

Rules [RED] and [SHORTCUT]

Our next two rules, Fig. 4, are reductions that can be used to eliminate redundant places, meaning places whose marking derives from a place invariant (and the knowledge of the marking of other places).

In rule [RED] for instance, with the assumption that we have more tokens in place z than in y initially, it is always the case that m(z)m(y) is a constant for all the reachable states m. Hence we can safely eliminate z and keep the relevant information in our linear system E.

Rule [SHORTCUT] gives a more involved example, that relies on a condition involving more than two places; an invariant of the form z = y 1 + y 2 + K.

We give the proof of correctness for the equivalence corresponding to rule [RED]. The proofs for other redundant place elimination rules are all similar.

Proposition 3.10. (Correctness of rule [RED])

Assuming K N , we have (N 1 , m 1 ) E (N 2 , m 2 ), with E the system containing the single equation x = y + N -K, and N 1 , N 2 the nets depicted in Fig. 4 (above).

Proof:

Condition K N is necessary in order to have that N -K 0, and therefore that the marking of y in N 2 is indeed non-negative.

By construction, we have m 1 m 2 |= E, satisfying condition (A1). The first constraint of condition (A2) follows from the fact that z = y + N -K is an invariant on (N 1 , m 1 ), meaning that for all firing sequence such that (N 1 , m 1 ) = ⇒ (N 1 , m 1 ) we have m 1 (z) = m 1 (y) + N -K. This can be proved by a simple induction on the length of . Hence, E is satisfied for every reachable marking in (N 1 , m 1 ), and so E is solvable. We now prove the second constraint of condition (A2) for the relation (N 1 , m 1 ) E (N 2 , m 2 ). Assume that (N 1 , m 1 ) = ⇒ (N 1 , m 1 ). We have that is also a firing sequence of (N 2 , m 2 ) and, moreover, (N 2 , m 2 ) = ⇒ (N 2 , m 2 ) such that m 2 (y) = m 1 (y). The proof is similar in the other direction.

Rules [REDT] and [DEADT]

We can use the same approach to simplify transitions in a net, rather than places. One such example is rule [REDT], to remove redundant transitions. Such rules are interesting because, when applied in collaboration with others, they can create new opportunities to apply reductions. We give an example of such mechanism in the example of Sect. 3.5.

Another example is the elimination of dead transitions, rule [DEADT], that can get rid of transitions that are "structurally dead". In this example, we know that place x will always stay empty since no transition can increase its marking. Hence the τ transition is dead and we can remove it without modifying the set of reachable markings nor the observation sequences.

Rules [CONSTANT] and [SOURCE]

Our last examples of rules illustrate the case of equivalences (N 1 , m 1 ) E (N 2 , m 2 ) where the final Petri net is "empty" (denoted ∅). A Petri net with an empty set of places has only one marking; the empty mapping, the only function with domain ∅ → N.

In this case the reachable markings of (N 1 , m 1 ) are exactly defined by the non-negative solutions of system E. Such cases may occur in practice when we can apply several reductions in a row. We say that the initial net is "fully reducible". In example [SOURCE] for instance, we can abstract the state space of the initial net with the single constraint x K.

We have other rules that allow us to fully reduce a net. For instance specific structural or behavioural restrictions, such as nets that are marked graphs or other cases where the set of reachable markings is exactly defined by the solutions of the state equation [START_REF] Hujsa | Checking marking reachability with the state equation in Petri net subclasses[END_REF].

Deriving E-equivalences using reductions

We can compute net reductions by reusing a tool, called REDUCE, that was developed in our previous work [START_REF] Berthomieu | Counting Petri net markings from reduction equations[END_REF] (see also Sect. 6). The tool takes a marked Petri net as input and returns a reduced net and a sequence of linear constraints. For example, given the net M 1 of Fig. 1, REDUCE returns net M 2 and equations (p 5 = p 4 ), (a 1 = p 1 + p 2 ), (a 2 = p 3 + p 4 ), and (a 1 = a 2 ), that corresponds to formula E M in Fig. 1.

The tool works by applying successive reduction rules, in a compositional way. We give an ex-ample of this mechanism in Fig. 7, where we show the four reduction steps involved in our running example. The first step is a direct application of rule [RED] inside a larger context; in each case we use colours to emphasize the sub-net where the rule is applied. The two following ones are variations of rule [CONCAT]. Each rule introducing a fresh "place variable", a 1 and a 2 . Finally, after simplification, we obtain a net with a new opportunity to apply a redundancy rule.

It is possible to prove that each reduction step computed by REDUCE, from a net

(M i , m i ) to (M i+1 , m i+1 ) with constraints E i , is such that (M i , m i ) E i (M i+1 , m i+1
). From Th. 3.5, we have (M 0 , m 0 ) E (M n , m n ), i.e., the results computed by REDUCE always translate into valid polyhedral abstractions.

In conclusion, we can use REDUCE to compute polyhedral abstractions automatically. In the other direction, we can use our notion of equivalence to prove the correctness of new reduction patterns that could be added in the tool. While it is not always possible to reduce the complexity of a net using this approach, we observed in our experiments (Sect. 6) that, on a benchmark suite that includes almost 1 000 instances of nets, about half of them can be reduced by a factor of more than 30%.

SMT-based model checking using abstractions

We introduce a general method for combining polyhedral abstractions with SMT-based model checking procedures. Assume we have (N 1 , m 1 ) E (N 2 , m 2 ), where the nets N 1 , N 2 have sets of places P 1 , P 2 respectively. In the following, we use p 1 (p 1 1 , . . . , p 1 k ) and p 2 (p 2 1 , . . . , p 2 l ) for the places in P 1 and P 2 . We also consider (disjoint) sequences of variables, x and y, ranging over (the places of) N 1 and N 2 . With these notations, we denote Ẽ( x, y) the formula obtained from E where place names in N 1 are replaced with variables in x, and place names in N 2 are replaced with variables in y. When we have the same place in both nets, say p 1 i = p 2 j , we also add the constraint (x i = y j ) to Ẽ in order to avoid shadowing variables. (Remark that Ẽ( p 1 , p 2 ) is equivalent to E, since equalities x i = y j become tautologies in this case.)

Ẽ( x, y) E{ p 1 ← x}{ p 2 ← y} ∧ {(i,j)|p 1 i =p 2 j } (x i = y j ) (6)
Given a formula F , we denote fv (F ) the set of free variables contained in it. Assume F 1 is a property that we want to study on N 1 , without loss of generality we can enforce the condition (fv (F 1 ) \ P 1 ) ∩ (fv (E) \ P 1 ) = ∅ (meaning we can always rename the variables in F 1 and E that are not places in N 1 ). This condition ensures that the property checked on the initial net does not inadvertently contain new variables introduced during the reduction. Definition 4.1. (E-transform formula) Assume (N 1 , m 1 ) E (N 2 , m 2 ) and take F 1 a property with variables in P 1 such that (fv (F 1 ) \ P 1 ) ∩ (fv (E)

\ P 1 ) = ∅. Formula F 2 ( y) ∃ x. Ẽ( x, y) ∧ F 1 ( x) is the E-transform of F 1 .
The following property states that, to check an invariant F 1 on the reachable markings of N 1 , it is enough to check the corresponding E-transform formula F 2 on the reachable markings of N 2 . Since F 1 invariant on N 1 is equivalent to ¬F 1 not reachable, we can directly infer an equivalent conservation theorem for reachability: to find a model of F 1 in N 1 , it is enough to find a model for

F 1 ( p 1 ) ∧ Ẽ( p 1 , p 2 ) in N 2 . Theorem 4.3. (Reachability conservation) Assume (N 1 , m 1 ) (N 2 , m 2 ) and that F 2 is the E-transform of formula F 1 on N 1 . Then formula F 1 is reachable in N 1 if and only if F 2 is reachable in N 2 .
Proof: Assume (N 1 , m 1 ) E (N 2 , m 2 ) and property F 1 is reachable in N 1 . Hence, there exists a reachable marking m 1 in N 1 such that m 1 |= F 1 . By definition of E-abstraction, we have at least one reachable marking

m 2 in N 1 such that m 1 m 2 |= E. The condition m 1 m 2 |= E is equivalent to m 1 ( p 1 ) ∧ m 2 ( p 2 ) ∧ E satisfiable. By definition we have Ẽ( p 1 , p 2 ) ≡ E, which implies m 1 ∧ m 2 ∧ Ẽ( p 1 , p 2 ) ∧ F 1 ( p 1
) satisfiable, since the only variables that are both in F 1 and E must also be in N 1 . Hence, m 2 satisfies the E-transform formula of F 1 . The proof is similar in the other direction.

BMC and PDR implementation

We developed a prototype model checker that takes advantage of net reductions. The tool includes two main verification procedures that have been developed for generalized Petri nets. (No specific optimizations are applied when we know the net is safe, like for instance using Boolean formulas instead of QF-LIA.) These procedures correspond to instantiations of the BMC and PDR methods for checking general reachability properties on Petri nets. We sketch these two procedures below.

Encoding Petri nets semantics using Linear Integer Arithmetic

Our approach is based on a revisit of the semantics of Petri nets using Linear Integer Arithmetic formulas.

We already defined (Sect. 2) a helper formula, or operator, ENBL t ( x) such that ENBL t ( x)∧m( x) is true when t is enabled at m. We can define, in the same way, a linear predicate to describe the relation between the markings before and after some transition t fires. To this end, we use a vector x of "primed variables" (x 1 , . . . , x n ), where x i will stand for the marking of place p i after a transition is fired.

With this convention, formula

FIRE t ( x, x ) is such that FIRE t (m, m ) entails m t - → m when t is enabled at m, or m = m .
With all these notations, we can define a predicate T( x, x ) that "encodes" the effect of firing at most one transition in the net N . By construction, formula m( x)

∧ T( x, x ) ∧ m ( x ) is true when m -→ m , or when m = m . ENBL t ( x) i∈1..n (x i Pre(t)(p i )) (7)
∆ t ( x, x ) i∈1..n (x i = x i + Post(t, p i ) -Pre(t, p i )) (8) EQ( x, x ) i∈1..n x i = x i (9) FIRE t ( x, x ) EQ( x, x ) ∨ ENBL t ( x) ∧ ∆ t ( x, x ) (10)
T( x, x ) EQ( x, x ) ∨ t∈T (ENBL t ( x) ∧ ∆ t ( x, x )) (11)

Bounded Model Checking (BMC)

BMC is an iterative method for exploring the state space of finite-state systems by unrolling their transitions [START_REF] Biere | Symbolic Model Checking without BDDs[END_REF]. The method was originally based on an encoding of transition systems into (a family of) propositional logic formulas and the use of SAT solvers to check these formulas for satisfiability [START_REF] Clarke | Bounded Model Checking Using Satisfiability Solving[END_REF]. There are several works that adapt BMC to Petri nets, such as [START_REF] Heljanko | Bounded Reachability Checking with Process Semantics[END_REF]. More recently, this approach was extended to more expressive models, and richer theories, using SMT solvers [START_REF] Armando | Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers[END_REF]. Our goal is not to develop a state of the art BMC model checker for generalized Petri nets. Instead, we develop a textbook implementation that is enough to test the impact on performances when using reductions.

Description of the algorithm

In BMC, we try to find a reachable marking m that is a model for a given formula F , that usually models a set of "feared events". The algorithm (see function BMC) starts by computing a formula, say φ 0 , representing the initial marking and checking whether φ 0 ∧ F is satisfiable (meaning F is initially true). If the formula is unsatisfiable, we compute a formula φ 1 representing all the markings reachable in one step, or less, from the initial marking and check φ 1 ∧ F . This way, we compute a sequence of formulas (φ i ) i∈N until either φ i ∧F is satisfiable (in which case a counter-example is found) or we have φ i+1 ⇒ φ i (in which case we reach a fixed point and no counter-example exists). The BMC method is not complete since it is not possible, in general, to bound the number of iterations needed to give an answer. Also, when the net is unbounded, we may very well have an infinite sequence of formulas φ 0 φ 1 . . . However, in practice, this method can be very efficient to find a counter-example when it exists. The crux of the method is to compute formulas φ i that represent the set of markings reachable using firing sequences of length at most i. We show how we can build such formulas incrementally. We assume that we have a marked net (N, m 0 ) with places P = {p 1 , . . . , p n } and transitions T = {t 1 , . . . , t k }. In the remainder of this section, we build formulas that express constraints between markings m and m such that m → m in N . Hence we define formulas with 2 n variables. We use the notation ψ( x, x ) as a shorthand for ψ(x 1 , . . . , x n , x 1 , . . . , x n ).

Formula φ i is the result of connecting i successive occurrences of formulas of the form T( x j , x j+1 ). We define the formulas inductively, with a base case (φ 0 ) which states that only m 0 is reachable initially. To define the φ i 's, we assume that we have a collection of (pairwise disjoint) sequences of variables, ( x i ) i∈N . In the following listings, we use the auxiliary function freshVariables to iterate over this family of variable vectors.

φ 0 (N, m 0 ) m 0 ( x 0 ) φ i+1 (N, m 0 ) φ i (N, m 0 ) ∧ T( x i , x i+1 )
Function BMC(EF F : linear predicate) Result: if F is reachable (meaning ¬F is not an invariant)

1 x ← freshVariables() 2 φ ← m 0 ( x) 3 while unsat(m 0 ( x) ∧ φ ∧ (¬F )( x)) do 4
x ← freshVariables()

5 φ ← φ ∧ T ( x, x ) 6 x ← x 7 return
We can prove that this family of BMC formulas provide a way to check reachability properties, meaning that formula F is reachable in (N, m 0 ) if and only if there exists i 0 such that F ( x i ) ∧ φ i (N, m 0 ) is satisfiable. The approach we describe here is well-known (see for instance [START_REF] Biere | Symbolic Model Checking without BDDs[END_REF]). It is also quite simplified. Actual model checkers that rely on BMC apply several optimization techniques, such as compositional reasoning; acceleration methods; or the use of invariants on the underlying model to add extra constraints. We do not consider such optimizations here, on purpose, since our motivation is to study the impact of polyhedral abstractions. We believe that our use of reductions is orthogonal and does not overlap with many of these optimizations, in the sense that we do not preclude them, and that the performance gain we observe with reductions could not be obtained with these optimizations.

Combination with polyhedral abstraction

Assume we have (N 1 , m 1 ) E (N 2 , m 2 ). We denote T 1 , T 2 the equivalent of formula T, above, for the nets N 1 , N 2 respectively. We also use x, y for sequences of variables ranging over (the places of) N 1 and N 2 respectively. We should use φ(N 1 , m 1 ) for the family of formulas built using operator T 1 and variables x 0 , x 1 , . . . and similarly for φ(N 2 , m 2 ), where we use T 2 and variables of the form y i .

The following property states that, to find a model of F in the reachable markings of N 1 (meaning EF F true), it is enough to find a model for its E-transform in N 2 .

Theorem 5.1. (BMC with E-transform) Assume (N 1 , m 1 ) E (N 2 , m 2 ) and that F 2 is the E-transform of F 1 . Formula F 1 is reachable in N 1 if and only if there exists j 0 such that F 2 ( y j ) ∧ φ j (N 2 , m 2 ) is satisfiable.

Proof:

Our proof relies on the property that BMC is sound and complete for finding a finite counter-example (see e.g. [START_REF] Cimatti | Infinite-state invariant checking with IC3 and predicate abstraction[END_REF]): there is a firing sequence , of size less than i, such that

m 1 = ⇒ m 1 and m 1 |= F 1 - meaning property F 1 is reachable in N 1 -if and only if F 1 ∧ φ i (N 1 , m 1 )
. We can prove this property by induction on the value of i and use the fact that m = ⇒ m or m = m in N 1 entails T 1 (m, m ).

By our conservation of reachability theorem (Th. 4.3), property F 1 is reachable in N 1 (say with a counter-example of size i) if and only if property F 2 is reachable in N 2 (say with a counter-example of size j). Therefore there exists i such that F 1 ( x i ) ∧ φ i (N 1 , m 1 ) is satisfiable if and only if there exists j such that F 2 ( y j ) ∧ φ j (N 2 , m 2 ) is satisfiable.

We can give a stronger result, comparing the value of i and j, when the reductions used in proving the E-abstraction equivalence never introduce new transitions. This is the case, for example, with the reductions computed using the REDUCE tool. Indeed, in this case, we can show that we may find a witness of length i in N 1 (a firing sequence of length i showing that F 1 is reachable in N 1 ) when we find a witness of length j i in N 2 . This is because, in this case, reductions may compact a sequence of several transitions into a single one or, at worst, not change it. Take the example of the [CONCAT] rule in Fig. 7. Therefore BMC benefits from reductions in two ways. First because we can reduce the size of formulas φ (which are proportional to the size of the net), but also because we can accelerate transition unrolling in the reduced net.

Property Directed Reachability (PDR)

While BMC is the right choice when we try to find counter-examples, it usually performs poorly when we want to check an invariant property, AG F . There are techniques that are better suited to prove inductive invariants in a transition system; that is a property that is true initially and stays true after firing any transition.

In order to check invariants with SMPT, we have implemented a method called PDR [START_REF] Bradley | SAT-Based Model Checking without Unrolling[END_REF][START_REF] Bradley | Understanding IC3. In: Theory and Applications of Satisfiability Testing (SAT)[END_REF] (also known as IC3), which incrementally generates clauses that are inductive "relative to stepwise approximate reachability information". PDR is a combination of induction, over-approximation, and SAT solving. For SMPT, we developed a similar method that uses SMT solving, to deal with markings and transitions, and that can take advantage of polyhedral abstractions.

As with BMC, our focus is not to study the performances of PDR per se, but its combination with polyhedral abstractions. We give more details about our adaptation of PDR for generalized Petri nets in [START_REF] Amat | Property Directed Reachability for Generalized Petri Nets[END_REF]. We keep enough information about our implementation in order to state an equivalent of Th. 5.1 for PDR.

We use similar notations as with BMC, but with a small difference. Indeed, since PDR "unrolls at most one transition" at a time, we only need two vectors of variables instead of a family ( x i ) i 0 like with BMC: we use unprimed variables ( x) to represent states before firing a transition and primed variables ( x ) to represent the reached states.

PDR requires to define a set of safe states, described as the models of some property F . It also requires a set of initial states, I. In our case I m 0 .

The procedure is complete for finite transition systems, for instance with bounded Petri nets. We can also prove termination in the general case when property ¬F is monotonic, meaning that m |= ¬F implies that m |= ¬F for all markings m that cover m (that is when m m, component-wise). An intuition is that it is enough, in this case, to check the property on the minimal coverability set of the net, which is always finite (see e.g. [START_REF] Finkel | The minimal coverability graph for Petri nets[END_REF]).

A formula F is inductive [START_REF] Bradley | Understanding IC3. In: Theory and Applications of Satisfiability Testing (SAT)[END_REF] when

I( x) ⇒ F ( x) and F ( x) ∧ T( x, x ) ⇒ F ( x ) are tautologies. It is inductive relative to formula G if both I( x) ⇒ F ( x) and G( x)∧F ( x)∧T( x, x ) ⇒ F ( x ) are tautolo- gies.
With PDR we compute Over Approximated Reachability Sequences (OARS), meaning sequences of formulas (F 0 , . . . , F k+1 ), with variables in x, that are monotonic:

I( x) ⇒ F 0 ( x), F i ( x) ⇒ F i+1 ( x)
for all i ∈ 0..k, and F k+1 ⇒ F ; and satisfies consecution:

F i ( x)∧T( x, x ) ⇒ F i+1 ( x ) for all i k+1.
The formulas F i change at each iteration of the procedure (each time we increase k). The procedure stops when we find an index i such that F i = F i+1 . In this case we know that F is an invariant. We can also stop during the iteration if we find a counter-example.

Description of the algorithm

Our implementation follows closely the algorithm for IC3 described in [START_REF] Bradley | Understanding IC3. In: Theory and Applications of Satisfiability Testing (SAT)[END_REF]. We only give the pseudo-code for the four main functions (prove, strengthen, inductivelyGeneralize and pushGeneralization).

The main function, prove, computes an Over Approximated Reachability Sequence (OARS) (F 0 , . . . , F k+1 ) of linear predicates, called frames, with variables in x. An OARS meets the following constraints: (1) it is monotonic: F i ( x) ∧ ¬F i+1 ( x) is unsatisfiable, for all i ∈ 0..k; (2) it contains the initial states: I( x) ∧ ¬F 0 ( x) is unsatisfiable; (3) it does not contain feared states: F k+1 ( x) ∧ ¬F ( x) is unsatisfiable; and (4) it satisfies consecution:

F i ( x) ∧ T( x, x ) ∧ ¬F i+1 ( x ) is unsatisfiable for all i ∈ 0..k + 1.
By construction, each frame F i in the OARS is defined as a set of clauses, CL(F i ), meaning that F i is built as a formula in CNF: F i = cl∈CL(F i ) cl . We also enforce that CL(F i+1 ) ⊆ CL(F i ) for all i ∈ 0..k, which means that the monotonicity property between frames is trivially ensured.

The body of function prove contains a main iteration (line 4) that increases the value of k (the number of levels of the OARS). At each step, we enter a second, minor iteration (line 2 in function strengthen), where we generate new minimal inductive clauses that will be propagated to all the frames. Hence both the length of the OARS, and the set of clauses in its frames, increase during computation. The procedure stops when we find an index i such that F i = F i+1 . In this case we know that F i is an inductive invariant satisfying F . We can also stop during the iteration if we find a counter-example (a model m of ¬F ). In this case, we can also return a trace leading to m.

When we start the first minor iteration, we have k = 1, F 0 = I and F 1 = F . If we have F k ( x) ∧ T ( x, x ) ∧ (¬F )( x ) unsatisfiable, it means that F is inductive, so we can stop and return that F is an invariant. Otherwise, we proceed with the strengthen phase, where each model of F k ( x) ∧ T ( x, x ) ∧ (¬F )( x ) becomes a potential counter-example, or witness, that we need to "block" (line 3-5 of function strengthen).

Function prove(AG F : linear predicate)

Result: if F is an invariant, otherwise ⊥ (meaning ¬F is reachable)

1 if sat(I( x) ∧ T ( x, x ) ∧ (¬F )( x )) then 2 return ⊥ 3 k ← 1, F 0 ← I, F 1 ← F 4 while do 5 if strengthen(k) then 6 return ⊥ 7 propagateClauses(k) 8 if CL(F i ) = CL(F i+1 ) for some 1 i k then 9 return 10 k ← k + 1
Function strengthen(k : current level) Instead of blocking only one witness (and to overcome the problem with a potential infinite number of witnesses), we first generalize it into a predicate that abstracts similar dangerous states (see the calls to generalizeWitness). We define the formula m( x) i∈1..n (x i ≥ m(p i )) that is valid for every marking that covers m; in the sense that m |= m only when m m. By virtue of the monotonicity of the flow function of Petri nets, when ¬F is monotonic and m is a witness, we know that all models of m are also witnesses. Hence we can improve the method by generating a minimal inductive clause (MIC) from ¬ m instead of ¬m. Another benefit of this choice is that m( x) is a conjunction of inequalities of the form (x j k i ), which greatly simplifies the computation of the MIC. When F is anti-monotonic (¬F is monotonic), we can prove the completeness of the procedure using an adaptation of Dickson's lemma, which states that we cannot find an infinite decreasing chain of witnesses (but the number of possible witness may be extremely large). Hence, when we block it, we learn new clauses from ¬ m that can be propagated to the previous frames.

1 try: 2 while (m t -→ m ) |= F k ( x) ∧ T ( x, x ) ∧ (¬F )( x ) do 3 m ← generalizeWitness(m) 4 n ← inductivelyGeneralize( m, k -2, k)
Before pushing a new clause, we test whether m is reachable from previous frames. We take advantage of this opportunity to find if we have a counter-example and, if not, to learn new clauses in

Combination with polyhedral abstraction

Assume we have (N 1 , m 1 ) E (N 2 , m 2 ) and that G 2 is the E-transform of formula G 1 on N 1 . We also assume that G 1 and G 2 are anti-monotonic (meaning ¬G 1 and ¬G 2 monotonic), in order to ensure the termination of the PDR procedure. (We can prove that Ẽ is monotonic for systems E computed with the REDUCE tool when the initial net does not use inhibitor arcs.) To check that formula G 1 is an invariant on N 1 (meaning AG G 1 true), it is enough [START_REF] Bradley | SAT-Based Model Checking without Unrolling[END_REF] to incrementally build OARS (F 0 , . . . , F k+1 ) on N 1 until F i = F i+1 for some index i ∈ 0..k. In this context, F 0 = m 1 and F k+1 ⇒ G 1 . In a similar way than with our extension of BMC with reductions, a corollary of our invariant conservation theorem (Th. 4.2) is that, to check that G 1 is an invariant on N 1 , it is enough to build OARS (F 0 , . . . , F l+1 ) on N 2 where F 0 = m 2 and F l+1 ⇒ G 2 .

Theorem 5.2. (PDR with E-transform) Assume (N 1 , m 1 ) E (N 2 , m 2 ) and that G 2 is the E-transform of G 1 , both anti-monotonic formulas. Formula G 1 is an invariant on N 1 if and only if there exists i 0 such that F i = F i+1 in the OARS built from net N 2 and formula G 2 .

Proof:

Our proof relies on the property that PDR is sound and complete for finite-state systems, see for instance Th. 1 in [START_REF] Bradley | SAT-Based Model Checking without Unrolling[END_REF]: G 1 is an invariant on (N 1 , m 1 ) if and only if there exists i 0 such that F i = F i+1 . Since we deal with monotonic formulas (in this case the feared states ¬G 1 and ¬G 2 ), the set of markings satisfying a frame F i is always upward-closed (if m |= F i and m m then also m |= F i ), and therefore we can work on the coverability graph of the net, instead on its actual marking graph, which is finite [START_REF] Finkel | The minimal coverability graph for Petri nets[END_REF]. The results follows from our invariant conservation theorem (Th. 4.2).

Combination of BMC and PDR

In the next section (Sect.6), we report on the results obtained with our implementation of BMC and PDR (with and without reductions), on an independent and comprehensive set of benchmarks.

With PDR, we restrict ourselves to the proof of liveness properties, EF φ where φ is monotonic (or equivalently, invariants AG φ with φ anti-monotonic). In practice, we do not check if φ is monotonic using our "semantical" definition. Instead, our implementation uses a syntactical restriction that is a sufficient condition for monotonicity. This is the case, for example, when testing the quasi-liveness of a set of transitions. On the other hand, deadlock is not monotonic. In such cases, we can only rely on the BMC procedure, which may not terminate if the net has no deadlocks. Hence, our bestcase scenario is when we check a monotonic property (or if a model for the property exists). In our benchmarks, we find that almost 30% of all the properties are monotonic.

We have plans to improve our PDR procedure to increase the set of properties that can be handled. In particular, we know how to do better when the net is k-bounded (and we know the value of k). We also have several proposals to improve the computation of a good witness, and its MIC, in the general case. We should explore all these ideas in a future work.

Experimental results

We have implemented the approach described in Sect. 5 into a new tool, called SMPT (for Satisfiability Modulo P/T Nets). The tool is open-source, under the GPLv3 license, and is freely available on GitHub (https://github.com/nicolasAmat/SMPT/). In this section, we report on some experimental results obtained with SMPT (v2) on an extensive benchmark of models and formulas provided by the Model Checking Contest (MCC) [START_REF] Amparore | Presentation of the 9th Edition of the Model Checking Contest[END_REF][START_REF] Hillah | Petri Nets Repository: A Tool to Benchmark and Debug Petri Net Tools[END_REF].

SMPT serves as a front-end to generic SMT solvers, such as z3 [START_REF] De Moura | Z3: An Efficient SMT Solver[END_REF][START_REF] Bjørner | The Z3 Theorem Prover[END_REF]. The tool can output sets of constraints using the SMT-LIB format [START_REF] Barrett | The SMT-LIB Standard: Version 2[END_REF] and pipe them to a z3 process through the standard input. We have implemented our tool with the goal to be as interoperable as possible, but we have not conducted experiments with other solvers yet.

SMPT takes as inputs Petri nets defined using the .net format of the TINA toolbox and can therefore also accept nets defined using the PNML syntax. For formulas, we accept properties defined with the XML syntax used in the MCC competition. The tool does not compute net reductions directly but relies on the tool REDUCE, that we described at the end of Sect. 3.

The tool REDUCE is distributed with the standard distribution of the TINA toolbox, which includes the most mature versions of our verification tools. We also provide an open source, feature complete version of an equivalent tool, called SHRINK (https://github.com/Fomys/pnets), that provide several Rust libraries for manipulating Petri nets and performing structural reductions.

Benchmarks and distribution of reduction ratios

Our benchmark suite is built from a collection of 102 models used in the MCC competition. Most of the models are parametrized, and therefore there can be several different instances for the same model. There are about 1 000 different instances of Petri nets whose size vary widely, from 9 to 50 000 places, and from 7 to 200 000 transitions. Most nets are ordinary (non-zero weights on all arcs are equal to 1), but a significant number of instances (about 150) use weighted arcs. Overall, the collection provides a large number of examples with various structural and behavioral characteristics, covering a large variety of use cases.

Since our approach relies on the use of net reductions, it is natural to wonder if reductions occur in practice. To answer this question, we computed the reduction ratio (r), obtained using REDUCE, as a quotient between the number of places before (p init ) and after (p red ) reduction: r = (p init -p red )/p init . We display the results for the whole collection of instances in Fig. 8, sorted in descending order.

A ratio of 100% (r = 1) means that the net is fully reduced; the resulting net has only one (empty) marking. We see that there is a surprisingly high number of models that are totally reducible with our approach (about 20% of the total number), with approximately half of the instances that can be reduced by a ratio of 30% or more.

For each edition of the MCC, a collection of about 30 random reachability properties are generated for each instance. We evaluated the performance of SMPT using the formulas of the MCC'2020, on a selection of 426 Petri nets taken from instances with a reduction ratio greater than 1%. (To avoid any bias introduced by models with a large number of instances, we selected at most 5 instances with a similar reduction ratio from each model.) Figure 8: Distribution of reduction ratios over the instances in the MCC A pair of an instance and a formula is called a test case. For each test case, we check the formulas with and without the help of reductions (using both the BMC and PDR methods in parallel) and with a fixed timeout of 120 s. This adds up to a total of 13 265 test cases which required the equivalent of 447 hours of CPU time.

Impact on the number of solvable queries

We report our results in the table of Fig. 9. Out of the almost 13 000 test cases, we were able to compute approximately 7 000 results using reductions and only 3 555 without reductions (so approximately twice more).

We compared our results with the ones provided by an oracle [START_REF] Thierry-Mieg | Oracle for the MCC[END_REF], which gives the expected answer (as computed by a majority of tools, using different techniques, during the MCC competition). We achieve 100% reliability on the benchmark; meaning we always give the answer predicted by the oracle.

We give the number of computed results for four different categories of test cases: Full contains only the fully reducible instances (the best possible case with our approach); while Low/Good/High correspond to instances with a low/moderate/high level of reduction. We chose the limits for these categories in order to obtain samples with comparable sizes. We also have a general category, All, for the complete set of benchmarks.

We observe that we are able to compute almost twice as many results when we use reductions than without. This gain is greater on the High (×3.1) than on the Good (×1.7) instances. Nonetheless, the fact that the number of additional queries solved using reductions is still substantial, even for a reduction ratio under 50%, indicates that our approach can benefit from all the reductions we can find in a model (and that our results are not skewed by the large number of fully reducible instances).

In the special case of fully reducible nets, checking a query amounts to solving a linear system on the initial marking of the reduced net. There are no iterations. Moreover this is the same system for both the BMC and PDR procedures. For this category, we are able to compute a result for all but one of the queries (that could be computed using a timeout of 180 s). Most of these queries can be solved in less than a few seconds.

When the distinction makes sense, we also report the number of cases solved using BMC/PDR. (As said previously, the two procedures coincide in category Full, with reductions.) We observe that the contribution of PDR is poor. This can be explained by several factors. First, we restricted our implementation of PDR to monotonic formulas (which represents 30% of all properties). Among these, PDR is useful only when we have an invariant that is true (meaning BMC will certainly not terminate). On the other hand, PDR is able to give answers on the most complex cases. Indeed, it is much more difficult to prove an invariant than to find a counter-example (and we have other means to try and find counter-examples, like simulation for instance). This is why we intend to improve the performances and the "expressiveness" of our PDR implementation. Another factor, already observed in [START_REF] Thierry-Mieg | Structural Reductions Revisited[END_REF], is the existence of a bias in the MCC benchmark: in more than 60% of the cases, the result follows from finding a counter-example (meaning an invariant that is false or a reachability property that is true).

Impact on computation time

To better understand the impact of reductions on the computation time, we compare the computation time, with or without reductions, for each test case. These results do not take into account the time spent for reducing each instance. This time is negligible when compared to each test, usually in the order of 1 s. Also, we only need to reduce the net once when checking the 30 properties for the same instance. We display our results in Fig. 10, where we give four scatter plots comparing the computation time "with" (y-axis) and "without" reductions (x-axis), for the Low, Good, High and Full categories of instances. Each chart uses a logarithmic scale. We also display a histogram, for each axis on the charts, that gives the density of points for a given duration. To avoid overplotting, we removed all the "trivial" properties (the bottom left part of the chart), that can be computed with and without reduction in less than 10 ms. These "trivial" queries (507 in total) correspond to instances with a small state space or to situations where a counter-example can be found very quickly.

We observe that almost all the data points are below the diagonal, meaning reductions accelerate the computation, with many test cases exhibiting speed-ups larger than ×100. We have added two light-coloured, dashed lines to materialize data points with speed-ups larger than ×10 and ×100 respectively. On our 13 265 test cases, we timeout with reductions but compute a result without on only 51 cases (0.4%). These exceptions can be explained by border cases where the order in which transitions are processed has a sizeable impact.

Another interesting point is the ratio of properties that can be computed only using reductions. This is best viewed when looking at the histogram values. A vast majority of the points in the charts are either on the right border (computation without reductions timeout) or on the x-axis (they can be computed in less than 10 ms using reductions).

Related work and conclusion

We propose a new method to combine structural reductions with SMT solving in order to check invariants on arbitrary Petri nets. While this idea is not original, the framework we developed is new. Our main innovation resides in the use of a principled approach, where we can trace back reachable markings (between an initial net and its residual) by means of a conjunction of linear equalities (the formula Ẽ). Basically, we show that we can adapt a SMT-based procedure for checking a property on a net (that relies on computing a family of formulas of the form (φ i ) i∈I ) into a procedure that relies on a reduced version of the net and formulas of the form (φ i ∧ Ẽ) i∈J .

As a proof of concept, we apply our approach to two basic implementations of the BMC and PDR procedures. Our empirical evaluation shows promising results. For example, we observe that we are able to compute twice as many results using reductions than without. We believe that our approach can be adapted to more decision procedures and could easily accommodate various types of optimizations.

Related work

Our main theoretical results (the conservation theorems of Sect. 4) can be interpreted as examples of reduction theorems [START_REF] Lipton | Reduction: a method of proving properties of parallel programs[END_REF][START_REF] Cohen | Reduction in TLA[END_REF], that allow to deduce properties of an initial model (N ) from properties of a simpler, coarser-grained version (N R ). While these works are related, they mainly focus on reductions where one can group a sequence of transitions into a single, atomic action. Hence, in our context, they correspond to a restricted class of reductions, similar to a subset of the agglomeration rules used in [START_REF] Berthomieu | Counting Petri net markings from reduction equations[END_REF].

We can also mention approaches where the system is simplified with respect to a given property, for instance by eliminating parts that cannot contribute to its truth value, like with the slicing or Cone of Influence abstractions [START_REF] Clarke | Model Checking[END_REF] used in some model checkers. Finding such "parts" (places and transitions) in a Petri net is not always easy, especially when the formula involves many places. This is not a problem with our approach, since we can always abstract away a place, as long as its effect is preserved in the E-transform formula.

In [START_REF] Schmidt | Using Petri Net Invariants in State Space Construction[END_REF], the author uses net invariants to compress the representation of markings. This approach is based on the fact that place invariants provide linear constraints between the markings of several places; like in our use of redundancy rules. But the goal is to reduce the memory footprint when computing the explicit state space, while verification is still performed on "uncompressed" markings.

On the contrary, our approach can be used with symbolic methods-working on a reduced version of the net-and can use more general rules. For instance, it cannot benefit from rules that agglomerate places.

In practice, we derive polyhedral abstractions using structural reductions, a concept introduced by Berthelot in [START_REF] Berthelot | Transformations and Decompositions of Nets[END_REF]. In our work, we are interested in reductions that preserve the reachable states. This is in contrast with most works about reductions, where more powerful transformations can be applied when we focus on specific properties, such as the absence of deadlocks. Several tools use reductions for checking reachability properties. TAPAAL [START_REF] Bønneland | Stubborn versus structural reductions for Petri nets[END_REF], for instance, is an explicit-state model checker that combines Partial-Order Reduction techniques and structural reductions and can check properties on Petri nets with weighted arcs and inhibitor arcs.

A more relevant example is ITS Tools [START_REF] Thierry-Mieg | Structural Reductions Revisited[END_REF][START_REF] Thierry-Mieg | Symbolic and Structural Model-Checking[END_REF], which combines several techniques, including structural reductions and the use of SAT and SMT solvers. This tool relies on efficient methods for finding counter-examples-with the goal to invalidate an invariant-based on the collaboration between pseudo-random exploration techniques; hints computed by an SMT engine; and reductions that may simplify atoms in the property or places and transitions in the net. It also describes a semi-decision procedure, based on an over-approximation of the state space, that may detect when an invariant holds (by ruling out infeasible behaviours). This leads to a very efficient tool, able to compute a result for most of the queries in our benchmark, when we solve only 52% of our test cases. Nonetheless, we are able to solve 46 queries with SMPT (with a timeout of 120 s) that are not in the oracle results collected from ITS Tools [START_REF] Thierry-Mieg | Oracle for the MCC[END_REF]; which means that no other tool was able to compute a result on these queries.

It has to be kept in mind, though, that our goal is to study the impact of polyhedral abstraction, in isolation from other techniques. However, the methods described in [START_REF] Thierry-Mieg | Structural Reductions Revisited[END_REF] provide many ideas for improving our approach, such as: using linear arithmetic over reals-which is more tractable than integer arithmetic-to over-approximate the state space of a net; adding extra constraints to strengthen invariants (for instance using the state equation or constraints derived from traps); dividing up a formula into smaller sub-parts, and checking them incrementally or separately; . . . But the main lesson to be learned is that there is a need for a complete decision procedure devoted to the proof of satisfiable invariants, which further our interest in improving our implementation of PDR.

A byproduct of our work is to provide a partial implementation of PDR that is correct and complete when the property is monotonic (see Sect. 4), even in the case of nets with an infinite state space. Our current solution can be understood as a restriction to the case of "coverability properties", which seems to be the current state-of-the-art with Petri nets; see for example [START_REF] Esparza | An SMT-Based Approach to Coverability Analysis[END_REF] and [START_REF] Kang | Abstraction-Based Incremental Inductive Coverability for Petri Nets[END_REF], or the extension of PDR to "well-structured transition systems" [START_REF] Kloos | Incremental, Inductive Coverability[END_REF]. The reachability problem for Petri nets or, equivalently, for Vector Addition Systems with States (VASS) is decidable [START_REF] Kosaraju | Decidability of Reachability in Vector Addition Systems (Preliminary Version)[END_REF]. Even if this result is based on a constructive proof, and its "construction" streamlined over time [START_REF] Leroux | The general vector addition system reachability problem by Presburger inductive invariants[END_REF], the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney approach does not lead to a workable algorithm. It is in fact a feat that this algorithm has been implemented at all, see e.g. the tool KREACH [START_REF] Dixon | KReach: A Tool for Reachability in Petri Nets[END_REF]. While the (very high) complexity of the problem means that no single algorithm could work efficiently on all inputs, it does not prevent the existence of methods that work well on some classes of problems. For example, several algorithms are tailored for the discovery of counter-examples. We can mention the tool FASTFORWARD [START_REF] Blondin | Directed Reachability for Infinite-State Systems[END_REF], that explicitly targets the case of unbounded nets. We can also mention the works on inductive procedures for infinite-state and/or parametrized systems, such as the verification methods used in Cubicle [START_REF] Conchon | Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems[END_REF]; see also [START_REF] Cimatti | Infinite-state invariant checking with IC3 and predicate abstraction[END_REF][START_REF] Gurfinkel | SMT-based verification of parameterized systems[END_REF].

Follow up work

We propose a new method that adapts our approach-initially developed for model checking with decision diagrams [START_REF] Berthomieu | Petri net reductions for counting markings[END_REF][START_REF] Berthomieu | Counting Petri net markings from reduction equations[END_REF]-for use with SMT solvers.

We have continued working with our polyhedral abstraction since our initial publication in [START_REF] Amat | On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets[END_REF]. In particular, we tried applying our approach to the verification of properties more complex than reachability, like with our recent work on the concurrent places problem [START_REF] Amat | Accelerating the Computation of Dead and Concurrent Places Using Reductions[END_REF]. The problem, in this case, is to enumerate all pairs of places that can be marked together, for some reachable states. In this work we defined a new data-structure that precisely captures the structure of reduction constraints, what we call the Token Flow Graph (TFG), and we used the TFGs to accelerate the computation of the concurrency relation

We also continued improving our adaptation of PDR, which is the most promising part of our work and raises several interesting theoretical problems. In this context, we recently proposed two new adaptions of PDR, to deal with non-monotonic formulas [START_REF] Amat | Property Directed Reachability for Generalized Petri Nets[END_REF]. But there is still a lot of work to be done, like for instance concerning the completeness of our new approach and/or its limits.

Future work

There is still ample room for improving our tool. We already mentioned some ideas for enhancements that we could borrow from ITS Tools, but we also plan to specialize our verification procedures in some specific cases, for example when we know that a net is 1-safe. A first step should be to compare our performances with other tools in more details. This is what motivates our participation to the next edition of the MCC, with SMPT alone in the reachability examinations, even though it is common knowledge that winning tools need to combine several different techniques.

On a more theoretical side, we also identified a need to develop an automated (or a semi-automatic) method to prove the correctness of new reduction rules.

Figure 1 :

 1 Figure 1: An example of Petri net, M 1 (left), and one of its polyhedral abstraction, M 2 (right), withE M (p 5 = p 4 ) ∧ (a 1 = p 1 + p 2 ) ∧ (a 2 = p 3 + p 4 ) ∧ (a 1 = a 2 ).

  and symmetrically with •2 on the second component of each transition pair).

3. 3 . 3 .

 33 Preservation by relabeling Another standard operation on labeled Petri nets is relabeling, denoted as N [a/b], that apply a substitution to the labeling function of a net. Assume l is the labeling function over the alphabet Σ. We denote l[a/b] the labeling function on (Σ \ {a}) ∪ {b} such that l[a/b](t) = b when l(t) = a and l[a/b](t) = l(t) otherwise. Then N [a/b] is the same as net N but equipped with labeling function l[a/b].

Figure 2 :

 2 Figure 2: Rule [CONCAT].

Figure 3 :

 3 Figure 3: Rule [AGG].

Figure 4 :

 4 Figure 4: Rule [RED] (above), assuming K N , and rule [SHORTCUT] (below).

Figure 5 :

 5 Figure 5: Rules [REDT] (above), and [DEADT] (below).

Figure 6 :

 6 Figure 6: Rules [CONSTANT] (left) and [SOURCE] (right).

Figure 9 :

 9 Figure 9: Impact of the reduction ratio on the number of solved instances.

1 Figure 10 :

 110 Figure 10: Comparing computation time, "with" (y-axis) and "without" (x-axis) reductions for categories Low (a), Good (b), High (c) and Full (d).

  there is at least one marking m 2 over P 2 such that m 1 m 2 |= E (e.g. solvable), and for all markings m 2 over P 2 such that m 1 m 2 |= E there must exist a firing sequence 2

  Assume (N 1 , m 1 ) E (N 2 , m 2 ) and that F 2 is the E-transform of formula F 1 on N 1 . Then F 1 is an invariant on N 1 if and only if F 2 is an invariant on N 2 . , m 1 ) E (N 2 , m 2 ) and property F 1 is an invariant on N 1 . Consider m 2 a reachable marking in N 2 . By definition of E-abstraction, we have at least one reachable markingm 1 in N 1 such that m 1 m 2 |= E. Since F 1 is an invariant on N 1 we have m 1 |= F 1 . The condition m 1 m 2 |= E is equivalent to m 1 ∧ m 2 ∧ E satisfiable. By definition we have Ẽ( p 1 , p 2 ) ≡ E, which implies m 1 ( p 1 ) ∧ m 2 ( p 2 ) ∧ Ẽ( p 1 , p 2 ) ∧ F 1 ( p 1) satisfiable, since the only variables that are both in F 1 and E must also be in N 1 . Hence, m 2 satisfies the E-transform formula of F 1 . The proof is similar in the other direction.

	Theorem 4.2. (Invariant conservation)
	Proof:
	Assume (N 1		p 1	τ	p 2			p 1	τ	p 2
				t 1					t 1
		p 0		p 4			p 0		p 4
		5	t 0 a		t 3 b	p 5 =p 4	5	t 0 a	t 6 b
	p 6					p 6
	4	t 4		t 2		4	t 4		t 5
		c	p 3	τ	p 5		c	p 3	τ
			p 1	τ	p 2				a 1
				t 1
		p 0		p 4			p 0		p 4
		5	t 0 a		t 6 b	a 1 =p 1 +p 2	5	t 7 a	t 8 b
	p 6					p 6
	4	t 4		t 5		4	t 4		t 5
		c	p 3	τ			c	p 3	τ
				a 1					a 1
		5 p 0	t 7 a	p 4	t 8 b	▷ a 2 =p 3 +p 4	p 0 5	t 9 a	t 10 b
	p 6					p 6
	4	t 4		t 5		4	t 11
		c	p 3	τ			c		a 2
				a 1
		p 0					p 0
		5	t 9 a		t 10 b	a 1 =a 2	5	t 12 a	t 13 b
	p 6					p 6
	4	t 11				4	t 14
		c		a 2			c		a 2
	Figure 7: Example of sequence of four reductions leading from the net N to N from Fig. 1.

Function inductivelyGeneralize(s : cube, min: level, k: level) 1 if min < 0 and sat(F 0 ( x) ∧ T ( x, x ) ∧ s( x )) then 2 raise Counterexample

Function pushGeneralization(states: set of (state, level), k: level)

the process. This is the role of functions pushGeneralization and inductivelyGeneralize.

The goal of inductivelyGeneralize is to strengthen the invariants in (F i ) i k by learning new clauses and finding the smallest index in 1..k that can lead to the dangerous states m. The goal of pushGeneralization is to apply inductive generalization, starting from the earliest possible level. We find a counter example (in the call to inductivelyGeneralize) if the generalization from a witness found at level k, say ŝ, reaches level 0 and F 0 ( x) ∧ T ( x, x ) ∧ ŝ( x ) is satisfiable (line 1 in inductivelyGeneralize). Indeed, it means that we can build a trace from I to ¬F by going through F 1 , . . . , F k .

The method relies heavily on checking the satisfiability of linear formulas in QF-LIA, which is achieved with a call to a SMT solver. In each function call, we need to test if predicates of the form F i ( x) ∧ T ( x, x ) ∧ G( x ) are unsatisfiable and, if not, enumerate its models. To accelerate the strengthening of frames, we also rely on the unsat core of properties in order to compute MIC.