where f(t) is a term with a fresh variable t such that - f is a solution of **x**˙ = **e** and - f(0) = id.

Some other rules of dL, such as the differential invariant rule (DI) that is central in many proofs, are introduced later in Definition 13.

## **3 Relational Differential Dynamic Logic**

Intuitively, we want a way to describe two dynamics that are executed in parallel, and compare their outputs. In terms of (nondeterministic) transition systems, parallel composition is available via tensor products.

**Definition 7 (tensor product).** Given two transition systems (S, R) and (S , R ), their *tensor product* (S × S , R ⊗ R ) is defined to be the transition system whose transition relation is given by

$$R \otimes R' := \{ (s, s'), (t, t') \mid (s, t) \in R, (s', t') \in R' \}.$$

No extension of the dL syntax is needed to model tensor products: disjointness of the variables of the two systems suffices. From now on we split variables into two disjoint sets: V = VV. We denote variables in V by x, y,... and those in V by x, y,... . Terms in T ( V ), first-order formulas in F*ml*( V ), and programs in HP( V ) are denoted by e, f,... , P , Q, . . . , and α, β,... , and similarly for the corresponding constructs with V.

An easy proof of the following fact can be found in the appendix.

**Proposition 8.** − - α →⊗−- α → = − - α; α →

Scenarios with two parallel differential dynamics are the main focus of this work. We formalize an assertion relating two dynamics using the following format. It is a syntactic counterpart of Proposition 8.

**Definition 9 (relational differential dynamics).** We call hybrid programs of the following form *relational differential dynamics (RDD)*

$$
\dot{\overline{\mathbf{x}}} = \overline{\mathbf{e}} \& \,\, \overline{Q} \; ; \quad \dot{\underline{\mathbf{x}}} = \underline{\mathbf{e}} \& \,\, \underline{Q} \tag{3}
$$

Now that we have ways to express separate systems evolving in parallel, we turn to the construction of proofs which reason about their relationships.

**Example 10.** Using RDD, the problem in Example 1 is expressed as ΓC δC ; δC φC where δC := x˙ = v, v˙ = 1 , δC := ( ˙x = v, v˙ = 2), ΓC := {x = x = 0, v = v = 0} is the precondition, and φC := (x = x = 1 ⇒ v ≤ v) is the postcondition.

Let us prove, in KeYmaera X, the RDD sequent ΓC δC ; δC φC . In KeYmaera X, the only applicable rule to this sequent turns it into ΓC δC δC φC . We then explicitly "solve" the second dynamics, yielding the following goal:

$$\{F\_C \vdash \left[\overline{\delta\_C}\right] \forall \underline{t} \ge 0. \left(\overline{x} = \underline{x} + \underline{v} \cdot \underline{t} + \underline{t}^2 = 1 \Rightarrow \overline{v} \le \underline{v} + \underline{t}\right) \tag{4}$$

where x and v in φC are replaced by their explicit solutions with respect to the freshly introduced time variable t. Again differential invariant rules do not apply to (4), so one must solve the first dynamics, too, yielding

$$\exists \, I\_C \vdash \forall \overline{t} \ge 0. \,\forall \underline{t} \ge 0. \left(\overline{x} + \overline{v} \cdot \overline{t} + \overline{t}^2 / 2 = \underline{x} + \underline{v} \cdot \underline{t} + \underline{t}^2 = 1 \Rightarrow \overline{v} + \overline{t} \le \underline{v} + \underline{t}\right)$$

Since this goal is first order, the quantifier elimination, a central proof technique in KeYmaera X [18], proves the goal.

The above example worked out since it admits explicit solutions expressible in dL. This is not always the case as the following example demonstrates.

**Example 11.** We consider two objects moving through fluids subjected to different kinds of drag. One object moves through a viscous fluid and is therefore subject to linear drag; its dynamics are δF := ( ˙x = v, v˙ = −v).

The other object moves through a less viscous fluid and is subject to turbulent drag; its dynamics are δF := (x˙ = v, v˙ = −v2). Our goal is to show that the latter has higher speed when both objects reach a certain point in space (x = x = l).

The following functions v∗, x∗, v∗ and x∗ are solutions of the dynamics.

$$\begin{aligned} \underline{v}^\*(\underline{t}) &= \underline{v}\_0 \cdot e^{-\underline{t}} & \underline{x}^\*(\underline{t}) &= \underline{x}\_0 + \underline{v}\_0 \cdot (1 - e^{-\underline{t}}) \\ \overline{v}^\*(\overline{t}) &= \frac{\overline{v}\_0}{1 + \overline{v}\_0 \cdot \overline{t}} & \overline{x}^\*(\overline{t}) &= \overline{x}\_0 + \log(1 + \overline{v}\_0 \cdot \overline{t}) \end{aligned}$$

where v0 etc. denote the initial values. Unfortunately, we cannot express exponentiations and logarithms in KeYmaera X, and thus the "solve" rule that we used in Example 10 cannot be applied here.

One obvious solution to this would be to add support for exponentiations and logarithms in KeYmaera X, but this would break the decidability of the underlying first order logic, which is a major feature of dL [18]. In fact, the same issue occurs even in standard use cases of KeYmaera X, and motivated the introduction of proof rules which do not demand explicit solutions to differential dynamics [20,22] using the *Lie derivative*.

**Definition 12 (formal Lie derivative in** dL **from [20,22]).** The formal Lie derivative of a term f along dynamics δ ≡ (**x**˙ = **e** & Q) of dimension n is a dL term Lδ f ∈ T (V) given by6

$$\mathcal{L}\_{\delta}f := \frac{\partial}{\partial x\_1} f \cdot e\_1 + \dots + \frac{\partial}{\partial x\_n} f \cdot e\_n$$

**Definition 13 (proof rules from [20,22]).**

The differential invariant rule (DI) is the central rule for proving safety properties [20,22]: it reduces a global property of the dynamics to local reasoning by means of Lie derivatives. The Darboux inequality rule (Dbx) is derived from real algebraic geometry; see e.g. [22].

**Example 14.** Consider an example differential dynamics in one variable, ˙x = 2. Suppose we want to show that x ≥ 0 holds after following these dynamics for any amount of time, starting from x = 1. One way to do this is to show that (1) this predicate holds initially and (2) the time derivative of x is always nonnegative. These are precisely the two premises of the (DI) rule: to show the sequent x = 1 [ ˙x = 2]x ≥ 0 (DI) requires us to prove (1) x = 1 x ≥ 0 and (2) x = 1 [ ˙x = 2]Lx˙=2 x ≥ 0, where Lx˙=2 x = 2. Note that we give an initial condition x = 1 in the precedent of this sequent.

## **4 Synchronizing Dynamics**

The intuitive explanation of the RDD construction of Definition 9 is a "serialization" of two dynamics. This construction however does not match the (DI)

6 It is easy to see that the *derivative* of a term t ∈ T (V) with respect to x ∈ V can be given as a dL term ∂ ∂x e ∈ T (V) such that - ∂ ∂x e = ∂ ∂x - e . The definition of ∂ ∂x e is inductive with respect to the term e.

and (Dbx) rules, as they accept only one dynamics followed by a comparison. In order to make use of these rules in our relational reasoning, we introduce another proof method. It "synchronizes" two dynamics.

After some theoretical preparations we define the new rule and prove its soundness. We will illustrate the usefulness of this rule in Section 6, through some case studies that are inspired by our collaboration with the industry.

## **4.1 Time Stretching**

A key theoretical tool towards the soundness of our synchronization rule is called *time stretching*. Its idea is very similar to the technique of *time-reparametrization* for ODEs [7].

**Definition 15 (time stretch function).** Let T ∈ R≥0. A function K : [0, T] → R≥0 is a *time stretch function* if K(0) = 0, K is continuously differentiable and K˙ (t) > 0 for each t ∈ [0, T].

**Remark 16.** The condition K˙ (t) > 0 ensures that K is strictly increasing and is a bijection from [0, T] to [0, K(T)]. The inverse of K is K−1 : [0, K(T)] → [0, T], and it is straightforward to check K−1 is another time stretch function.

The next results tell us how to turn an ODE into another, given a time stretching function K, so that a time-stretch ψ◦K of a solution ψ of one becomes a solution of the other.

**Lemma 17.** *Suppose* f : RV → RV *is a vector field and* K : [0, T] → [0, K(T)] *is a time stretch function. If* ψ : [0, K(T)) → RV *satisfies* ψ˙(s) = f(ψ(s)) *for all* s ∈ [0, K(T))*, then the function* ρ = ψ ◦ K : [0, T) → RV *satisfies* ρ˙(t) = K˙ (t) · f(ρ(t)) *for all* t ∈ [0, T)*.*

*Proof.* We have ˙ρ(t) = K˙ (t)·ψ˙(K(t)) = K˙ (t)·f(ψ(K(t))) = K˙ (t)·f(ρ(t)), where the first equality is by the definitions and the chain rule, the second equality is by the assumption on ψ˙, and the last equality is by the definition of ρ.

Since the inverse of a time stretch function is another time stretch function, we obtain the following corollary of Lemma 17.

**Corollary 18.** *Let* K : [0, T] → [0, K(T)] *be a time stretch function. Let* ρ : [0, T) → RV *satisfy* ρ˙(t) = K˙ (t)· f(ρ(t)) *whenever* 0 ≤ t<T*. Then the function* ψ : [0, K(T)) → RV *, defined by* ψ(s) := ρ(K−1(s))*, satisfies* ψ˙(s) = f(ψ(s)) *whenever* 0 ≤ s<K(T)*.*

### **4.2 Towards a Syntactic Representation**

So far our time-stretch function K has been a semantical object. Here we introduce a syntactic way of reasoning via time-stretch functions. Since a desired time-stretch function is not necessarily expressible in dL, our syntactic reasoning uses an indirect method that exploits a pair of functions called a synchronizer. We will be eventually led to a syntactic reasoning rule (Sync) (Thm. 24).

Given a term g ∈ T (X) and a mapping ψ : [0, T) → RX, we define gψ : [0, T) → R by

$$g\_{\psi}(t) := \|g\|\_{\psi(t)}.\tag{5}$$

Intuitively, gψ(t) is the value of g at time t when we follow the dynamics whose solution is ψ.

**Definition 19 (synchronizers).** Let (δ, δ) be a pair of dynamics, (ω, ω) ∈ RV × RV be a pair of states, and ψ : [0, T) → RV and ψ : [0, T) → RV be the unique solutions of δ and δ from ω and ω, respectively. We say a pair of dL terms (g, g) ∈ T ( V ) × T ( V ) *synchronizes* (δ, δ) from (ω, ω) if the following hold.

**–** gψ(0) = gψ(0)

**–** The derivatives of gψ and gψ are both strictly positive.

The following lemma ensures that, for any synchronizer, a corresponding time stretch function exists.

**Lemma 20.** *In the setting of Definition 19, let* t ∈ [0, T) *and* t ∈ [0, T) *be such that* gψ(t) = gψ(t)*. Then the function* K*, defined by* K(s) := gψ−1(gψ(s))*, is a time stretch function from* [0,t] *to* [0, t]*. Moreover we have* K˙ (s) = g˙ ψ(s) g˙ ψ(K(s)) *.*

*Proof.* Since gψ is strictly monotonic on [0, t], it has an inverse gψ−1 defined from gψ([0, t]) to [0, t]. By assumption we have gψ(0) = gψ(0), and thus K(0) = gψ−1(gψ(0)) = gψ−1(gψ(0)) = 0. Also since gψ(t) = gψ(t), we see that gψ−1 is defined from gψ([0,t]) to [0, t]. Thus K = gψ−1 ◦ gψ is defined from [0,t] to [0, t].

$$\begin{aligned} \dot{K}(s) &= \dot{\overline{g}}\_{\overline{\psi}}(s) \cdot \left( \underline{g\_{\psi}}^{\cdot -1} \right) (\overline{g\_{\overline{\psi}}}(s)) & \text{derivative of } K = \underline{g\_{\psi}}^{-1} \circ \overline{g\_{\overline{\psi}}} \\ &= \frac{\dot{\overline{g\_{\psi}}}(s)}{\underline{g\_{\psi}}(\underline{g\_{\psi}}^{\cdot -1} \circ \overline{g\_{\overline{\psi}}}(s)))} & \text{derivative of } \underline{g\_{\psi}}^{-1} \\ &= \frac{\dot{\overline{g\_{\psi}}}(s)}{\underline{g\_{\psi}}(K(s))} \end{aligned}$$

