Parameterized verification of finite-state processes with rendez-vous synchronization is notoriously undecidable when processes are linearly ordered. In this paper we study two kinds of bounds under which we determine the complexity of safety checking over tree topologies. When bounding the depth we obtain that the complexity is related to the fast growing hierarchy. Our second bound limits the alternations between upwards and downwards synchronizations in the tree (phases), and occurs naturally in many concrete settings. If we fix the number of phases then the complexity of safety checking is EXPSPACE complete, and if the number of phases is part of the input it is 2EXPSPACE complete (both for arbitrary depth).

The reachability problem for Vector Addition Systems (VAS) is a central decision problem in the theory of infinite-state systems, first solved by Kosaraju and Mayr in the 1980s. An alternative, conceptually simpler approach introduced by Leroux shows that non-reachability is always witnessed by semilinear inductive invariants, yielding a decision procedure by combining an enumeration of runs with a search for such invariants. However, the construction of these invariants relies on a back-and-forth scheme that depends symmetrically on the source and the target. As a result, the invariants are not guaranteed to reflect the structural properties of the VAS, and the construction is difficult to extend to asymmetric models such as Branching VAS. We introduce a new forward-only construction of semilinear inductive invariants for VAS. Our method builds invariants from the source configuration alone and avoids the need for backward reasoning. This yields invariants that are more canonical and better aligned with the structure of the system. In particular, our method produces periodic inductive invariants for periodic VAS. Beyond its intrinsic interest, our approach provides a step toward extending invariant-based techniques to Branching VAS.

We revisit finite-state communicating systems with round-based communication under mailbox semantics. Mailboxes correspond to one FIFO buffer per process (instead of one buffer per pair of processes in peer-to-peer systems). Round-based communication corresponds to sequences of rounds in which processes can first send messages, then only receive (and receives must be in the same round as their sends). A system is called synchronizable if every execution can be re-scheduled into an equivalent execution that is a sequence of rounds. Previous work mostly considered the setting where rounds have fixed size. Our main contribution shows that the problem whether a mailbox communication system complies with the round-based policy, with no size limitation on rounds, is Pspace-complete. For this we use a novel automata-based approach, that also allows to determine the precise complexity (Pspace) of several questions considered in previous literature.

International audience

Vector addition system with states is an ubiquitous model of computation with extensive applications in computer science. The reachability problem for vector addition systems is central since many other problems reduce to that question. The problem is decidable and it was recently proved that the dimension of the vector addition system is an important parameter of the complexity. In fixed dimensions larger than two, the complexity is not known (with huge complexity gaps). In dimension two, the reachability problem was shown to be PSPACE-complete by Blondin et al. in 2015. We consider an extension of this model, called 2-TVASS, where the first counter can be tested for zero. This model naturally extends the classical model of one counter automata (OCA). We show that reachability is still solvable in polynomial space for 2-TVASS. As in the work Blondin et al., our approach relies on the existence of small reachability certificates obtained by concatenating polynomially many cycles.

The boundedness problem is a well-known exponential-space complete problem for vector addition systems with states (or Petri nets); it asks if the reachability set (for a given initial configuration) is finite. Here we consider a dual problem, the co-finiteness problem that asks if the complement o f the reachability set is finite; by restricting the question we get the co-emptiness (or universality) problem that asks if all configurations are reachable. We show that both the co-finiteness problem and the co-emptiness problem are exponential-space complete. While the lower bounds are obtained by a straightforward reduction from coverability, getting the upper bounds is more involved; in particular we use the bounds derived for reversible reachability by Leroux (2013). The studied problems were motivated by a result for structural liveness of Petri nets; this problem was shown decidable by Jančar (2017), without clarifying its complexity. The structural liveness problem is tightly related to a generalization of the co-emptiness problem, where the sets of initial configurations are (possibly infinite) downward closed sets instead of just singletons. We formulate the problems even more generally, for semilinear sets of initial configurations; in this case we show that the co-emptiness problem is decidable (without giving an upper complexity bound), and we formulate a conjecture under which the co-finiteness problem is also decidable.

International audience

We prove that the reachability relation of two-counter machines with one zero-test and one reset is Presburger-definable and effectively computable. Our proof is based on the introduction of two classes of Presburger-definable relations effectively stable by transitive closure. This approach generalizes and simplifies the existing different proofs and it solves an open problem introduced by Finkel and Sutre in 2000.

