key: cord-0048955-ib6x8wbm
authors: Bozga, Marius; Esparza, Javier; Iosif, Radu; Sifakis, Joseph; Welzel, Christoph
title: Structural Invariants for the Verification of Systems with Parameterized Architectures
date: 2020-03-13
journal: Tools and Algorithms for the Construction and Analysis of Systems
DOI: 10.1007/978-3-030-45190-5_13
sha: 94af93c09e11e041a9c18354beb282dca8006c62
doc_id: 48955
cord_uid: ib6x8wbm

We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata.

The problem of parameterized verification asks whether a system composed of n replicated processes is safe, for all n ≥ 2. By safety we mean that every execution of the system stays clear of a set of global error configurations, such as deadlocks or mutual exclusion violations. Even if we assume each process to be finite-state and every interaction to be a synchronization of actions without exchange of data, ranging over large or infinite domains, the problem remains challenging because we ask for a general proof of safety that works for any number of processes.

Parameterized verification is undecidable, even if processes only manipulate data from a bounded domain [6] . Various restrictions of communication and architecture 3 define decidable subproblems [18, 31, 27, 5] . Seminal works consider rendez-vous communication, with participants placed in a ring [18, 27] or a clique [31] of arbitrary size. Recently, MSO-definable graphs (with bounded tree-and clique-width) and point-topoint rendez-vous communication have been considered [5] . Most approaches to define decidable problems focus on manually proving a cut-off bound c ≥ 2 such that Institute of Engineering Univ. Grenoble Alpes 3 We use the term architecture for the shape of the graph along which the interactions take place. correctness for at most c processes implies correctness for any number of processes [18, 27, 26, 7, 34] . Other methods identify systems with well-structured transition relations [31, 1, 29] . An exhaustive chart of decidability results for verification of parameterized systems is drawn in [12] . When decidability is not of concern, over-approximation and semi-algorithmic techniques such as regular model checking [36, 2] , SMT-based bounded model checking [4, 21] , abstraction [10, 14] and automata learning [19] can be used to deal with more general classes of systems.

The efficiency of a verification method crucially relies on its ability to synthesize an inductive safety invariant, i.e., an infinite set of configurations that contains the initial configurations, is closed under the transition relation, and excludes the error configurations. In general, automatically synthesizing invariants requires computationally expensive fixpoint iterations [22] . In the particular case of parameterized systems, invariants can be either global, relating the local states of all processes [23] , or modular, relating the local states of a few processes whose identity is irrelevant [38, 20] . Our Contributions. The novelty of the approach described in this paper is three-fold:

1. The architecture of the system is not fixed a priori, but given as a parameter of the verification problem. In fact, we describe parameterized systems using the Behavior-Interaction-Priorities (BIP) framework [9] , in which processes are instances of finite-state component types, whose interfaces are sets of ports, labeling transitions between local states, and interactions are sets of strongly synchronizing ports, described by formulae of an interaction logic. An interaction formula captures the architecture of the interactions (pipeline, ring, clique, tree) and the communication scheme (rendez-vous, broadcast), which are not hardcoded, but rather specified by the designer of the system. 2. We synthesize parameterized invariants directly from the interaction formula of a system, without iterating its transition relation. Such invariants depend only on the structure (and not on the operational semantics) of an infinite family of Petri Nets, one for each instance of the system, and are thus structural invariants. Essentially, the invariants we infer use the traps 4 of the system, which are sets W of local states with the property that, if a process is initially in a state from W, then always some process will be in a state from W. Following [11, 17] , we call them (parameterized) trap invariants. Computing trap invariants only requires a simple syntactic transformation of the interaction formula and the result is expressed using WSκS, the weak monadic second order logic of κ ≥ 1 successor functions. Thus invariant computation is very cheap, and the verification problem (proving the emptiness of the intersection between the invariant and the set of error states) is reduced to the unsatisfiability of a WSκS formula with a single quantifier alternation. In practice, this check can be carried out quite efficiently by existing tools, such as Mona [33] . 3. We refine the approach by considering so called 1-invariants, that can also be derived cheaply from the interaction formula of the system. We show that 1-invariants in conjunction with trap invariants successfully verify additional examples. Comparison to related work. Trap invariants have been very successfully used in the verification of non-parameterized systems [11, 28, 13] . The technique was lifted to parameterized systems in [17] , but the work there is only applicable to clique architec-tures, in which processes are indistinguishable, and the system can be described by one single Petri Net with an infinite family of initial markings. Here, for the first time, we show that the trap technique can be extended to pipelines, token rings and trees, where the system is defined by an infinite family of Petri Nets, each with a different structure. These systems cannot be analyzed using the techniques of [31, 1, 29] , because they do not yield well-structured transition systems. Contrary to [18, 27, 26, 7, 34] , our approach does not require a manual cut-off proof. Contrary to regular model checking and automata learning [2, 19] , it does not require any symbolic state-space exploration. Finally, our approach produces an explanation of why the property holds in terms of the trap invariant and 1-invariants used. Summarizing, our approach provides a comparatively cheap technique for parameterized verification, that succeeds in numerous cases. It is ideal as preprocessing step that can very quickly lead to success with a very clear explanation of why the property holds, and otherwise provides at least a strong invariant that can be used for further analysis.