whose value is positive by assumptions on the derivatives of gψ and gψ.

We remark that time stretch functions we obtain in Lemma 20 are not necessarily expressible as a dL term, as exemplified by the following example.

**Example 21.** Consider two dynamics δF := (x˙ = v, v˙ = −v2) and δ := (x˙ = 1). Their solutions ψ,ψ : R≥0 → R2 from initial value x = 0, v = 1 are

$$
\overline{\psi}(s) = \left(\log(1+s), (1+s)^{-1}\right) \qquad \qquad \underline{\psi}(s) = (s,0).
$$

Now let g = x and g = x. Then gψ(s) = log(1 + s), gψ = gψ−1 = id and thus K(s) = gψ−1(gψ(s)) = log(1 + s). This is not rational and not expressible in dL.

Using the syntactic Lie derivative (Definition 12), we state a sound inference rule that does not need K to be represented explicitly. We note that there is strong support for Lie derivatives in the tool KeYmaera X, as a key syntactic operation behind the differential invariant (DI) rule (Definition 13).

**Definition 22.** Let δ := **x**˙ = **e** & Q and δ := **x**˙ = **e** & Q be two dynamics and let (g, g) ∈ T ( V ) × T ( V ) (which is supposed to be a synchronizer). We define the *synchronized dynamics* of (δ, δ) with respect to (g, g) as follows:

$$\left(\overline{\boldsymbol{\delta}} \otimes\_{(\overline{\boldsymbol{g}}, \underline{\boldsymbol{g}})} \underline{\boldsymbol{\delta}}\right. := \left(\dot{\overline{\mathbf{x}}} = \overline{\mathbf{e}}, \ \dot{\underline{\mathbf{x}}} = \frac{\mathcal{L}\_{\overline{\boldsymbol{\delta}}} \overline{\boldsymbol{g}}}{\mathcal{L}\_{\underline{\boldsymbol{g}}} \underline{\boldsymbol{g}}} \cdot \underline{\mathbf{e}}\right) \&\left(\overline{\boldsymbol{Q}} \wedge \underline{\boldsymbol{Q}} \wedge \mathcal{L}\_{\overline{\boldsymbol{\delta}}} \overline{\boldsymbol{g}} > 0 \wedge \mathcal{L}\_{\underline{\boldsymbol{\delta}}} \underline{\boldsymbol{g}} > 0\right),$$

**Lemma 23.** *Let* (g, g) *be a synchronizer of* (δ, δ) *from* (ω0, ω0)*. The following are equivalent, where the semantical transition relations are from Definition 5.*

*1.* (ω0, ω0) − - δ; δ → (ω, ω) *and* (ω, ω) ∈ - g = g *2.* (ω0, ω0) − - δ ⊗(g,g) δ → (ω, ω)

*Proof.* We first prove (1 ⇒ 2). In the proof of Lemma 20, we can observe that g˙ ψ(s) = - Lδ g ψ(s), and analogously, ˙gψ(s) = - Lδ g ψ(s). Hence we obtain

$$\dot{K}(s) = \frac{\left[\mathcal{L}\_{\overline{\mathcal{S}}} \overline{g}\right]\_{\overline{\psi}(s)}}{\left[\mathcal{L}\_{\underline{\mathcal{S}}} \underline{g}\right]\_{\overline{\psi}(K(s))}} = \left[\frac{\mathcal{L}\_{\overline{\mathcal{S}}} \overline{g}}{\mathcal{L}\_{\underline{\mathcal{S}}} \underline{g}}\right]\_{\rho(s)}\tag{6}$$

where ρ : [0,t) → RVV is defined by ρ(s) := ψ(s), ψ(K(s)) .

We note that K : [0,t] → [0, K(t)] is a time-stretch function, and that ψ is a solution of **x**˙ = **e**, that is, ψ˙ (u) = - **e** ψ(u) whenever 0 ≤ u<t = K(t). Combined with Lemma 17, we obtain

$$\iota\left(\underline{\psi}\circ\overset{\cdot}{K}\right)(s) = \dot{K}(s)\cdot\left[\underline{\mathbf{e}}\right]\underline{\psi}(K(s)) = \dot{K}(s)\cdot\left[\underline{\mathbf{e}}\right]\_{\rho(s)}\qquad\text{whenever }0 \le s < \overline{t}.$$

Hence, with the fact that ψ is a solution of **x**˙ = **e**, we obtain

$$\dot{\rho}(s) = \left( \dot{\overline{\psi}}(s), \left( \dot{\underline{\psi}} \circ \overset{\cdot}{K} \right)(s) \right) = \left( \left[ \overline{\mathbf{e}} \right]\_{\rho(s)}, \dot{K}(s) \cdot \left[ \underline{\mathbf{e}} \right]\_{\rho(s)} \right) = \left[ \left( \overline{\mathbf{e}}, \frac{\mathcal{L}\_{\overline{\delta}} \overline{\mathcal{g}}}{\mathcal{L}\_{\underline{\delta}} \underline{\mathcal{g}}} \cdot \underline{\mathbf{e}} \right) \right] \rho(s)$$

whenever 0 ≤ s < t. Here the last equality is from (6). This concludes that ρ is a solution of the dynamics δ ⊗(g,g) δ. It remains to prove that for all τ ∈ [0,t], - Q ∧ Q ∧ Lδ g > 0 ∧ Lδ g > 0 ρ(τ) is true. This is an easy consequence of item 1, and the fact that (g, g) is a synchronizer of (δ, δ) from (ω0, ω0).

For the direction (2 ⇒ 1), let (ξ, ξ) : [0, T) → RV ×RV be the unique solution of δ ⊗(g,g) δ from (ω0, ω0). Then there is t ∈ [0, T) such that (ξ(t), ξ(t)) = (ω, ω). Let us prove that (ω, ω) ∈ - g = g . The function h : s ∈ [0, T) → - g ξ(s) − - g ξ(s) is equal to 0 at s = 0 and its derivative is given by:

$$\dot{h}(s) = \left[\mathcal{L}\_{\overline{\delta}} \overline{g}\right]\_{\overline{\xi}(s)} - \left[\mathcal{L}\_{\underline{\delta}} \underline{g}\right]\_{\underline{\xi}(s)} \cdot \frac{\left[\mathcal{L}\_{\overline{\delta}} \overline{g}\right]\_{\overline{\xi}(s)}}{\left[\mathcal{L}\_{\underline{\delta}} \underline{g}\right]\_{\underline{\xi}(s)}} = 0$$

Consequently, h is the constant function equal to 0, which implies that (ω, ω) ∈ - g = g . By definition, ξ is a solution of δ, so ω0 − - δ → ω. Furthermore, by Corollary 18, ξ ◦ K−1 is a solution of δ. Thus ω0 − - δ → ω and

$$\{\left(\overline{\omega}\_{0},\underline{\omega}\_{0}\right)\}\text{ --}\lbrack\overline{\delta};\ \underline{\delta}\rbrack\mapsto(\overline{\omega},\underline{\omega}).\tag{7}$$

The above lemma is a key observation in the current work. It allows us to turn the relational dynamics δ; δ—expressed as a sequential composition in dL into a combined dynamics δ ⊗(g,g) δ. Moreover, we can do so in a way that the two dynamics are synchronized in a reparametrized manner, as specified by (g, g). Such combination of two dynamics is crucial in exploiting the logical infrastructure of dL and KeYmaera X—we emphasize again that the (DI) rule does not support invariant reasoning about the relationship between δ and δ, when the relational dynamics is expressed in the original form δ; δ.

The following is an incarnation of Lemma 23 as a proof rule. We assume that a postcondition is a conditional form E ⇒ ϕ; E is called an *exit condition*. By assuming that E implies g = g, we enforce the second condition (ω, ω) ∈ - g = g in item 1 of Lemma 23. The first three premises are there to ensure that (g, g) is a synchronizer. Under these premises (the first four), the rule allows one to transform its conclusion (about δ; δ) into one about the combined dynamics δ ⊗(g,g) δ, which is amenable to application of the (DI) rule, for example.

**Theorem 24 (synchronization rule).** *The following inference rule is sound:*

$$\frac{\begin{array}{c} I \vdash [\,^{\tilde{\delta}}\rangle \mathcal{L}\_{\overline{\delta}} \overline{g} > 0 \quad \Gamma \vdash \overline{g} = \underline{g} \\\ I \vdash [\underline{\delta}\,] \mathcal{L}\_{\underline{\delta}} \underline{g} > 0 \quad E \vdash \overline{g} = \underline{g} \quad \Gamma \vdash [\,^{\overline{\delta}}\otimes|\_{(\overline{g},\underline{g})} \,\underline{\delta}\,](E \Rightarrow \varphi) \\\ I \vdash [\,^{\overline{\delta}}\overline{\delta};\underline{\delta}\,](E \Rightarrow \varphi) \end{array}}{(Sym)}(Smc))$$

Recall the definition of δ ⊗(g,g) δ (Definition 22), where time stretching for the second dynamics δ is expressed syntactically by Lie derivatives. We call the four premises Γ g = g, E g = g, Γ [ δ ]Lδ g > 0, and Γ [ δ ]Lδ g > 0 the *synchronizability conditions*. These obligations are usually easy to discharge. The last premise, which we call the *synchronized formula*, is typically the core remaining obligation.

**Remark 25 (choice of** (g, g)**).** In applying the (Sync) rule, one still has to find a suitable synchronizer (g, g). This turns out to be straightforward in many examples. In all the case studies in Section 6 and in Example 1, the exit condition E is of the form x = x = C where C is a constant. This suggests the use of g = x, g = x. Indeed, all our proofs use this choice of (g, g).

## **5 Implementation**

KeYmaera X [17] is an interactive theorem prover based on the sequent calculus formulation of dL. It is implemented in Scala, replacing its former system KeYmaera [16]. It has a web-based GUI environment, and a support of automated theorem proving using computer algebra systems such as Mathematica [27].

For the formalization of case studies in Section 6, we extended KeYmaera X version 4.7 (available at [17]) with the (Sync) rule. This extension of KeYmaera X, together with our proofs in case studies, are currently available at http:// group-mmm.org/rddl tacas 2020/.

The KeYmaera X implementation is structured in a flexible manner, from which we benefited. To add a rule to KeYmaera X, one has to implement a Scala program that take the conclusion of the rule and generate the premises of the rule as subgoals. The fact that any Scala program is allowed here enabled us to implement complex algorithms, such as inductive translation of formulas.

In implementing the (Sync) rule, the functions in KeYmaera X called *helpers* helped us, such as in the Lie derivative computation and the functionality to simplify formulas into equivalent ones. The bulk of our effort regarded the ⊗(g,g) operator. There we did a bit more general than we stated in the paper: not only taking dynamics of form **x**˙ = **e** & Q, we also allow sequences of dynamics possibly interleaved by guards and nondeterministic choices. This feature was utilized in the case study that will be described in Section 6.3.

## **6 Case Studies**

We describe three case studies where we proved relational properties of hybrid dynamics. We did so formally in our extension of KeYmaera X described in Section 5. In all the examples, we apply the (Sync) rule as a main proof step, in conjunction with the existing rules in dL. Below, we describe our example systems and outline the important steps in the formal proofs.

#### **6.1 Collision Speed with Constant Acceleration**

In this section we apply the (Sync) rule to the running Example 1. For this example we consider two dynamics δC := x˙ = v, v˙ = a and δC := ( ˙x = v, v˙ = a). Both dynamics represent a car with constant acceleration. Our claim is that if acceleration is larger in the first system, then the first car is necessarily faster than the second car after traveling the same distance l; formally,

$$\left[\varGamma \vdash \left[\overline{\delta\_C}; \underline{\delta\_C}\right]\right] \left(\overline{x} = l \land \underline{x} = l \Rightarrow \underline{v} \le \overline{v}\right) \tag{7}$$

where

$$\Gamma := \{ 0 = \overline{x} = \underline{x}, \ 0 < \overline{v} = \overline{v}\_0, \ \underline{v} = \underline{v}\_0, \ \overline{v}\_0 \ge \underline{v}\_0, \ \ 0 \le \underline{a} \le \overline{a} \}$$

We apply the (Sync) rule, where g := x and g := x. The first two synchronizability conditions are Γ x = x and x = l, x = l x = x, which are trivial. The last two synchronizability conditions are

$$\Gamma \vdash \left[\overline{\delta\_C}\right] \mathcal{L}\_{\overline{\delta\_C}} \overline{g} = \overline{v} > 0 \qquad\qquad \Gamma \vdash \left[\underline{\delta\_C}\right] \mathcal{L}\_{\underline{\delta\_C}} \underline{g} = \underline{v} > 0$$

which are proven using differential invariants (DI). The synchronized formula is

$$T \vdash \left[\overline{\delta\_C}, \underline{\dot{x}} = \underline{v} \cdot (\overline{v}/\underline{v}), \underline{\dot{v}} = \underline{a} \cdot (\overline{v}/\underline{v}) \& \ \overline{v} > 0 \land \underline{v} > 0 \right] (\overline{x} = l \land \underline{x} = l \Rightarrow \underline{v} \le \overline{v})$$

One might try to show the inequality v − v ≥ 0 by the differential invariant (DI) rule, but the Lie derivative of the term v − v is a − a · (v/v), which is not obviously nonnegative. Instead, a trickier expression a·(v2−v2 0)−a·(v2−v2 0)=0 turns out to be an invariant. Its Lie derivative is a · (2v) · a · (v/v) − a · (2v) · a, which is clearly 0, since we also know v > 0.

We do not have an intuitive explanation for this invariant, but it was found by a template-based search, like many other invariants in dL. By positing the existence of a polynomial invariant of a certain degree, we can find conditions on the coefficients by requiring its Lie derivative and initial value are zero. Solving these conditions for a second-degree invariant on the velocities in the system yielded the invariant above.

After finding our invariant, we additionally have to show the invariant entails our desired result, v ≤ v. This can be shown with a standard monotonicity property of modal logics: from φ ψ and Γ [α]φ, we can conclude Γ [α]ψ, where φ states the expression above is an invariant and the velocities are always greater than their initial value, and ψ is our goal: v ≤ v.

#### **6.2 Collision Speed with Different Kinds of Friction**

Here we continue Example 11, where we consider two dynamics δF ≡ (x˙ = v, v˙ = −v2) and δF ≡ ( ˙x = v, v˙ = −v). Our goal is ΓF [ δF ; δF ](x = x = l ⇒ v ≤ v), with ΓF := {x = x = 0, 0 < v ≤ v ≤ 1}.

First, we establish the fact that the objects in this example always have positive velocity. We show this by the (Dbx) rule (Definition 13), where LδF v = −v2 and LδF v = −v. This allows us to infer v > 0 and v > 0 hold at all times.

We apply the (Sync) rule along x = x, yielding the synchronized dynamics

$$\dot{\overline{x}} = \overline{v}, \dot{\overline{v}} = -\overline{v}^2, \dot{\underline{x}} = \underline{v} \cdot (\overline{v}/\underline{v}), \dot{\underline{v}} = -\underline{v} \cdot (\overline{v}/\underline{v}) \text{ & } \overline{v} > 0 \land \underline{v} > 0$$

Note that the new evolution domain condition v > 0 allows us to rewrite v ·(v/v) to v. The synchronizability conditions follow immediately from the fact that v > 0 and v > 0. For the synchronized formula, we apply the (DI) rule, so the desired inequality v ≥ v is reduced to v2 ≤ v, that is, v ≤ 1. To this end, v > 0 tells us that the derivative of v, that is, −v2, is always negative, therefore v ≤ 1.

#### **6.3 Model Refinement**

In this example, we consider two abstract models of cars. The first car is able to provide a high amount of constant acceleration a at low velocities, but at a certain velocity vcut the engine switches to a different mode and then provides a lesser, but still constant acceleration acut. The second car is an abstracted version of the first, which ignores this mode change and provides the same constant amount of acceleration a at all velocities. Our aim in this example is to establish a safety envelope around the first car's behavior using the more simply stated second car's dynamics. Hence we show that the second car's velocity is greater than the first's at any position x = x = l. More formally, the behavior of the

first car is expressed as a hybrid program α := ( δ1; ?v = vcut; δ2 ) with two modes: δ1 := (x˙ = v, v˙ = a & v ≤ vcut) and δ2 := (x˙ = v, v˙ = acut). The second car follows the simple dynamics δ := ( ˙x = v, v˙ = a). Our goal is to prove the sequent Γ α; δ (x = x = l ⇒ v ≤ v), where the initial conditions are given by

$$\Gamma := \left( \overline{x} = \underline{x} = 0, 0 < \overline{v} = \underline{v} = v\_0, 0 < v\_{cut}, 0 < a\_{cut} \le a \right)$$

Technically, the (Sync) rule merges one differential dynamics with another, but the program the first car executes is a more complicated composition of dynamics and testing. However, it is possible to synchronize *piecewise*, first synchronizing δ with δ1 until the first car changes modes, then synchronizing δ with δ2 for the remainder of their runs. This slightly generalized synchronization procedure means that we can instead show

$$F \vdash \left[ \overline{\delta\_1} \otimes\_{\left( \overline{x}, \underline{x} \right)} \underline{\delta}; ? \overline{v} = v\_{cut}; \overline{\delta\_2} \otimes\_{\left( \overline{x}, \underline{x} \right)} \underline{\delta} \right] \left( \underline{x} = \overline{x} = l \Rightarrow \underline{v} \le \overline{v} \right)$$

There are also now two sets of synchronizability conditions to satisfy, but both are again straightforward. Since δ1 and δ are nearly identical (except for the evolution domain constraint), their synchronization δ1⊗(x,x) δ basically identifies the two dynamics. The synchronization of δ2 and δ is exactly the synchronization performed above in Section 6.1, and proceeds in the same way.

## **7 Conclusions and Future Work**

In this paper, we present a relational extension of the differential dynamic logic based on time stretching of dynamics. This reparametrization enables us to enforce that comparisons between two systems occur when certain conditions are satisfied, for example when two cars are passing through the same position. While such reparametrizations can be thought of as stretching or compressing time for one of the dynamics, we also show they can be conducted by a transformation of the dynamics themselves, based on Lie derivatives. We call this process *synchronizing* the dynamics (Definition 19), and it leads us to a new dL proof rule, the (Sync) rule (Theorem 24). We implemented the new rule in the KeYmaera X tool and use our extension to demonstrate several nontrivial relational properties of dynamical systems.

In the future, we think it would be interesting to combine our relational logic with orthogonal relational extensions of dL [14] which focus on *refinement relations* with varying levels of nondeterminism. We also hinted in our last case study that it is possible to synchronize wider classes of hybrid programs than just two differential dynamics. We also think that the level of automated proof search available in KeYmaera X may enable the automatic detection of monotonic properties in *product lines*. This may be useful in industry both to provide sanity checks on formalized models of products, as well as enabling strong guarantees to be more easily obtained for those models.

## **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), 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, you will need to obtain permission directly from the copyright holder.

## Verifying Concurrent Systems

#### Assume, Guarantee or Repair*-*

Hadar Frenkel1, Orna Grumberg1, Corina Pasareanu2 and Sarai Sheinvald3

1 Department of Computer Science, The Technion, Haifa, Israel

2 Carnegie Mellon University and NASA Ames Research Center, CA, USA

3 Department of Software Engineering, Braude College of Engineering, Karmiel, Israel

Abstract. We present Assume-Guarantee-Repair (AGR) – a novel framework which not only verifies that a program satisfies a set of properties, but also *repairs* the program in case the verification fails. We consider *communicating programs* – these are simple C-like programs, extended with synchronous communication actions over communication channels. Our method, which consists of a learning-based approach to assume-guarantee reasoning, performs verification and repair simultaneously: in every iteration, AGR either makes another step towards proving that the (current) system satisfies the specification, or alters the system in a way that brings it closer to satisfying the specification. We manage handling infinite-state systems by using a finite abstract representation, and reduce the semantic problems in hand – satisfying complex specifications that also contain first-order constraints – to syntactic ones, namely membership and equivalence queries for regular languages. We implemented our algorithm and evaluated it on various examples. Our experiments present compact proofs of correctness and quick repairs.

#### 1 Introduction

Verification of large-scale systems is a main challenge in the field of formal verification. Often, the verification process of such a system does not scale well. *Compositional verification* aims to verify small components of a system separately, and from the correctness of the individual components, to conclude the correctness of the entire system. This, however, is not always possible, since the correctness of a component often depends on the behavior of its environment.

The Assume-Guarantee (AG) style compositional verification [22,26] suggests a solution to this problem. The simplest AG rule checks if a system composed of components M1 and M2 satisfies a property P by checking that M1 under assumption A satisfies P and that any system containing M2 as a component satisfies A. Several frameworks have been proposed to support this style of reasoning. Finding a suitable assumption A is then a common challenge in such frameworks.

In this work, we present *Assume-Guarantee-Repair* (AGR) – a fully automated framework which applies the Assume-Guarantee rule, and while seeking a suitable assumption A, incrementally repairs the given program in case the verification fails. Our framework is inspired by [24], which presented a learning-based method to finding an assumption A, using the L∗ [5] algorithm for learning regular languages.

Our AGR framework handles *communicating programs*. These are infinite-state C-like programs, extended with the ability to synchronously read and write messages over communication channels. We model such programs as finite-state automata over an *action alphabet*, which reflects the program statements. The accepting states in these automata model points of interest in the program that the specification can relate to. The automata representation is similar in nature to that of control-flow graphs. Its advantage, however, is in the ability to exploit an automata-learning algorithm such as L∗.

- This research was partially supported by the Technion Hiroshi Fujiwara Cyber Security Research Center, the Israel National Cyber Directorate and the Israel Science Foundation (ISF)

#### 212 H. Frenkel et al.

The composition of the two program components, M1 and M2, denoted M1||M2, synchronizes on readwrite actions on the same channel. Between two synchronized actions, the individual actions of both systems interleave.

Fig. 1: Modeling a communicating program as an automaton M2

Figure 1 presents the code of a communicating program (left) and its corresponding automaton M2 (right). The automaton alphabet consists of constraints (e.g. xpw ≤ 999), assignment actions (e.g. ypw := 2 · ypw in M1 of Figure 2), and communication actions (e.g. enc!xpw sends the value of variable xpw over channel enc, and getEnc?xpw2 reads a value to xpw2 on channel getEnc).

The specification P is modeled as an automaton that does not contain assignment actions. It may contain communication actions in order to specify behavioral requirements, as well as constraints over the variables of both system components, that express requirements on their values in various points in the runs.

Consider, for example, the program M1 and the specification P seen in Figure 2, and the program M2 of Figure 1. M2 reads a password on channel read to the variable xpw, and once it is long enough (has at least four digits), it sends the value of xpw to M1 through channel enc. M1 reads this value to variable ypw and then applies a simple function that changes its value, and sends the changed variable back to M2. The property P reasons about the parallel run of the two programs. The pair (getEnc?xpw2, getEnc!ypw) denotes a synchronization of M1 and M2 on channel getEnc. P makes sure that the parallel run of M1 and M2 always reads a value and then encrypts it – a temporal requirement. In addition, it makes sure that the value after encryption is different than the original value, and that there is no overflow – both are semantic requirements on the program variables. That is, P expresses temporal requirements that contain first order constraints. In case one of the requirements does not hold, P reaches the state r4 which is an error state. Note that P here is not complete, for simplicity of presentation (see Definition 5 for a formal definition of a complete program).

Fig. 2: The programs M1, M2, and the specification P

The L∗ algorithm aims at learning a regular language U. Its entities consist of a *teacher* – an oracle who answers *membership queries* ("is the word w in U?") and *equivalence queries* ("is A an automaton whose language is U?"), and a *learner*, who iteratively constructs a finite deterministic automaton A for U by submitting a sequence of membership and equivalence queries to the teacher.

In using the L∗ algorithm for learning an assumption A for the AG-rule, membership queries are answered according to the satisfaction of the specification P: If M1||t satisfies P, then the trace t in hand should be in A. Otherwise, t should not be in A. Once the learner constructs a stable system A, it submits an equivalence query. The teacher then checks whether A is a suitable assumption, that is, whether M1||A satisfies P, and whether the language of M2 is contained in the language of A. According to the results, the process either continues or halts with an answer to the verification problem. The learning procedure aims at learning the weakest assumption Aw, which contains all the traces that in parallel with M1 satisfy P . The key observation that guarantees termination in [24] is that the components in this procedure – M1,M2, P and Aw – are all regular.

Our setting is more complicated, since the traces in the components – both the programs and the specification – contain constraints, which are to be checked semantically and not syntactically. These constraints may cause some traces to become infeasible. For example, if a trace contains an assignment x := 3 followed by a constraint x ≥ 4 (modeling an "if" statement), then this trace does not contribute any concrete runs, and therefore does not affect the system behavior. Thus, we must add feasibility checks to the process.

Constraints in the specification also pose a difficulty, as satisfiability of a specification is determined by the semantics of the constraints and not only by the language syntax, and so there is more here to check than standard language containment. Moreover, in our setting Aw above may no longer be regular, see Example 3. However, our method manages to overcome this problem.

As we have described above, not only do we construct a learning-based method for the AG-rule for communicating programs, but we also repair the programs in case the verification fails. An AG-rule can either conclude that M1||M2 satisfies P, or return a real, non-spurious counterexample of a computation t of M1||M2 that violates P. In our case, instead of returning t, we repair M2 in a way that eliminates this counterexample. Our repair is both syntactic and semantic, where for semantic repair we use *abduction* [25] to infer a new constraint which makes the counterexample t infeasible.

Consider again M1 and P of Figure 2 and M2 of Figure 1. The composition M1||M2 does not satisfy P. For example, if the initial value of xpw is 263, then after encryption the value of ypw is 264, violating P. Our algorithm finds a bad trace during the AG stage which captures this bad behavior, and the abduction in the repair stage finds a constraint that eliminates it: xpw < 263, and inserts this constraint to M2.

Following this step we now have an updated M2, and we continue with applying the AG-rule again, using information we have gathered in the previous steps. In addition to removing the error trace, we update the alphabet of M2 with the new constraint.

Continuing our example, in a following iteration AGR will verify that the repaired M2 together with M1 satisfy P, and terminate.

Thus, AGR operates in a verify-repair loop, where each iteration runs a learning-based process to determine whether the (current) system satisfies P, and if not, eliminates bad behaviors from M2 while enriching the set of constraints derived from these bad behaviors, which often leads to a quicker convergence. In case the current system does satisfy P, we return the repaired M2 together with an assumption A that abstracts M2 and acts as a smaller proof for the correctness of the system.

We have implemented a tool for AGR and evaluated it on examples of various sizes and of various types of errors. Our experiments show that for most examples, AGR converges and finds a repair after 2-5 iterations of verify-repair. Moreover, our tool generates assumptions that are significantly smaller then the (possibly repaired) M2, thus constructing a compact and efficient proof of correctness.

214 H. Frenkel et al.

Contributions To summarize, the main contributions of this paper are:

Related Work Assume-guarantee style compositional verification [22,26] has been extensively studied. The assumptions necessary for compositional verification were first produced manually, limiting the practicality of the method.

More recent works [9,16,14,6] proposed techniques for automatic assumption generation using learning and abstraction refinement techniques, making assume-guarantee verification more appealing. In [24,6] alphabet refinement has been suggested as an optimization, to reduce the alphabet of the generated assumptions, and consequently their sizes. This optimization can easily be incorporated into our framework as well.

Other learning-based approaches for automating assumption generation have been described in [7,17,8]. All these works address non-circular rules and are limited to finite state systems. Automatic assumption generation for circular rules is presented in [12,13], using compositional rules similar to the ones studied in [21,23].

Our approach is based on a non-circular rule but it targets complex, infinite-state concurrent systems, and addresses not only verification but also repair. The compositional framework presented in [19] addresses L∗ based compositional verification and synthesis but it only targets finite state systems.

Also related is the work in [18], which addresses automatic synthesis of circular compositional proofs based on logical abduction; however the focus of that work is sequential programs, while here we target concurrent programs. A sequential setting is also considered in [3], where abduction is used for automatically generating a program environment. Our computation of abduction is similar to that of [3]. However, we require our constraints to be over a predefined set of variables, while they look for a minimal set.

The approach presented in [27] aims to compute the *interface* of an infinite-state component. Similar to our work, the approach works with both over- and under- approximations but it only analyzes one component at a time. Furthermore, the component is restricted to be deterministic (necessary for the permissiveness check). In contrast we use both components of a system to compute the necessary assumptions, and as a result they can be much smaller than in [27]. Furthermore, we do not restrict the components to be deterministic and, more importantly, we also address the system repair in case of dissatisfaction.

#### 2 Communicating Programs

In this section we present the notion of *communicating programs*. These are C-like programs, extended with the ability to synchronously read and write messages over communication channels. We model such programs as automata over an *action alphabet* that reflects the program statements. The alphabet includes *constraints*, which are quantifier-free first-order formulas, representing the conditions in *if* and *while* statements. It also includes *assignment statements* and read and write *communication actions*. The automata representation is similar in nature to that of a control-flow graph. Its advantage, however, is in the ability to exploit an automata-learning algorithm such as L∗ for its verification.

We first formally define the alphabet over which communicating programs are defined. Let G be a finite set of communication channels. Let X be a finite set of variables (whose ordered vector is x¯) and D be a (possibly infinite) data domain. For simplicity, we assume that all variables are defined over D. The elements of D are also used as constants in arithmetic expressions and constraints.

Definition 1. *An* action alphabet *is* α = G∪E∪C *where:*

Definition 2. *A* communicating program *(or, a program) is* M = Q, X, α, δ, q0, F *, where:*

	- *–* α ∈G∪E *for all* (q, α, q ) ∈ δ

*That is, for each state it holds that either all outgoing edges are labeled with constraints, or that all outgoing edges are labeled with assignments or communication actions.*

*5.* F ⊆ Q *is the set of accepting states.*

The words that are read along a communicating program are a *symbolic representation* of the program behaviors. We refer to such a word as a *trace*. Each such trace induces *concrete runs* of the program, which are formed by concrete assignments to the program variables in a way that conforms with the actions along the word.

We now formally define these notions.

Definition 3. *A* path *in a program* M *is a finite sequence of states and actions* p = (q0, a1,

q1,...,an, qn)*, starting with the initial state* q0*, such that* ∀0 ≤ i<n *we have* (qi, ai+1, qi+1) ∈ δ*. The* induced trace *of* p *is the sequence* t = (a1,...,an) *of the actions in* p*. If* qn *is accepting, then* t *is an* accepted trace *of* M*.*

From now on we assume that every trace we discuss is induced by some path. We turn to define the concrete runs of the program.

Definition 4. *Let* t = (a1,...,an) *be a trace and let* (β0,...,βn) *be a sequence of valuations (i.e., assignments to the program variables)*4*. Then a sequence* r = (β0, a1, β1, a2,...,an, βn) *is a* run *of* t *if the following holds.*

4 Such valuations are usually referred to as states. We do not use this terminology here in order not to confuse them with the states of the automaton.

*We say that* t *is* feasible *if there exists a run of* t*.*

The *symbolic language* of M, denoted T (M), is the set of all *accepted* traces induced by paths of M. The *concrete language* of M is the set of all runs of accepted traces in T (M). We will mostly be interested in feasible traces, which represent (concrete) runs of the program. Intuitively, the symbolic language of a program M corresponds to its syntactic behavior, while the concrete language corresponds to the semantics of the program.

#### 2.1 Parallel Composition

We now describe and define the parallel run of two communicating programs, and the way in which they communicate.

Let M1 and M2 be two programs, where Mi = Qi, Xi, αi, δi, q0 i , Fi for i ∈ {1, 2}. Let G1, G2 be the sets of communication channels occurring in actions of M1, M2, respectively. We assume X1 ∩ X2 = ∅.

The *interface alphabet* αI of M1 and M2 consists of all communication actions on channels that are common to both components. That is, αI = { g?x, g!x | g ∈ G1 ∩ G2, x ∈ X1 ∪ X2}.

In *parallel composition*, the two components synchronize on their communication interface only when one component writes data through a channel, and the other reads it through the same channel. The two components cannot synchronize if both are trying to read or both are trying to write. We distinguish between communication of the two components with each other (on their common channels), and their communication with their environment. In the former case, the components must "wait" for each other in order to progress together. In the latter case, the communication actions of the two components interleave asynchronously.

Formally, the *parallel composition* of M1 and M2, denoted M1||M2, is the program M = Q, x, α, δ, q0, F defined as follows.

	- (a) For (g ∗ x1, g ∗ x2) ∈ α:
		- i. δ((q1, q2),(g ∗ x1, g ∗ x2)) = (q 1, q 2).

ii. δ((q 1, q 2), x1 == x2)=(δ1(q1, g ∗ x1), δ2(q2, g ∗ x2)).

That is, when a communication is performed synchronously in both components, the data is transformed through the channel from the writing component to the reading component. As a result, the values of x1 and x2 equalize. This is enforced in M by adding a transition labeled by the constraint x1 == x2 that immediately follows the synchronous communication.

That is, on actions that are not in the interface alphabet, the two components interleave.

5. F = F1 × F2

Figure 3 demonstrates the parallel composition of components M1 and M2 of Figures 1 and 2. The program M = M1||M2 reads a password from the environment through channel read. The two components synchronize on channels enc and getEnc.

Fig. 3: Parallel composition M = M1||M2 of components M1 and M2 from Figures 1, 2

#### 3 Regular Properties and Their Satisfaction

In this section we define the syntax and semantics of the properties that we consider. These are properties that can be represented as finite automata, hence the name *regular*. However, the alphabet of such automata includes communication actions and first-order constraints over program variables. Thus, such automata are suitable for specifying the desired and undesired behaviors of communicating programs over time.

In order to define our properties, we first need the notion of a *deterministic and complete* program. The definition is somewhat different from the standard definition for finite automata, since it takes the semantic meaning of constraints into account.

Intuitively, in a deterministic and complete program, every concrete run has exactly one trace that induces it.

Definition 5. *A program over alphabet* α *is* deterministic and complete *if for every state* q *and for every action* a ∈ α *the following hold:*

*1. There is exactly one state* q *such that* (q, a, q ) *is in* δ*.* 5

5 in our examples we sometimes omit the actions that lead to a rejecting sink for the sake of clarity.

*2. If* (q, c1, q ) *and* (q, c2, q) *are in* δ *for constraints* c1, c2 ∈ C *and* q = q*, then* c1 ∧ c2 ≡ f alse*. 3. Let* Cq *be the set of all constraints on transitions leaving* q*. Then* ( - c∈Cq c) ≡ true *.*

A *property* is a deterministic and complete program with no assignment actions.

A trace is accepted by a property P if it reaches a state in F, the set of accepting states of P. Otherwise, it reaches a state in Q \ F, and is rejected by P.

Next, we define the satisfaction relation between a program and a property. Intuitively, a program M satisfies a property P (denoted M - P) if all runs induced by accepted traces of M reach an accepting state in P.

A property P specifies the behavior of a program M by referring to communication actions of M and imposing constraints over the variables of M. Thus, the set of variables of P is identical to that of M. Let G be the set of communication actions of M. Then, αP includes a subset of G as well as constraints over the variables of M. The *interface* of M and P, which consists of the communication actions that occur in P, is defined as αI = G ∩ αP.

In order to capture the satisfaction relation between M and P, we define a *conjunctive composition* between M and P, denoted M × P. In conjunctive composition, the two components synchronize on their common communication actions when both read or both write through the same communication channel. They interleave on constraints and on actions of αM that are not in αP.

Definition 6. *Let* M = QM, XM, αM, δM, qM 0 , FM *be a program and* P = QP , XP , αP, δP , qP 0 , FP *be a property, where* XM = XP *. The* conjunctive composition *of* M *and* P *is* M ×P = Q, X, α, δ, q0, F *, where:*

	- *(a) For* a = (g ∗ x, g ∗ y) ∈ αI*, or* a = g ∗ x ∈ αI*:* δ((q1, q2), a)=(δM(q1, a), δP (q2, a))*.*
	- *(b) For* a ∈ αM \ αI*:* δ((q1, q2), a)=(δM(q1, a), q2)*.*
	- *(c) For* a ∈ αP \ αI*:* δ((q1, q2), a)=(q1, δP (q2, a))*.*

*That is, on actions that are not common communication actions to* M *and* P*, the two components interleave.*

*5.* F = FM × BP *, where* BP = QP \ FP *.*

Note that accepted traces in M × P are those that are accepted in M and rejected in P. Such traces are called *error traces* and their corresponding runs are called *error runs*. Intuitively, an error run is a run along M which violates the properties modeled by P. Such a run either fails to synchronize on the communication actions, or reaches a point in the computation in which its assignments, coming from M, violate some constraint described by P. These runs are manifested in the traces that are accepted in M but are composed with matching traces that are rejected in P. We can now formally define when a program satisfies a property.

Definition 7. *For a program* M *and a property* P*, we define* M - P *iff* M ×P *contains no feasible accepted traces.*

6 Note that communication actions of the form (g ∗ x, g ∗ y) can only appear if M is a parallel composition of two programs.

Thus, a feasible error trace in M × P is an evidence to M - P, since it indicates the existence of a run that violates P.

*Example 2.* Consider the program M of Figure 3 and the property P of Figure 2. As we discussed in Section 1, M - P. The trace t = read?xpw, 999 < xpw,(enc!xpw, enc?ypw), xpw == ypw, ypw := 2 · ypw,(getEnc?xpw2, getEnc!ypw), xpw2 == ypw, xpw! = xpw2, ypw ≥ 264 is a feasible error trace in M × P proving that an overflow is possible.

#### 4 The Assume-Guarantee-Repair (AGR) Framework

In this section we discuss our Assume-Guarantee-Repair (AGR) framework for communicating programs. The framework consists of a learning-based Assume-Guarantee algorithm, called AGL∗ , and a REPAIR procedure, which are tightly joined.

Let M1 and M2 be two programs, and let P be a property. The classical Assume-Guarantee (AG) proof rule [26] assures that if we find an assumption A (in our case, a communicating program) such that M1||A - P and M2 - A both hold, then M1||M2 - P holds as well. For LTSs [9], the AG-rule is guaranteed to either prove correctness or return a real (non-spurious) counterexample. The work in [9] relies on the L∗ algorithm [5] for learning an assumption A for the AG-rule. In particular, L∗ aims at learning Aw, the weakest assumption for which M1||Aw - P holds. A crucial point of this method is the fact that Aw is *regular* [15], and thus can be learned by L∗.

Lemma 1. *For infinite-state communicating programs, the weakest assumption* Aw *is not always regular.*

*Example 3.* Consider the programs M1, M2 and the property P of Figure 4. The weakest assumption with which M1 satisfies P should contain exactly all traces (over the alphabet of M2) that contain equally many actions of the form x := x + 1 and y := y + 1. This set of traces is not regular, and therefore cannot be learned by L∗.

Fig. 4: A system for which the weakest assumption is not regular

To cope with this difficulty, we change the target of learning. Instead of learning the (possibly) nonregular language of Aw, we learn T (M2), the set of accepted traces of M2. This language is guaranteed to be regular, as it is represented by the automaton M2.

Note that in case that M1||M2 - P, repair is never needed, and M2 is a valid assumption. In the worst case, the procedure halts once it has learned M2. In particular, in case there are no error traces, termination of our algorithm is guaranteed. If M1||M2 - P then there does not exist a matching assumption, and attempting to learn M2 will reveal this. Therefore, using T (M2) as a learning goal matches the AG rule. The nature of AGL∗ is such that the assumptions it learns before it reaches M2 may contain the traces of M2 and more, but still be represented by a smaller automaton. Therefore, similarly to [9], AGL∗ often terminates with an assumption A that is much smaller than M2. Indeed, our tool often produces very small assumptions (see Section 5).

As mentioned before, not only that we determine whether M1||M2 - P, but we also repair the program in case it violates the specification. When M1||M2 - P, the AGL∗ algorithm returns an error trace t as a witness for the violation. In this case, we initiate the REPAIR procedure, which eliminates t from M2. REPAIR applies abduction in order to learn a new constraint which, when added to t, creates an infeasible trace.7 The new constraint enriches the alphabet in a way which may make similar traces infeasible as well. We elaborate on our use of abduction in Section 4.2. The removal of t and the addition of the new constraint result in a new goal M 2 for AGL∗ to learn. We now return to AGL∗ to search for a new assumption A that allows to verify M1||M 2 -P.

An important feature of our AGR algorithm is its *incrementality*. When learning an assumption A for M 2 we can use the membership queries previously asked for M2, since the answer for them has not been changed. In the full version [1] we prove that the difference between the languages of M2 and M 2 lies in words (traces) whose membership has not yet been queried on M2. This allows the learning of M 2 to start from the point where the previous learning has left off, resulting in a more efficient algorithm.

As opposed to the case where M1||M2 - P, we cannot guarantee the termination of the repair process in case M1||M2 - P. This, since we are only guaranteed to remove one (bad) trace and add one (infeasible) trace in every AGR REPAIR iteration (although in practice, every iteration may remove a larger set of traces). Thus, we may never converge to a repaired system. Nevertheless, in case of property violation, our algorithm always finds an error trace, thus a progress towards a "less erroneous" program is guaranteed.

It should be noted that the AGL∗ part of our AGR algorithm deviates from the AG-rule of [9] in two important ways. First, since the goal of our learning is M2 rather than Aw, our membership queries are different in type and order. Second, in order to identify real error traces and send them to REPAIR as early as possible, we add additional queries to the membership phase that reveal such traces. We then send them to REPAIR without ever passing through equivalence queries, which improves the overall efficiency. Indeed, our experiments include several cases in which all repairs were invoked from the membership phase. In these cases, AGR ran an equivalence query only when it has already successfully repaired M2, and terminated.

#### 4.1 The Assume-Guarantee-Repair (AGR) Algorithm

We now describe our AGR algorithm in more detail (see Algorithm 1). Figure 5 describes the flow of the algorithm. AGR comprises two main parts, namely AGL∗ and REPAIR.

The input to AGR are the components M1 and M2, and the property P. While M1 and P stay unchanged during AGR, M2 keeps being updated as long as the algorithm recognizes that it needs repair (we can guarantee termination in certain cases, as we discuss in Section 4.4).

The algorithm works in iterations, where in every iteration the next updated Mi 2 is calculated, starting with iteration i = 0, where M0 2 = M2. An iteration starts with the membership phase in line 2, and ends either when AGL∗ successfully terminates (line 16) or when procedure REPAIR is called (lines 7 and 24). When a new system Mi 2 is constructed, AGL∗ does not start from scratch. The information that has been used in previous iterations is still valid for Mi 2. The new iteration is given additional new trace(s) that have been added or removed from the previous Mi 2 (lines 9,11,20, 27).

AGL∗ consists of two phases: membership, and equivalence.

The membership phase (lines 2-11) consists of a loop in which the learner constructs the next assumption Ai j according to answers it gets from the teacher on a sequence of membership queries on various traces.

7 There are also cases in which we do not use abduction, as discussed in Section 4.3

Fig. 5: The flow of AGR

These queries are answered in accordance with traces we allow in Ai j : traces in Mi 2 that in parallel with M1 satisfy P. If a trace t ∈ T (Mi 2) in parallel with M1 does not satisfy P, then t is a bad behavior of M2. Therefore, if such a t is found during the membership phase, REPAIR is invoked.

Once the learner reaches a stable assumption Ai j , it passes it to the equivalence phase (lines 12-27). Ai j is a suitable assumption if both M1||Ai j - P and T (Mi 2) ⊆ T (Ai j ) hold. In this case, AGR terminates and returns Mi 2 as a successful repair of M2. If M1||Ai j - P, then a counterexample t is returned, that is composed of bad traces in M1, Ai j , and P. If the bad trace t2, the restriction of t to the alphabet of Ai j , is also in Mi 2, then t2 is a bad behavior of Mi 2, and here too the REPAIR phase is invoked. Otherwise, AGR returns to the membership phase with t2 as a trace that should not be in Ai j , and continues to learn Ai j+1.

As we have described, REPAIR is called when a bad trace t is found in (M1||Mi 2) × P and should be removed. If t contains no constraints then its sequence of actions is illegal and its subtrace t2 from Mi 2 should be removed from Mi 2. In this case, REPAIR returns to AGL∗ with a new learning goal Mi+1 2 such that T (Mi+1 2 ) ⊆ T (Mi 2) \ {t2}, along with the answer "no" to the membership query on t2. In 4.3 we discuss different methods for removing t2 from Mi 2.

The more interesting case is when t contains constraints. In this case, we not only remove the matching t2 from Mi 2, but we also add a new constraint c to the alphabet of Mi+1 2 , which causes t2 to be infeasible. This way we eliminate t2, and may also eliminate a family of bad traces that violate the property in the same manner. We deduce c using abduction, see Section 4.2. As before, REPAIR returns to AGL∗ with a new goal to be learned, but now also with an extended alphabet. The membership phase is then provided with two new answers to the membership query: t2 that should *not* be included in the new assumption, and (t2 · c) that should be included.

Incremental learning One of the advantages of AGR is that it is *incremental*, in the sense that membership answers from previous iterations remain unchanged for the repaired system. Indeed, since this is the first time that AGL∗ queries t2, we can return to AGL∗ with the answer t2 ∈ T / (Mi+1 2 ), without contradicting any previous queries. In addition, t 2 obtained by abduction is a new word (over a new alphabet), which also was not queried earlier. Therefore, we can incrementally add t2 and t 2 as answers from the teacher, and continue to use answers from previous queries on all other traces.

#### 4.2 Repair by Abduction

We now describe the repair we apply to Mi 2, in case the error trace t contains constraints (see Algorithm 1, line 32). Error traces with no constraints are removed from Mi 2 syntactically (line 31), while in abduction we *semantically* eliminate t by making it infeasible. The new constraints are then added to the alphabet of Mi+1 2 in a way that may eliminate additional error traces. Note that even-though we add new alphabet letters to M2, we do not add new *feasible traces*, since the constraints added by abduction can only restrict the behavior of M2, making more traces infeasible. Therefore, we do not add counterexamples to M2.

The process of inferring new constraints from known facts about the program is called *abduction* [11]. We now describe how we apply it. Given a trace t, let ϕt be the first-order formula (a conjunction of constraints), which constitutes the SSA representation of t [4]. In order to make t infeasible, we look for a formula ψ such that ψ ∧ ϕt → false8.

Note that t ∈ T (M1||Mi 2) × P, and so it includes variables both from X1, the set of variables of M1, and from X2, the set of variables of Mi 2. Since we wish to repair Mi 2, the learned ψ is over the variables in X2 only.

The formula ψ ∧ ϕt → false is equivalent to ψ → (ϕt → false). Thus, ψ = ∀x ∈ X1(ϕt → false) ≡ ∀x ∈ X1(¬ϕt), is such a desired constraint: ψ makes t infeasible and is defined only over X2. We now use quantifier elimination [28] to produce a quantifier-free formula over X2. Computing ψ is similar to the abduction suggested in [11], but the focus here is on finding a formula over X2 rather than over any minimal set of variables. We use Z3 [10] to apply quantifier elimination and to generate the new constraint. After generating ψ(X2), we add it to the alphabet of Mi+1 2 (line 35 of Algorithm 1). In addition, we produce a new trace t 2 = t2 · ψ(X2). The trace t 2 is returned as the output of the abduction.

*Example 4.* Recall the error trace t = read?xpw, 999 < xpw,(enc!xpw, enc?ypw), xpw == ypw, ypw := 2 · ypw,(getEnc?xpw2, getEnc!ypw), xpw2 == ypw, xpw! = xpw2, ypw ≥ 264 of Example 2. From t we create the formula ϕt = (999 < xpw) ∧ (ypw = xpw) ∧ (y pw = 2 · ypw) ∧ (xpw2 = y pw) ∧ (xpw = xpw2) ∧ (y pw ≥ 264). We then apply quantifier elimination and simplification on the formula ∀ypw∀y pw(¬ϕt) and get the new constraint xpw < 263.

Lemma 2. *Let* t = (t1||t2) × tP *. If* t2 *is infeasible, then* t *is infeasible as well.*

This is due to the fact that tP can only restrict the behaviors of t1 and t2, thus if t2 is infeasible, t cannot be made feasible. See the full version of the paper [1] for a formal proof. Therefore, by making t2 infeasible, we eliminate the error trace t.

We now want to build a repaired component Mi+1 2 of Mi 2, which includes t2 · ψ(X2) but not t2. To do so, we split the state q that t2 reaches in Mi 2 into two states q, q , and add a transition labeled ψ(X2) from q to q , where only q is now accepting9. Thus, we eliminated a violating trace from M1||Mi 2. AGR now returns to AGL∗ in order to learn an assumption for the repaired component Mi+1 2 , which now includes t 2 but not t2.

#### 4.3 Removal of Error Traces

Recall that the goal of REPAIR is to remove a bad trace t from M2 once it is found by AGL∗ . If t contains constraints, we remove it using abduction. Otherwise, we can remove t by constructing a system whose language is T (M2) \ {t}. We call this the *exact* method for repair. However, removing a single trace at a time may lead to slow convergence, and to an exponential blow-up in the size of the repaired systems. Moreover, as we have discussed, in some cases there are infinitely many such error traces, in which case AGR may never terminate.

For faster convergence, we have implemented two additional heuristics, namely *approximate* and *aggressive*. These heuristics may remove more than a single trace at a time, while keeping the size of the systems small. While "good" traces may be removed as well, the correctness of the repair is maintained, since no bad traces are added. Moreover, an error trace is likely to be in an erroneous part of the system, and in these cases our heuristics manage removing a set of error traces in a single step.

We briefly survey the three methods.

8 Usually, in abduction, we look for ψ such that ψ ∧ ϕt is not a contradiction. In our case, however, since ϕt is a violation of the specification, we want to infer a formula that makes ϕt unsatisfiable. 9 Note that q is an accepting state in Mi

2 since t ∈ T (Mi 2).

#### 4.4 Correctness and Termination

For this discussion, we assume a sound and complete teacher who can answer the membership and equivalence queries in AGL∗ , which require verifying communicating programs and properties with first-order constraints.

As we have discussed earlier, AGR is not guaranteed to terminate, and there are cases where the REPAIR stage may be called infinitely many times. However, in case that no repair is needed, or if a repaired system is obtained after finitely many calls to REPAIR, then AGR is guaranteed to terminate with a correct answer.

To see why, consider a repaired system Mi 2 for which M1||Mi 2 - P. Since the goal of AGL∗ is to syntactically learn Mi 2, which is regular, this stage will terminate at the latest when AGL∗ learns exactly Mi 2 (it may terminate sooner if a smaller appropriate assumption is found). Notice that, in particular, if M1||M2 -P, then AGR terminates with a correct answer in the first iteration of the verify-repair loop.

REPAIR is only invoked when a (real) error trace t is found in Mi 2, in which case a new system Mi+1 2 , that does not include t, is produced by REPAIR. If M1||Mi 2 - P, then an error trace is guaranteed to be found by AGL∗ either in the membership or equivalence phase. Therefore, also in case that Mi 2 violates P, the iteration is guaranteed to terminate. To conclude, we have the following.

Theorem 1. – *An iteration* i *of AGR ends with an error trace* t *iff* M1||Mi 2 - P*, where* Mi 2 *is the repaired system at iteration* i*.*

– *If, after finitely many iterations, a repaired program* M 2 *is such that* M1||M 2 - P*, then AGR terminates with a correct answer.*

We have shown that every iteration of AGR is guaranteed to terminate with a correct answer. The detailed correctness proofs are in the full version of this paper [1].

In particular, since every iteration of AGR finds and removes an error trace t, and no new erroneous traces are introduced in the updated system, then in case that M2 has finitely many error traces, AGR is guaranteed to terminate with a correctly repaired system.

#### 5 Experimental Results and Conclusions

We implemented our AGR framework in Java, integrating L∗ implementation from the LTSA tool [20]. We used Z3 [10] as the teacher for the satisfaction queries in AGL∗ , and for abduction in REPAIR.

Table 1 displays some results of running AGR on various examples, varying in their sizes, types of errors – semantic and syntactic – and their amount. Additional results are in the full version of this paper [1], and the full examples are available on [2]. The *iterations* column indicates the number of iterations of the verify-repair loop, until a repaired M2 is achieved. Examples with no errors were verified in the first iteration, and are indicated by *verification*. We tested the three repair methods described in Section 4.3 for counterexamples without constraints, and used abduction when needed. Figure 6 presents comparisons between the three methods in terms of run-time and the size of the repair and assumptions (note that the graphs are given in logarithmic scale).

Table 1: AGR algorithm results on various examples

Most of our examples model multi-client-server communication protocols, with varying sizes. Our tool managed repairing all these examples when needed.

As can be seen in Table 1, our tool successfully generates assumptions that are significantly smaller than the repaired and the original M2.

For the examples that needed repair, in most cases our tool needed 2-5 iterations of verify-repair in order to successfully construct a repaired component. Interestingly, in example #15 the *aggressive* method converged slower than the *approximate* method. This is due to the structure of M2, in which different error traces lead to different states. Marking these states as non-accepting removed each trace separately. However, some of these traces have a common transition, and preventing this transition from reaching an accepting state, as done in the *approximate* method, managed removing several error traces in a single repair. This example also includes repairs by abduction (as do examples #16, #18 and #19).

Example #22 models a simple structure in which, due to a loop in M2, the same alphabet sequence can generate infinitely many error traces. The *exact* repair method timed out, since it attempted removing one

Fig. 6: Comparing repair methods: time and repair size (logarithmic scale).

error trace at a time. On the other hand, the *aggressive* method removed all accepting states, creating an empty program – a trivial (yet valid) repair. However, the *approximate* method created a valid, non-trivial repair.

Conclusion AGR offers a new take on the learning-based approach to assume-guarantee verification, and manages coping with complex properties and repairing infinite-state programs. Our experimental results show that using existing semantic tools, AGR produces very succinct proofs, and quickly and efficiently repairs flawed communicating programs.

#### References

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), 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, you will need to obtain permission directly from the copyright holder.