Karp and Miller's algorithm is a well-known decision procedure that solves the termination and boundedness problems for vector addition systems with states (VASS), or equivalently Petri nets. This procedure was later extended to a general class of models, well-structured transition systems, and, more recently, to pushdown VASS. In this paper, we extend pushdown VASS to higher-order pushdown VASS (called HOPVASS), and we investigate whether an approach à la Karp and Miller can still be used to solve termination and boundedness. We provide a decidable characterisation of runs that can be iterated arbitrarily many times, which is the main ingredient of Karp and Miller's approach. However, the resulting Karp and Miller procedure only gives a semi-algorithm for HOPVASS. In fact, we show that coverability, termination and boundedness are all undecidable for HOPVASS, even in the restricted subcase of one counter and an order 2 stack. On the bright side, we prove that this semi-algorithm is in fact an algorithm for higher-order pushdown automata.

Whether the reachability problem for branching vector addition systems, or equivalently the provability problem for multiplicative exponential linear logic, is decidable has been a long-standing open question. The one-dimensional case is a generalisation of the extensively studied one-counter nets, and it was recently established polynomial-time complete provided counter updates are given in unary. Our main contribution is to determine the complexity when the encoding is binary: polynomial-space complete.

Driven by the concurrency revolution, the study of the coverability problem for Petri nets has regained a lot of interest in the recent years. A promising approach, which was presented in two papers last year, leverages a downward-closed forward invariant to accelerate the classical backward coverability analysis for Petri nets. In this paper, we propose a generalization of this approach to the class of well-structured transition systems (WSTSs), which contains Petri nets. We then apply this generalized approach to lossy channel systems (LCSs), a well-known subclass of WSTSs. We propose three downward-closed forward invariants for LCSs. One of them counts the number of messages in each channel, and the other two keep track of the order of messages. An experimental evaluation demonstrates the benefits of our approach.

We introduce a logic for specifying trace properties of vector addition systems (VAS). This logic can express linear relations among pumping segments occurring in a trace. Given a VAS and a formula in the logic, we investigate the question whether the VAS contains a trace satisfying the formula. Our main contribution is an exponential space upper bound for this problem. The proof is based on a small model property for the logic. Compared to similar logics that are solvable in exponential space, a distinguishing feature of our logic is its ability to express non-context-freeness of the trace language of a VAS. This allows us to show that the context-freeness problem for VAS, whose complexity was not established so far, is ExpSpace -complete. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Petri nets, or equivalently vector addition systems (VAS), are widely recognized as a central model for concurrent systems. Many interesting properties are decidable for this class, such as boundedness, reachability, regularity, as well as context-freeness, which is the focus of this paper. The context-freeness problem asks whether the trace language of a given VAS is context-free. This problem was shown to be decidable by Schwer in 1992, but the proof is very complex and intricate. The resulting decision procedure relies on five technical conditions over a customized coverability graph. These five conditions are shown to be necessary, but the proof that they are sufficient is only sketched. In this paper, we revisit the context-freeness problem for VAS, and give a simpler proof of decidability. Our approach is based on witnesses of non-context-freeness, that are bounded regular languages satisfying a nesting condition. As a corollary, we obtain that the trace language of a VAS is context-free if, and only if, it has a context-free intersection with every bounded regular language.

In order to verify protocols that tag messages with integer values, we investigate the decidability of the reachability problem for systems of communicating one-counter machines. These systems consist of local one-counter machines that asynchronously communicate by exchanging the value of their counters via, a priori unbounded, FIFO channels. This model extends communicating finite-state machines (CFSM) by infinite-state local processes and an infinite message alphabet. The main result of the paper is a complete characterization of the communication topologies that have a solvable reachability question. As already CFSM exclude the possibility of automatic verification in presence of mutual communication, we also consider an under-approximative approach to the reachability problem, based on rendezvous synchronization.

One approach to model checking software is based on the abstract-check-refine paradigm: build an abstract model, then check the desired property, and if the check fails, refine the model and start over. We introduce the concept of lazy abstraction to integrate and optimize the three phases of the abstract-check-refine loop. Lazy abstraction continuously builds and refines a single abstract model on demand, driven by the model checker, so that different parts of the model may exhibit different degrees of precision, namely just enough to verify the desired property. We present an algorithm for model checking safety properties using lazy abstraction and describe an implementation of the algorithm applied to C programs. We also provide sufficient conditions for the termination of the method.