Running Example. Consider the dining philosophers system in Fig. 1 , consisting of n ≥ 2 components of type Fork and Philosopher respectively, placed in a ring of size 2n. The k-th philosopher has a left fork, of index k, and a right fork, of index (k + 1) mod n. Each component is an instance of a finite state automaton with states f (ree) and b(usy) for Fork, respectively w(aiting) and e(ating) for Philosopher. A fork goes from state f to b via a t(ake) transition and from f to b via a (eave) transition. A philosopher goes from w to e via a g(et) transition and from e to w via a p(ut) transition. The g action of the k-th philosopher is executed jointly with the t actions of the k-th and [(k + 1) mod n]-th forks, in other words, the philosopher takes both its left and right forks simultaneously. Similarly, the p action of the k-th philosopher is executed simultaneously with the action of the k-th and [(k + 1) mod n]-th forks, i.e. each philosopher leaves both its left and right forks at the same time. We describe these interactions by the interaction formula: Γ philo = (g(i) ∧ t(i) ∧ t(succ(i))) ∨ (p(i) ∧ (i) ∧ (succ(i))) (1) where the free variable i refers at some arbitrary component index.

Intuitively, the transitions of the system with n dining philosophers and n forks are given by the minimal models of the disjuncts of Γ philo with universe {0, 1, . . . , n − 1}, and succ interpreted as "successor modulo n'. In particular, for each 0 ≤ k ≤ n − 1 the first disjunct has a minimal model that interprets the predicates g and t as the sets {k} and {k, (k + 1) mod n}. This model describes the interaction in which the k-th philosopher takes a g-transition (from waiting to eating), while, simultaneously, the k-th and (k + 1)th forks take t-transitions (from free to busy). This is graphically represented by one of the dashed lines in Fig. 1 . Observe that the ring topology of the system is implicit in the modulo-n interpretation of the successor function.