## Structural Invariants for the Verification of Systems with Parameterized Architectures

Marius Bozga1, Javier Esparza2 , Radu Iosif1, Joseph Sifakis1 and Christoph Welzel2

1 Univ. Grenoble Alpes, CNRS, Grenoble INP--, Verimag 2 Technische Universitat M¨ unchen ¨

We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata. Components communicate by executing atomic interactions whose participants update their states simultaneously. We introduce an interaction logic to specify both the type of interactions (e.g. rendez-vous, broadcast) and the topology of the system (e.g. pipeline, ring). The logic can be easily embedded in monadic second order logic of κ ≥ 1 successors (WSκS), and is therefore decidable.

Proving safety properties of such a parameterized system, like deadlock freedom or mutual exclusion, requires to infer an inductive invariant that contains all reachable states of all system instances, and no unsafe state. We present a method to automatically synthesize inductive invariants directly from the formula describing the interactions, without costly fixed point iterations. We experimentally prove that this invariant is strong enough to verify safety properties of a large number of systems, including textbook examples (dining philosophers, synchronization schemes), classical mutual exclusion algorithms, cache-coherence protocols and self-stabilization algorithms, for an arbitrary number of components.

## 1 Introduction

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 architecture3 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-o*ff 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:

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-

4 Called in this way by analogy with the notion of traps for Petri Nets [39].

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.

