242
M. Bozga et al.
constructs for a given formula φ(X) a finite automaton recognizing all the sets X for
which ϕ holds. Since the automaton can have very large alphabets, its transition relation is encoded as a binary decision diagram (BDD). The columns report the number of
states and the number of nodes of the BDD for different formulas. More precisely, the
columns trap, trap-inv, flow, and flow-inv give the sizes of the automata for the formula
trap-pred S ∧ initially-marked S , trap-invariant S , 1-pred S and 1-invariant S respectively.
We write “n.a.” (for “not available”) to indicate that Mona timed out before the automaton was computed.
The first observation is that the satisfiability checks often can be done in very short
time. This is surprising, because the formulas to be checked, namely (7) and (10), exhibit one quantifier alternation (recall that trap-invariant S and 1-invariant S contain universal quantifiers). More specifically, since trap-invariant S is obtained by universally
quantifying over trap-pred S ∧ initially-marked S , one would expect the automaton for
the former to be much larger than the one for the latter, at least in some cases. But this
does not happen: In fact, the automaton for trap-invariant S is almost always smaller.
Similarly, there is no blowup from 1-pred S to 1-invariant S . A possible explanation
could be that the exponential blowup caused by universal quantification in WSκS manifests only on theoretical corner cases, which do not occur in our examples.
6 Conclusions
We have shown that the trap technique used in [11,28,13] for the verification of single
systems can be extended to parameterized systems with sophisticated communication
structures, like pipelines, token rings and trees. Our extension constructs a parameterized trap invariant, a formula of WSκS satisfied by the reachable global states of all
instances of the system. The core of the approach is a purely syntactic, automatic derivation of the trap invariant from the interaction formula describing the possible transitions
of the system. When the set of safe global states can also be expressed in WSκS, which
is usually the case, we check using the Mona tool whether the trap invariant implies
the safety formula. The technique proves correctness of systems that do not produce
well-structured transition systems in the sense of [1,29], and of systems with broadcast
communication, for which, to the best of our knowledge, cut-off results have not been
obtained yet.
Our experiments demonstrate that trap invariants can be very effective in finding
proofs of correctness (inductive invariants) of common benchmark examples. In practice, the technique is very cheap, since it avoids costly fixpoint computations. This
suggests incorporating it into other verifiers as a preprocessing step.
Data Availability Statement and Acknowledgements. The work of the second and fifth
author has received funding from the European Research Council (ERC) under the European
Union’s Horizon 2020 research and innovation programme under grant agreement No 787367
(PaVeS).
The tool ostrich and associated files are available in the Zenodo repository: https://zenodo.org/
record/3676940
M. Bozga et al.
constructs for a given formula φ(X) a finite automaton recognizing all the sets X for
which ϕ holds. Since the automaton can have very large alphabets, its transition relation is encoded as a binary decision diagram (BDD). The columns report the number of
states and the number of nodes of the BDD for different formulas. More precisely, the
columns trap, trap-inv, flow, and flow-inv give the sizes of the automata for the formula
trap-pred S ∧ initially-marked S , trap-invariant S , 1-pred S and 1-invariant S respectively.
We write “n.a.” (for “not available”) to indicate that Mona timed out before the automaton was computed.
The first observation is that the satisfiability checks often can be done in very short
time. This is surprising, because the formulas to be checked, namely (7) and (10), exhibit one quantifier alternation (recall that trap-invariant S and 1-invariant S contain universal quantifiers). More specifically, since trap-invariant S is obtained by universally
quantifying over trap-pred S ∧ initially-marked S , one would expect the automaton for
the former to be much larger than the one for the latter, at least in some cases. But this
does not happen: In fact, the automaton for trap-invariant S is almost always smaller.
Similarly, there is no blowup from 1-pred S to 1-invariant S . A possible explanation
could be that the exponential blowup caused by universal quantification in WSκS manifests only on theoretical corner cases, which do not occur in our examples.
6 Conclusions
We have shown that the trap technique used in [11,28,13] for the verification of single
systems can be extended to parameterized systems with sophisticated communication
structures, like pipelines, token rings and trees. Our extension constructs a parameterized trap invariant, a formula of WSκS satisfied by the reachable global states of all
instances of the system. The core of the approach is a purely syntactic, automatic derivation of the trap invariant from the interaction formula describing the possible transitions
of the system. When the set of safe global states can also be expressed in WSκS, which
is usually the case, we check using the Mona tool whether the trap invariant implies
the safety formula. The technique proves correctness of systems that do not produce
well-structured transition systems in the sense of [1,29], and of systems with broadcast
communication, for which, to the best of our knowledge, cut-off results have not been
obtained yet.
Our experiments demonstrate that trap invariants can be very effective in finding
proofs of correctness (inductive invariants) of common benchmark examples. In practice, the technique is very cheap, since it avoids costly fixpoint computations. This
suggests incorporating it into other verifiers as a preprocessing step.
Data Availability Statement and Acknowledgements. The work of the second and fifth
author has received funding from the European Research Council (ERC) under the European
Union’s Horizon 2020 research and innovation programme under grant agreement No 787367
(PaVeS).
The tool ostrich and associated files are available in the Zenodo repository: https://zenodo.org/
record/3676940