arXiv subjects

Grégoire Sutre

Publications and source records attributed to Grégoire Sutre.

12 recordsLinked to original sources

arXiv2026

Bridging the Gap Between Plain VASS and Branching VASS

Vectors addition systems with states (VASS), a model equivalent to Petri nets, are finite-state machines with finitely many counters ranging over the natural numbers. The decidable reachability problem for VASS has many applications in logic, automata, and verification. In this paper we study the reachability problem for BVASS, a branching generalization of VASS. We show that BVASS reachability sets are very similar to VASS reachability sets, namely that they are sections of VASS. Our proof relies on a new well-quasi-order (wqo) on BVASS runs that generalizes the well-known wqo on VASS runs. By leveraging an amalgamation property, we prove that every BVASS run can be transformed into an equivalent one of bounded branching complexity. This allows us to derive several results on the geometry of BVASS reachability sets. As an application we obtain that reachability sets of 5-dimensional BVAS are effectively semilinear, as is the case for 5-dimensional VAS.

cs.LO↗

arXiv2026

Solving the Reachability Problem for Branching Vector Addition Systems via Semilinear Inductive Invariants

In this paper, we solve the reachability problem for branching vector addition systems (BVAS), a long standing open problem. Our approach is based on semilinear inductive invariants. More precisely, we prove that if a configuration of a BVAS is not reachable, then there exists an inductive invariant, given as a semilinear set, that does not contain this configuration. Based on this property, we deduce a very simple (enumerative) algorithm solving the reachability problem for BVAS.

cs.LO↗

arXiv2026

A Forward-Only Construction of Semilinear Inductive Invariants for VAS

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.

cs.LO↗

arXiv2026

On Parameterized Verification Over Tree Topologies

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

cs.LO↗

arXiv2026

An automata-based approach for synchronizable mailbox communication

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.

cs.LO↗

arXiv2025

On the Reachability Problem for Two-Dimensional Branching VASS

Vectors addition systems with states (VASS), or equivalently Petri nets, are arguably one of the most studied formalisms for the modeling and analysis of concurrent systems. A central decision problem for VASS is reachability: whether there exists a run from an initial configuration to a final one. This problem has been known to be decidable for over forty years, and its complexity has recently been precisely characterized. Our work concerns the reachability problem for BVASS, a branching generalization of VASS. In dimension one, the exact complexity of this problem is known. In this paper, we prove that the reachability problem for 2-dimensional BVASS is decidable. In fact, we even show that the reachability set admits a computable semilinear presentation. The decidability status of the reachability problem for BVASS remains open in higher dimensions.

cs.LO↗

arXiv2020

Reachability in Two-Dimensional Vector Addition Systems with States: One Test is for Free

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.

cs.LO↗

arXiv2016

Occam's Razor Applied to the Petri Net Coverability Problem

The verification of safety properties for concurrent systems often reduces to the coverability problem for Petri nets. This problem was shown to be ExpSpace-complete forty years ago. Driven by the concurrency revolution, it has regained a lot of interest over the last decade. In this paper, we propose a generic and simple approach to solve this problem. Our method is inspired from the recent approach of Blondin, Finkel, Haase and Haddad. Basically, we combine forward invariant generation techniques for Petri nets with backward reachability for well- structured transition systems. An experimental evaluation demonstrates the efficiency of our approach.

cs.LO↗

arXiv2015

On Boundedness Problems for Pushdown Vector Addition Systems

We study pushdown vector addition systems, which are synchronized products of pushdown automata with vector addition systems. The question of the boundedness of the reachability set for this model can be refined into two decision problems that ask if infinitely many counter values or stack configurations are reachable, respectively. Counter boundedness seems to be the more intricate problem. We show decidability in exponential time for one-dimensional systems. The proof is via a small witness property derived from an analysis of derivation trees of grammar-controlled vector addition systems.

cs.FL↗

arXiv2015

On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension

Does the trace language of a given vector addition system (VAS) intersect with a given context-free language? This question lies at the heart of several verification questions involving recursive programs with integer parameters. In particular, it is equivalent to the coverability problem for VAS that operate on a pushdown stack. We show decidability in dimension one, based on an analysis of a new model called grammar-controlled vector addition systems.

cs.FL↗

arXiv2012

Reachability of Communicating Timed Processes

We study the reachability problem for communicating timed processes, both in discrete and dense time. Our model comprises automata with local timing constraints communicating over unbounded FIFO channels. Each automaton can only access its set of local clocks; all clocks evolve at the same rate. Our main contribution is a complete characterization of decidable and undecidable communication topologies, for both discrete and dense time. We also obtain complexity results, by showing that communicating timed processes are at least as hard as Petri nets; in the discrete time, we also show equivalence with Petri nets. Our results follow from mutual topology-preserving reductions between timed automata and (untimed) counter automata.

cs.LO↗

arXiv2012

Reachability Analysis of Communicating Pushdown Systems

The reachability analysis of recursive programs that communicate asynchronously over reliable FIFO channels calls for restrictions to ensure decidability. Our first result characterizes communication topologies with a decidable reachability problem restricted to eager runs (i.e., runs where messages are either received immediately after being sent, or never received). The problem is EXPTIME-complete in the decidable case. The second result is a doubly exponential time algorithm for bounded context analysis in this setting, together with a matching lower bound. Both results extend and improve previous work from La Torre et al.

cs.LO↗