Fig. 1: Parameterized Dining Philosophers

*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 2*n*. 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*:

$$\Gamma\_{\text{philo}} = (\mathbf{g}(\mathbf{i}) \wedge \mathbf{t}(\mathbf{i}) \wedge \mathbf{t}(\text{succ}(\mathbf{i}))) \quad \lor \quad (\mathbf{p}(\mathbf{i}) \wedge \mathbf{t}(\mathbf{i}) \wedge \mathbf{t}(\text{succ}(\mathbf{i}))) \tag{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

$$\begin{aligned} \text{deadlock}(X\_{\textit{w}}, X\_{\textit{e}}, X\_{f}, X\_{b}) &= \forall i \ . \left[ \neg X\_{\textit{w}}(i) \lor \neg X\_{f}(i) \lor \neg X\_{f}(\text{succc}(i)) \right] \land \\ & \quad \left[ \neg X\_{\textit{e}}(i) \lor \neg X\_{b}(i) \lor \neg X\_{b}(\text{succc}(i)) \right] \end{aligned} \tag{2}$$

where *Xw*, *Xe*, *Xf* , *Xb* are set variables, the intended meaning of *Xw*(*i*) resp. *Xe*(*i*) is that the *i*-th philosopher is waiting, resp. eating, and the intended meaning of *Xf*(*i*) resp. *Xb*(*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 .

## 2 Parameterized Component-based Systems

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 = C1 ,...,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 succ0, ..., succκ−1, of arity one. The formulae of ILκ are generated by the syntax

$$\begin{array}{l} t := i \in \mathsf{Val} \mid \mathsf{succc}\_{0}(t) \mid \dots \mid \mathsf{succc}\_{\kappa - 1}(t) \begin{array}{l} \mathsf{terms} \\ \phi := t\_{1} \leq t\_{2} \mid \mathsf{pr}(t) \mid \phi\_{1} \land \phi\_{2} \mid \neg \phi\_{1} \mid \exists i \; . \ \phi\_{1} \; \text{formulaae} \end{array} \end{array}$$

Abbreviations like *t*1 = *t*2, *t*1 < *t*2, φ1 ∨ φ2, φ1 ↔ φ2, and ∀*i* . φ are defined as usual. 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 *w*0,*w*1,...,*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 succ0,...,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 succ0 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:

$$\forall i \forall j \ . \bigwedge\_{\substack{p, q \in \mathsf{Preed} \\ \mathsf{type}(p) = \mathsf{type}(q)}} p(i) \land q(j) \to i \neq j \tag{3}$$

with a finite disjunction of formulae of the form:

$$\mathfrak{C}(i\_1, \ldots, i\_\ell) \stackrel{\text{def}}{=} \varphi \; \wedge \; \bigwedge\_{j=1}^\ell p\_j(i\_j) \; \wedge \; \bigwedge\_{j=1}^m \forall k \; . \; \psi\_j \to q\_j(k) \tag{4}$$

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 = C1 ,C2 ,Γ, where C1 and C2 have ports *p*1 and *p*2, respectively, and Γ has one single clause

$$\mathfrak{C}(i,j,k) = (i < j \land k = \text{succc}(j)) \quad \land \ (p\_1(i) \land p\_2(j)) \quad \land \ \forall i. i > k \to p\_1(i)$$

Γ states that an interaction consists of: the *i*-th process of type C1 executes transition *p*1; the *j*-th process of type C2 executes *p*2; and, for every *i* > (*j*+1) mod *n*, the *i*-th process of type C1 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,...,*qm* 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 I1 = (U,ι1) and I2 = (U,ι2) sharing the same universe U, we say I1 I2 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 |= φ.

#### 2.1 Execution Semantics of Component-based Systems

The semantics of a component-based system S = C1 ,...,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.

Preliminaries: Petri Nets. A *Petri Net* (PN) is a tuple N = *S*,*T*,*E*, where *S* is a set of *places*, *T* is a set of *transitions*, *S* ∩*T* = ∅, and *E* ⊆ (*S* ×*T*)∪(*T* ×*S* ) is a set of *arcs*. The elements of *S* ∪*T* are called *nodes*. Given nodes *x*, *y* ∈ *S* ∪*T*, we write *E*(*x*, *y*) def = 1 if (*x*, *y*) ∈ *E* and *E*(*x*, *y*) def = 0, otherwise. For a node *x*, let • *x* def = {*y* ∈ *S* ∪*T* | *E*(*y*, *x*) = 1}, *x*• def = {*y* ∈ *S* ∪*T* | *E*(*x*, *y*) = 1} and lift these definitions to sets of nodes.

A *marking* of N is a function m : *S* → N. A transition *t* is *enabled* in m if and only if m(*s*) > 0 for each place *s* ∈ •*t*. For all markings m, m and transitions *t*, we write m *t* −→ m whenever *t* is enabled in m and m (*s*) = m(*s*)− *E*(*s*,*t*)+ *E*(*t*,*s*), for all *s* ∈ *S* .  A marking m is *reachable* in N if there exists a firing sequence σ such that m0 σ −→ m. We denote by R(N) the set of reachable markings of N. A marked PN N is 1*-safe* if m(*s*) ≤ 1, for each *s* ∈ *S* and m ∈ R(N). All PNs considered in the following will be 1-safe and we shall silently blur the distinction between a marking m : *S* → {0,1} and the boolean valuation βm : *S* → {⊥,} defined as βm(*s*) = ⇐⇒ m(*s*) = 1. A set of markings M is an *inductive invariant* of N = (N,m0) if and only if m0 ∈ M and for each m *t* −→ m such that m ∈ M, we have m ∈ M.

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 = C1 ,...,C*N*,Γ be a system. Fix a universe U of Γ. We define a marked Petri Net NU S def = (*S*,*T*,*E*,m0) as follows:

It follows immediately from this definition that NU 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 shows the Petri Net NU S for universe U = {0,1,2}. For clarity,

Fig. 2: Petri Net of the dining philosophers for the universe U = {0,1,2}. In reality, the two pink and green places are only one place.

the places (*f*,0) and (*b*,0) have been duplicated; in reality the two copies are merged. The places of each philosopher are {(*w*,*i*),(*e*,*i*)} for *i* = 0,1,2. For example, transition *i*3 corresponds to the minimal model {(*g*,1),(*t*,1),(*t*,2)}, in which philosopher 1 takes forks 1 and 2.

## 3 Trap Invariants

Given a Petri Net N = (*S*,*T*,*E*), a set of places *W* ⊆ *S* is called a *trap* if and only if *W*• ⊆ •*W*. A trap *W* of N is an *initially marked trap* (IMT) of the marked PN N = (N,m0) if and only if m0(*s*) = for some *s* ∈ *W*.

*Example 3.* {(*f*,1),(*b*,1)} and {(*f*,0),(*b*,1),(*f*,2),(*e*,2)} are two traps of the Petri Net in Figure 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:

$$\Theta(\mathsf{N}) \stackrel{\mathsf{def}}{=} \bigwedge\_{I \in T} \left( \vee\_{\times \in \mathsf{T}} \mathsf{1}\_I \right) \to \left( \vee\_{\mathfrak{y} \in I} \mathsf{y} \right),$$

where each place *x*, *y* ∈ *S* is viewed as a propositional variable. It is not hard to show5 that any boolean valuation β : *S* → {⊥,} that satisfies the trap constraint Θ(N) defines a trap *W*β of N in the obvious sense *W*β = {*s* ∈ *S* | β(*s*) = }. Further, if m0 : *S* → {0,1} is the initial marking of a 1-safe Petri Net N and μ0 def = m0(*s*)=1 *s* is a propositional formula, then every valuation of μ0 ∧Θ(N) defines an IMT of (N,m0). 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.

### 3.1 From ILκ to WSκS

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-

5 See e.g. [8] for a proof.

order variables (also called set variables), denoted as *X*,*Y*,... in the following. The syntax of WSκS is:

$$\begin{aligned} t &:= \overline{\epsilon} \mid \ge |\operatorname{succ}\_0(t)| \mid \dots \mid \operatorname{succ}\_{\kappa}(t) & \text{terms} \\ \phi &:= t\_1 = t\_2 \mid \operatorname{pr}(t) \mid X(t) \mid \phi\_1 \land \phi\_2 \mid \neg \phi\_1 \mid \exists \ge \dots \, \phi\_1 \mid \exists X \, . \phi\_1 \; \operatorname{formula} \end{aligned}$$

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:

*x* ≤ *y* def = ∀*X* . *closed*(*X*)∧ *X*(*x*) → *X*(*y*) *closed*(*X*) def = ∀*x* . *X*(*x*) → κ−1 *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*in* (*x*)...) = *y* by the formula ∃*x*1 ...∃*xn* . *xn* = succ*in* (*x*)∧*y* = succ*i*1 (*x*1)∧ *n*−1 *j*=1 *xj* = succ*ij* (*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:

$$\operatorname{Tr}(\mathbf{succc}\_i(\mathbf{x}) = \mathbf{y}) \stackrel{\mathsf{def}}{=} (\neg \max(\mathbf{x}) \land \operatorname{succc}\_i(\mathbf{x}) = \mathbf{y}) \lor (\max(\mathbf{x}) \land \mathbf{y} = \overline{\mathbf{c}}) \dots$$

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*(φ)*.*

## 3.2 Defining Parameterized Trap Invariants in WSκS

Fix a component-based system S = C1 ,...,C*N*,Γ and recall that every universe U induces a Petri Net NU S whose set of places is -*N k*=1 S*k* ×U. For every state *s* ∈ -*N i*=1 S*i* , let *Xs* 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 NU 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 NU S: *P* is a trap of NU S iff the assignment *Xq* → {*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 NU S. For every clause C of Γ, of the form (4), we define the WSκS formulae:

$$\text{intersects-pre}\_{\mathcal{S}}^{\mathbb{E}}(\overline{X}, \mathbf{x}\_{1}, \dots, \mathbf{x}\_{\ell}) = \bigvee\_{j=1}^{\ell} X \bullet\_{P\_{j}} (\mathbf{x}\_{j}) \vee \bigvee\_{j=\ell+1}^{\ell+m} \exists \mathbf{x}\_{j} \cdot \operatorname{Tr}(\psi\_{j}) \wedge X \bullet\_{P\_{j}} (\mathbf{x}\_{j}) \text{ and } \mathbf{x}\_{\ell} \text{ in } \mathbf{x}\_{\ell} \text{ in } \mathbf{x}\_{\ell} \text{ in } \mathbf{x}\_{\ell} \text{ in } \mathbf{x}\_{\ell} \text{ in } \mathbf{x}\_{\ell} \text{ in } \mathbf{x}\_{\ell} \text{ in } \mathbf{x}\_{\ell} \text{ in } \mathbf{x}\_{\ell} \text{ in } \mathbf{x}\_{\ell} \text{ in } \mathbf{x}\_{\ell} \text{ in } \mathbf{x}\_{\ell}}{\forall \mathbf{x}\_{\ell}}$$

$$\text{intersects-post}\_{\mathcal{S}}^{\mathbb{E}}(\overline{X}, \mathbf{x}\_{1}, \dots, \mathbf{x}\_{\ell}) = \bigvee\_{j=1}^{\ell} X\_{P\_{j}} \bullet \left(\mathbf{x}\_{j} \right) \vee \bigvee\_{j=\ell+1}^{\ell+m} \exists \mathbf{x}\_{j} \dots \operatorname{Tr}(\psi\_{j}) \wedge X\_{P\_{j}} \bullet \left(\mathbf{x}\_{j} \right) .$$

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)) of Γ