Since philosophers can only grab their two forks simultaneously, the system is deadlock-free for any number n ≥ 2 of philosophers. An automatic proof requires to compute an invariant, and prove that it has an empty intersection with the set of deadlock configurations defined by the WSκS formula deadlock(X w , X e , X f ,

(2) where X w , X e , X f , X b are set variables, the intended meaning of X w (i) resp. X e (i) is that the i-th philosopher is waiting, resp. eating, and the intended meaning of X f (i) resp. X b (i) is that the i-th fork is free, resp. busy. Our method automatically computes from Γ philo a formula trap-invariant S which formalizes an inductive invariant of the system. Moreover, we express the consistency requirement that every component is in one of its state at all times in a formula marking S and derive the deadlock-freeness for any number of philosophers by the unsatisfiability of the formula deadlock ∧ trap-invariant S ∧ marking S .

A component type is a tuple C = P, S, s 0 , ∆ , where P = {p, q, r, . . .} is a finite set of ports, S is a finite set of states, s 0 ∈ S is an initial state and ∆ ⊆ S × P × S is a set of transitions denoted s p − → s , for s, s ∈ S and p ∈ P. We assume there are no two different transitions with the same port.

A component-based system S = C 1 , . . . , C N , Γ consists of a fixed number N ≥ 1 of component types C k = P k , S k , s 0 k , ∆ k and an interaction formula Γ. In the dining philosophers there are two component types, Philosopher and Fork, each with two states and two transitions, as shown in Fig. 1 . We assume that P i ∩P j = ∅ and S i ∩S j = ∅, for all 1 ≤ i < j ≤ N. We denote the component type of a port p or a state s by type(p) and type(s), respectively. For instance, in Fig. 1 we have type(p) = type(g) = type(w) = type(e) = Philosopher and type(t) = type( ) = type( f ) = type(b) = Fork.

The interaction formula Γ determines the family of systems we can construct out of these components. It does so by specifying, for each possible number of replicated instances (for example, 3 philosophers and 3 forks), which are the possible interactions between them. An interaction consists of a set of transitions that are executed simultaneously. For example, in an interaction philosopher 3 executes a g(et) transition simultaneously with t(ake) transitions of the forks 2 and 3. Before formalizing this, we introduce the syntax and semantics of Interaction Logic.

Interaction Logic. For a constant κ ≥ 1, fixed throughout the paper, the Interaction Logic ILκ is built on top of a countably infinite set Var of variables, the set Pred = N k=1 P k of monadic predicate symbols ranged over by pr (i.e. the logic has a predicate symbol for each port), the binary predicate ≤, and the successor functions succ 0 , . . ., succ κ−1 , of arity one. The formulae of ILκ are generated by the syntax

ILκ is interpreted over finite ranked trees of arity κ, which we identify with a prefixclosed language of words, also called nodes, over the alphabet {0, . . . , κ − 1}. The root of the tree is the empty word , and the children of w are w0, w1, . . . , w(κ − 1). Formally, an interpretation or structure is a pair I = (U, ι), where the universe U is a tree and ι assigns a node to each variable and a set of nodes to each predicate in Pred. The predicate ≤ and the functions succ 0 , . . . , succ k−1 have the usual fixed interpretations: If t and t are interpreted as w and w , then t 1 ≤ t 2 holds iff w is a prefix of w , and succ i (t) is interpreted as the node wi, if wi ∈ U, and as the root otherwise. So, loosely speaking, successor functions wrap around to the root.

When κ = 1, formulae are interpreted on languages { , 0, 00, . . . , 0 n−1 } for some number n. To simplify notation, in this case we assume that they are interpreted over the set {0, 1, . . . , n − 1}, and succ 0 is the usual successor function on numbers, modulo n.

Intuitively, a universe U determines an instance of the component-based system, with one instance of each component for each w ∈ U. So, for example, for κ = 1 and U = {0, 1, 2, . . . , n − 1} in our running example we have philosophers 0, 1, . . . , n − 1 and forks 0, 1, . . . , n − 1. Generally, with κ = 1 we can describe pipeline and token-ring architectures, whereas higher values describe tree-shaped architectures.

Interaction formulae. A formula of ILκ is an interaction formula if it is the conjunction of the following formula:

with a finite disjunction of formulae of the form:

where ϕ, ψ 1 , . . . , ψ m are conjunctions of atomic formulae of the form t 1 ≤ t 2 and their negations. Intuitively, formula (3) is a generic axiom that prevents two ports of the same instance of a component type from interacting. The formulae of form (4) are called the clauses of the interaction formula.

Example 1. Consider a component-based system S = C 1 , C 2 , Γ , where C 1 and C 2 have ports p 1 and p 2 , respectively, and Γ has one single clause

states that an interaction consists of: the i-th process of type C 1 executes transition p 1 ; the j-th process of type C 2 executes p 2 ; and, for every i > ( j + 1) mod n, the i-th process of type C 1 executes transition p 1 as well; all this happens simultaneously in one atomic step.

Loosely speaking, (4) states that in an interaction components can simultaneously engage in a multiparty rendez-vous, together with a broadcast to the ports q 1 , . . . , q m of the components whose indices satisfy the constraints ψ 1 , . . . , ψ m , respectively. An example of peer-to-peer rendez-vous with no broadcast is the dining philosophers system in Fig. 1 , whereas examples of broadcast are found among the benchmarks in §5. In the next section we show that, despite this generality, it is possible to construct a trap invariant for any interaction formula in a purely syntactic way.

Observe that the interaction formula does not explicitly specify that every other process remains idle. Formally, as we will see in the next section, the system has an interaction for each minimal model of (4), which allows us not to have to specify idleness. Given structures I 1 = (U, ι 1 ) and I 2 = (U, ι 2 ) sharing the same universe U, we say I 1 I 2 if and only if ι 1 (pr) ⊆ ι 2 (pr) for every pr ∈ Pred. Given a formula φ, a structure I is a minimal model of φ if I | = φ and, for all structures I such that I I and I I, we have I | = φ.

The semantics of a component-based system S = C 1 , . . . , C N , Γ is an infinite family of Petri Nets, one for each universe of Γ. The reachable markings and actions of the Petri Net characterize the reachable global states and transitions of the system, respectively. To fix notations, we recall several basic definitions. Petri Net Semantics of Component-Based Systems. We define the semantics of a component-based system as an infinite family of 1-safe Petri Nets. For k = 1, . . . , N let C k = P k , S k , s 0 k , ∆ k be a component type and, then, let S = C 1 , . . . , C N , Γ be a system.

Fix a universe U of Γ. We define a marked Petri Net N U S def = ( S , T, E , m 0 ) as follows:

That is, the net has a place (s, u) for each state s of each component type, and for each node u.

-For each minimal model I = (U, ι) of a clause C of Γ, the set T contains a transition t ι ∈ T , and the set E contains edges ((s, u), t ι ) and (t ι , (s , u)) for every s

. Nothing else is in T or E. Intuitively, t ι "synchronizes" all the transitions s p − → s of the different components occurring in the interaction.

-For each 1 ≤ k ≤ N, each s ∈ S k and each u ∈ U, m 0 ((s, u)) = 1 if s = s 0 k and m 0 ((s, u)) = 0, otherwise. That is, m 0 contains the places (s, u) such that s is an initial state. It follows immediately from this definition that N U S is a 1-safe Petri Net. Indeed, for every u ∈ U, for every component-type C k , and for every reachable marking m, we have s∈S k m((s, u)) = 1. This reflects that the instance of C k at u is always in exactly one of the states of S k ; if s is that state, then (s, u) is the place carrying the token.

Example 2. Consider our running example, with U = {0, 1, . . . , n−1}, i.e., n philosophers and n forks. Since the interaction formula (1) has no constants, its models are pairs (U, ι), where ι gives the interpretation of the free variable i and the predicates g, t, etc. The first disjunct of (1) is [g(i) ∧ t(i) ∧ t(succ(i))]. It has a minimal model for each k ∈ U, namely the model with ι(i) = k, ι(g) = {k} and ι(t) = {k, (k + 1) mod n}. In the interaction produced by this model, the k-th philosopher executes transition g(et), the forks with numbers k and (k + 1) mod n execute transition t(ake), and all other philosophers and forks remain idle. The second disjunct yields the interactions in which a philosopher puts down its forks. Fig. 2 An IMT defines an invariant of the Petri Net, because some place in the trap will always be marked, no matter which sequence of transitions is fired. The trap invariant of N is the set of markings that mark each IMT of N. Clearly, since marked traps remain marked, the set of reachable markings is contained in the trap invariant. Hence, to prove that a certain set of markings is unreachable, it is sufficient to prove that the set has empty intersection with the trap invariant. For self-completeness, we briefly discuss the computation of the trap invariant for a given marked Petri Net of fixed size, before explaining how this can be done for the infinite family of marked Petri Nets defining the executions of parameterized systems.

The trap constraint of a Petri Net N = (S , T, E) is the formula: is the initial marking of a 1-safe Petri Net N and µ 0 def = m 0 (s)=1 s is a propositional formula, then every valuation of µ 0 ∧ Θ(N) defines an IMT of (N, m 0 ). Usually, computing invariants requires building a sequence of underapproximants whose limit is the least fixed point of an abstraction of the transition relation of the system [22] . This is not the case of the trap invariant, that can be directly computed from the trap constraint and the initial marking [11, 17] .

In the rest of the section we construct a parameterized trap constraint that characterizes the traps, not of one single net, as Θ(N), but of the infinite family of Petri Nets obtained from a component-based system. The parameterized trap constraint is a formula of WSκS. In Section 3.1 we first explain how to embed our interaction logic into WSκS, and in Section 3.2 we construct the parameterized trap constraint.

We briefly recall the syntax and semantics of WSκS, the monadic second order logic WSκS of κ successors (see e.g. [37] ). Let SVar be a countably infinite set of second-order variables (also called set variables), denoted as X, Y, . . . in the following. The syntax of WSκS is:

So WSκS extends ILκ with the constant symbol , atoms X(t) and monadic second order quantifiers ∃X . φ. We can consider w.l.o.g. equality atoms t 1 = t 2 instead of the inequalities t 1 ≤ t 2 in ILκ, because the latter can be defined in WSκS as usual:

i=0 X(succ i (x)) Like ILκ, the formulae of WSκS are interpreted on ordered trees of arity κ. The models of WSκS are structures (U, ι), where ι assigns the root of the tree to , a node ι(x) to each variable x ∈ Var and a set ι(X) ⊆ U to each set variable X ∈ SVar. The satisfaction relation (U, ι) | = WSκS φ is defined as for ILκ, with one difference: in ILκ, the successor of a leaf of a tree is the root of the tree, while in WSκS the successor of leaf is, by convention, the leaf itself [37, Example 2. 10.3] . This is the only reason why ILκ is not just a fragment of WSκS.

We define an embedding of ILκ formulae, without occurrences of predicates and set variables, into WSκS. W.l.o.g. we consider ILκ formulae that have been previously flattened, i.e the successor function occurs only within atomic propositions of the form succ i (x) = y. This is done by replacing each atomic proposition of the form succ i 1 (. . . succ i n (x) . . .) = y by the formula ∃x 1 . . . ∃x n . x n = succ i n (x) ∧ y = succ i 1 (x 1 ) ∧ n−1 j=1 x j = succ i j (x j+1 ). The translation of an ILκ formula φ into WSκS is the formula Tr(φ), defined recursively on the structure of φ such that Tr simply preserves first-order connectives and, secondly, yields:

We show that a formula φ of ILκ and its WSκS counterpart Tr(φ) are equivalent: Lemma 1. Given an ILκ formula φ, for any structure I = (U, ι), we have I | = IL φ ⇐⇒ I | = WSκS Tr(φ).

Fix a component-based system S = C 1 , . . . , C N , Γ and recall that every universe U induces a Petri Net N U S whose set of places is N k=1 S k × U. For every state s ∈ N i=1 S i , let X s be a monadic second-order variable, and let X be the tuple of these variables in an arbitrary but fixed order. We define a formula trap-pred S (X), with X as set of free variables, that characterizes the traps of the infinitely many Petri Nets N U S corresponding to S. Formally, trap-pred S (X) has the following property:

For every universe U and for every set P ⊆ N k=1 S k × U of places of N U S : P is a trap of N U S iff the assignment X q → {u ∈ U | (q, u) ∈ P} satisfies trap-pred S (X).

Observe that every assignment to X encodes a set of places, and vice versa. So, abusing language, we can speak of the set of places X.

We define auxiliary predicates that capture the intersection of the set of places X with the pre ( • t) and postset (t • ) of a transition t in N U S . For every clause C of Γ, of the form (4), we define the WSκS formulae:

intersects-pre C S (X, x 1 , . . . , x ) = j=1 X• p j (x j ) ∨ +m j= +1 ∃x j . Tr(ψ j ) ∧ X• p j (x j ) and

intersects-post C S (X,

Now we can define trap-pred S (X) as the conjunction of the following formulae, one for each clause C (in the form described in (4)

So, intuitively, trap-pred S (X) states that for every transition of the Petri Net, if the set X of places intersects the preset of the transition, then it also intersects its postset. This is the condition for the set of places to be a trap. Formally, we obtain:

Given a component-based system S = C 1 , . . . , C N , Γ and a structure I = (U, ι), where ι is an interpretation of the set variables X, the set P = { s, u ∈ N k=1 S k ×U | u ∈ ι(X s )} is a trap of N U S if and only if (U, ι) | = WSκS trap-pred S (X). Parameterized Trap Invariants in WSκS. Loosely speaking, the intended meaning of trap-pred S (X) is "the set of places X is a trap". Our goal is to construct a formula stating: "the marking m marks all initially marked traps".

Recall that the Petri Nets obtained from component-based systems are always 1safe, and so a marking is also a set of places. Recall, however, that all reachable markings have the property that they place exactly one token in the set of places modeling the set of states of a component (loosely speaking, the set of places of the k-th philosopher is (w, k) and (e, k), and there is always one token in the one or the other). So we define a formula marking S (X) with intended meaning "the set of places X is a legal marking", and another one, trap-invariant S (X) with intended meaning "the set of places X marks every initially marked trap".

In addition to the tuple of set variables X defined above, we consider now the "copy" tuple X def = X s s∈S i ,1≤i≤N . Intuitively, X and X represent one set of places each. First, we define a (1-safe) marking as a set of places that marks exactly one state of each copy of each component:

Second, we give a formula describing the intersection of two sets of places:

Finally, to actually capture IMTs we need to determine if a trap is initially marked. However, this can be easily described by the formula:

So we can define the trap-invariant by the WSκS formula:

Relying on Lemma 2 we are assured that the set represented by X intersects all IMTs. Now, let ϕ(X) be any formula that defines a set of good global states of the componentbased systems (or, equivalently, a good set of markings of their corresponding Petri nets), with the intuition that, at any moment during execution, the current global state of the component-based system should be good. We can now state the following theorem, that captures the soundness of the verification method based on trap invariants: Theorem 1. Given a component-based system S and a WSκS formula ϕ(X), if the formula ∃X . marking S (X) ∧ trap-invariant S (X) ∧ ¬ϕ(X) (7) is unsatisfiable, then for every universe U, the property defined by the formula ϕ(X) holds in every reachable marking of N U S . In the light of the above theorem, verifying the correctness of a component-based system with any number of active components boils down to deciding the satisfiability of a WSκS formula. The latter problem is known to be decidable, albeit with nonelementary worst-case complexity. A closer look at the verification conditions of the form (7) generated by our method suffices to see that the quantifier alternation is finite, which implies that the time needed to decide the (un)satisfiability of (7) is elementary. Moreover, our experiments show that these checks are very fast (less than 1 second on an average machine) for a non-trivial set of examples.

Since the safety verification problem is undecidable for parameterized systems [6] , the verification method based on trap invariants cannot be complete. As an example, consider the alternating dining philosophers system, of which an instance (for n = 3) is shown in Fig. 3 . The system consists of two philosopher component types, namely Philosopher rl , which takes its right fork before its left fork, and Philosopher lr , taking the left fork before the right one. Each philosopher has two interaction ports for taking the forks, namely g (get left) and gr (get right) and one port for releasing the forks p (put). The ports of the Philosopher rl component type are overlined, in order to be distinguished. The Fork component type is the same as in Fig. 1 . The interaction formula for this system Γ alt philo , shown in Fig. 3 , implicitly states that only the 0-index philosopher component is of type Philosopher rl , whereas all other philosophers are of type Philosopher lr . Note that the interactions on ports g , gr and p are only allowed if zero(x) def = ∀y . x ≤ y holds, in other words if x is interpreted as the root of the universe (in our case, 0 since U = {0, . . . , n − 1}).

It is well-known that any instance of the parameterized alternating dining philosophers system consisting of at least one Philosopher rl and one Philosopher lr is deadlockfree. However, trap invariants are not enough to prove deadlock freedom, as shown by the global state { b, 0 , h, 0 , b, 1 , w, 1 , f, 2 , e, 2 }, marked with thick red lines in Fig. 3 . Note that no interaction is enabled in this state. Moreover, this state intersects with any trap of the marked PN that defines the executions of this particular instance, as proved below. Consequently, the trap invariant contains a deadlock configuration, and the system cannot be proved deadlock-free by this method. (s(x) ))] Philosopher lr (2) Fork (0) Fork (1) Philosopher lr (1) Philosopher rl (0)

Proposition 1. Consider an instance of the alternating dining philosophers system in Fig. 3 , consisting of components Fork(0), Philosopher rl (0), Fork(1), Philosopher lr (1), Fork(2) and Philosopher lr (2) placed in a ring, in this order. Then each nonempty trap of this system contains one of the places b, 0 , h, 0 , b, 1 , w, 1 , f, 2 or e, 2 .

However, the configuration is unreachable by a real execution of the PN, started in the initial configuration that marks f, i and w, i , for all i = 0, 1, 2. An intuitive reason is that, in any reachable configuration, each fork is in state f (ree) only if none of its neighboring philosophers is in state e(ating). In order to prove deadlock freedom, one must learn this and other similar constraints. Next, we present a heuristic method for strengthening the trap invariant that infers such universal constraints.

As shown by the example above, trap constraints do sometimes fail to prove interesting properties. Hence, it is desirable to refine the overapproximation of viable markings to exclude more spurious counterexamples. In order to do so, we consider a special class of linear invariants, called 1-invariants in the following. Although linear invariants are not structural and rely on the set of reachable markings of a marked Petri Net, the set of 1-invariants can be sufficiently under-approximated by structural conditions. The following lemma relates 1-invariants to some structural properties. However, there are 1-invariants not captured by these conditions. Taking the intersection of this set of 1-invariants defines a weaker invariant, which is sound for our verification purposes. We devote the rest of this section to describe WSκS formulae which capture the structural properties necessary to define 1-invariants as laid down by Lemma 3 (2) . As demonstrated in Section 3 the pre-and postset of transitions, as well as general sets of places in a PN describing the execution semantics can be defined in WSκS. Hence, we present the definitions of the following formulae only in the full version of this article [16] and just give the intuitions here.

As before, we fix two tuples of set variables X and X , with one variable X s for each state s ∈ N i=1 S i and define the following formulae: unique-init S (X), which captures that the set of places induced by an interpretation of X uniquely intersects the set of all initial states, and unique-intersection S (X, X ), which states that the set of places induced by an interpretation of X and X share precisely one place. Given a transition t of the marked Petri Net N U S defining the execution semantics of a component-based system S, for a universe U, we consider the following formulae:

uniquepre C S (X, x 1 , . . . , x ), which describes that the set of places encoded by the interpretation of X uniquely intersects • t, and uniquepost C S (X, x 1 , . . . , x ), which in the same sense captures the unique intersection with t • . Now we define a predicate 1-pred S which consists of a conjunction of unique-init S and the formulae:

one for each clause C in Γ. We show the soundness of this definition, by the following: 

. We may now define the 1-invariant analogously to the trap-invariant before:

1-invariant S (X) = ∀X . 1-pred S (X ) → unique-intersection S (X, X ).

(9) Reasoning as before we obtain a refinement of Theorem 1 since every reachable marking has to satisfy both invariants.

Theorem 2. Given a component-based system S and a WSκS formula ϕ(X), if the formula:

∃X . marking S (X) ∧ 1-invariant S (X) ∧ trap-invariant S (X) ∧ ¬ϕ(X) (10) is unsatisfiable, then for every universe U, the property defined by the formula ϕ(X) holds in every reachable marking of N U S .

We have implemented a prototype (called ostrich [15] ) of this verification procedure to evaluate the viability of our approach. The current version of the prototype can only handle token-ring and pipeline topologies, but not trees; for these topologies the verification reduces to checking satisfiability of a formula of WS1S. We have also considered one example with tree-topology (see below), for which the formula was constructed manually. Satisfiability of WS1S and WSκS formulae was checked using version 1.4/17 of Mona [33] . We consider various examples separated in categories:

Cache Coherence. Following [24] we formalized and checked the described safety properties and deadlock-freedom of the following cache coherence protocols: Illinois, Berkeley, Synapse, Firefly, MESI, MOESI, and Dragon. Mutual Exclusion. We modelled and checked for deadlock-freedom and mutual exclusion Burns' [35] , Dijkstra's and Szymanski's [3] algorithms as well as a formulation of Dijkstra's algorithm on a ring structure with token passing [30] . Furthermore, we check synchronization via a semaphore which is atomically aquired and by broadcasting to ensure everyone else is not in the critical section. Dining Philosophers. This is the classical problem of dining philosophers which all take first the right fork and then the left fork. We consider the following "flavors" of this problem: there is one philosopher who takes first her left and then her right fork, as above but the forks remember whom took them, and there are two global forks everyone grabs in the same order. Preemptive Tasks. There are tasks which can be either waiting, ready, executing or preempted. Initially one task is executing while all others are waiting. At any point a task may become ready and any ready task may preempt the currently executing task. Upon finishing the executing task re-enables one preempted task. Here, we have additionally two alternatives: Firstly, we consider the case where always the agent with highest index resumes execution. Secondly, we let the processes establish the initial condition from a position where everyone is waiting (referenced later as uninitialized). Dijkstra-Scholten. This is an algorithm that is used to detect termination of distributed systems by message passing along a tree [25] . Since the prototype only supports linear topologies we can generate the necessary formula automatically only for this case. Herman. This algorithm implements self-stabilizing token passing in rings. The formulation is modelled after [19] . This applies for all following examples. Hence, we describe the examples only in little detail. Israeli-Jalfon. This is another self-stabilizing token passing algorithm in rings. Lehmann-Rabin. This is a randomized solution to the dining philosophers problem. Dining Cryptographers. A group of cryptographers want to determine if one of them paid for a meal or a stranger but do not reveal how they acted individually.

The results are shown in Table 1 . The first column reports the size of the example in terms of the amount of states (#st.) and clauses (#cls.). The second column indicates which properties could ( ) and could not be verified (×) because the conjunction of trap and one-invariant was not strong enough to prove the given property. The third column reports the time (in second) it takes to prove all considered properties. These results are measured on the provided virtual machine for artifacts [32] where the host system is an average laptop. To understand the next four columns, recall that Mona constructs for a given formula φ(X) a finite automaton recognizing all the sets X for which ϕ holds. Since the automaton can have very large alphabets, its transition relation is encoded as a binary decision diagram (BDD). The columns report the number of states and the number of nodes of the BDD for different formulas. More precisely, the columns trap, trap-inv, flow, and flow-inv give the sizes of the automata for the formula trap-pred S ∧ initially-marked S , trap-invariant S , 1-pred S and 1-invariant S respectively. We write "n.a." (for "not available") to indicate that Mona timed out before the automaton was computed.

The first observation is that the satisfiability checks often can be done in very short time. This is surprising, because the formulas to be checked, namely (7) and (10), exhibit one quantifier alternation (recall that trap-invariant S and 1-invariant S contain universal quantifiers). More specifically, since trap-invariant S is obtained by universally quantifying over trap-pred S ∧ initially-marked S , one would expect the automaton for the former to be much larger than the one for the latter, at least in some cases. But this does not happen: In fact, the automaton for trap-invariant S is almost always smaller. Similarly, there is no blowup from 1-pred S to 1-invariant S . A possible explanation could be that the exponential blowup caused by universal quantification in WSκS manifests only on theoretical corner cases, which do not occur in our examples.

We have shown that the trap technique used in [11, 28, 13] for the verification of single systems can be extended to parameterized systems with sophisticated communication structures, like pipelines, token rings and trees. Our extension constructs a parameterized trap invariant, a formula of WSκS satisfied by the reachable global states of all instances of the system. The core of the approach is a purely syntactic, automatic derivation of the trap invariant from the interaction formula describing the possible transitions of the system. When the set of safe global states can also be expressed in WSκS, which is usually the case, we check using the Mona tool whether the trap invariant implies the safety formula. The technique proves correctness of systems that do not produce well-structured transition systems in the sense of [1, 29] , and of systems with broadcast communication, for which, to the best of our knowledge, cut-off results have not been obtained yet.

Our experiments demonstrate that trap invariants can be very effective in finding proofs of correctness (inductive invariants) of common benchmark examples. In practice, the technique is very cheap, since it avoids costly fixpoint computations. This suggests incorporating it into other verifiers as a preprocessing step.

Data Availability Statement and Acknowledgements. The work of the second and fifth author has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme under grant agreement No 787367 (PaVeS). The tool ostrich and associated files are available in the Zenodo repository: https://zenodo.org/ record/3676940

General decidability theorems for infinitestate systems

Regular model checking without transducers (on efficient verification of parameterized systems)

Parameterized verification through view abstraction

A framework for the verification of parameterized infinite-state systems

Parameterized model checking of rendezvous systems

Limits for automatic verification of finite-state concurrent systems

Tight cutoffs for guarded protocols with fairness

An effective characterization of minimal deadlocks and traps in Petri nets based on graph theory

Rigorous component-based system design using the BIP framework

Tools and Algorithms for the Construction and Analysis of Systems

D-Finder: A tool for compositional deadlock detection and verification

Decidability of Parameterized Verification

Approaching the coverability problem continuously

Abstract regular model checking

Structural invariants for the verification of systems with parameterized architectures

Checking deadlock-freedom of parametric component-based systems

Reasoning about networks with many identical finite state processes

Learning to prove safety over parameterised concurrent systems

Environment abstraction for parameterized verification

Cubicle: A parallel SMT-based model checker for parameterized systems

Systematic design of program analysis frameworks

Iterating transducers. The Journal of Logic and Algebraic Programming 52-53

Automatic verification of parameterized cache coherence protocols

Termination detection for diffusing computations

Reducing model checking of the many to the few

Reasoning about rings

An smt-based approach to coverability analysis

Well-structured transition systems everywhere! Theor

Reachability sets of parameterized rings as regular languages

Reasoning about systems with many processes

Mona: Monadic second-order logic in practice

Analyzing guarded protocols: Better cutoffs, more systems, more expressivity

A proof of Burns n-process mutual exclusion algorithm using abstraction

Symbolic model checking with rich assertional languages

Automata Theory and Its Applications

Tools and Algorithms for the Construction and Analysis of Systems

Mathematical Foundations of Computer Science

), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use