$$\begin{array}{c} \mathsf{V}\mathsf{x}\_{1}\ldots\mathsf{V}\mathsf{x}\_{\ell} \cdot \left[ Tr(\varphi) \wedge \mathsf{intersets-pre} \frac{\mathbb{C}}{\mathbb{S}} (\overline{\mathsf{X}}, \mathsf{x}\_{1}, \ldots, \mathsf{x}\_{\ell}) \right] \\ \rightarrow \mathsf{intersets-post} \frac{\mathbb{C}}{\mathbb{S}} (\overline{\mathsf{X}}, \mathsf{x}\_{1}, \ldots, \mathsf{x}\_{\ell}). \end{array} \tag{5}$$

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:

Lemma 2. *Given a component-based system* S = C1 ,...,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* ∈ ι(*Xs*)} *is a trap of* NU 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 1 safe, 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 ss*∈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:

$$
bar{\operatorname{sing}}\_{\mathcal{S}}(\overline{X}) = \forall \mathbf{x} \cdot \bigwedge\_{1 \le i \le N} \bigvee\_{s \in S} \left( X\_s(\mathbf{x}) \wedge \bigwedge\_{s' \in S'} \neg X\_{s'}(\mathbf{x}) \right).$$

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

$$\text{intersection}\_{\mathfrak{S}}(\overline{X}, \overline{X'}) = \exists \boldsymbol{\alpha} \; . \quad \bigvee\_{s \in \bigcup\_{1 \le i \le N} \mathbb{S}^{l}} (X\_s(\boldsymbol{\alpha}) \wedge X'\_s(\boldsymbol{\alpha})) .$$

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

$$\text{initially-mark}\_{\mathcal{S}}(\overline{\mathcal{X}}) = \exists \mathbf{x} \; . \bigvee\_{1 \le i \le N} X\_{s\_0}(\mathbf{x}).$$

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

$$\text{trap-invariants}\_{\mathcal{S}}(\overline{X}) = \forall \overline{X'} \cdot \begin{bmatrix} \text{trap-pred}\_{\mathcal{S}}(\overline{X'}) \land \text{initially-marked}\_{\mathcal{S}}(\overline{X'})\\ \to \text{intersection}\_{\mathcal{S}}(\overline{X}, \overline{X'}) . \end{bmatrix} \tag{6}$$

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* NU 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.

## 4 Refining Trap Invariants

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.

Fig. 3: Alternating Dining Philosophers Structural Invariants for Parameterized Architectures 239

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.

#### 4.1 One Invariants

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.

Definition 1. *Given a marked PN* N = ((*S*,*T*,*E*),m0)*, with S* = {*s*1,...,*sn*}*, a vector* a = (*a*1,...,*an*) ∈ {0,1} *n is a* 1-invariant *of* N *if and only if, for each reachable marking* m ∈ R(N)*, we have n i*=1 *ai* ·m(*si*) = 1*.*

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.

Lemma 3. *Given a marked PN* N = ((S,*T*,*E*),m0)*, a set of places* F ⊆ S *is a* 1 *invariant if the following hold:*

$$I.\quad\sum\_{s}\mathfrak{m}\_{0}(s) = 1,$$

*s*∈F *2. either* ||F∩•*t* || = ||F∩*t* • || = *k with k* ∈ {0,1} *or* ||F∩•*t* || > 1 *for every t* ∈ *T.*

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 *Xs* for each state *s* ∈ -*N i*=1 S*i* and define the following formulae:

Given a transition *t* of the marked Petri Net NU S defining the execution semantics of a component-based system S, for a universe U, we consider the following formulae:

Now we define a predicate *1*-*pred*S which consists of a conjunction of *unique*-*init*S and the formulae:

$$\begin{array}{l} \vee \vee \iota\_{1}, \dots, \vee \iota\_{\ell} \ . (Tr(\varphi) \to [\neg intersects\neg pre\prescript{\mathbb{Q}}{}{\mathbb{S}} \land \neg intersects\neg post\prescript{\mathbb{Q}}{}{\mathbb{S}} \\ \vee \ unique\ prere{\prescript{\mathbb{Q}}{}} \wedge \ unique\ post\prescript{\mathbb{Q}}{}{\mathbb{S}} \\ \vee \text{intersects\neg pre\prescript{\mathbb{Q}}{}{\mathbb{S}} \land \neg uniqueppre\prescript{\mathbb{Q}}{}{\mathbb{S}}} \end{array} \tag{8}$$

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

Lemma 4. *Let* S = C1 ,...,C*N*,Γ *be a component-based system and let X be a tuple of set variables, one for each state in a component of* S*. Then, for any structure* (U,ι) *such that* ι *interprets the variables in X, the set P* = {*s*,*u* ∈ -*N i*=1 S*i* ×U | *u* ∈ ι(*Xs*)} *is a* 1*-invariant of* NU S *if* (U,ι) |=WSκS *1*-*pred*S(*X*)*.*

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

$$I \text{-} invariant\_{\mathcal{S}}(\overline{X}) = \forall \overline{X'} \quad I \text{-} pred\_{\mathcal{S}}(\overline{X'}) \to \text{unique} \text{-} intersection\_{\mathcal{S}}(\overline{X}, \overline{X'}). \tag{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:*

$$\exists \overline{X} \; . \; marking\_{\mathcal{S}}(\overline{X}) \land I \; \text{imvariant}\_{\mathcal{S}}(\overline{X}) \land trap \; \text{imvariant}\_{\mathcal{S}}(\overline{X}) \land \neg \varphi(\overline{X}) \qquad (10)$$

*is unsatisfiable, then for every universe* U*, the property defined by the formula* ϕ(*X*) *holds in every reachable marking of* NU S *.*

## 5 Experiments

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:

	- 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.

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.