-
On the Reachability Problem for Two-Dimensional Branching VASS
Authors:
Clotilde Bizière,
Thibault Hilaire,
Jérôme Leroux,
Grégoire Sutre
Abstract:
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 be…
▽ More
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.
△ Less
Submitted 27 June, 2025;
originally announced June 2025.
-
An automata-based approach for synchronizable mailbox communication
Authors:
Romain Delpy,
Anca Muscholl,
Grégoire Sutre
Abstract:
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 sen…
▽ More
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.
△ Less
Submitted 19 December, 2024; v1 submitted 9 July, 2024;
originally announced July 2024.
-
Reachability in Two-Dimensional Vector Addition Systems with States: One Test is for Free
Authors:
Jérôme Leroux,
Grégoire Sutre
Abstract:
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 dimensio…
▽ More
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.
△ Less
Submitted 17 July, 2020;
originally announced July 2020.
-
On Functions Weakly Computable by Pushdown Petri Nets and Related Systems
Authors:
J. Leroux,
M. Praveen,
Ph. Schnoebelen,
G. Sutre
Abstract:
We consider numerical functions weakly computable by grammar-controlled vector addition systems (GVASes, a variant of pushdown Petri nets). GVASes can weakly compute all fast growing functions $F_α$ for $α<ω^ω$, hence they are computationally more powerful than standard vector addition systems. On the other hand they cannot weakly compute the inverses $F_α^{-1}$ or indeed any sublinear function. T…
▽ More
We consider numerical functions weakly computable by grammar-controlled vector addition systems (GVASes, a variant of pushdown Petri nets). GVASes can weakly compute all fast growing functions $F_α$ for $α<ω^ω$, hence they are computationally more powerful than standard vector addition systems. On the other hand they cannot weakly compute the inverses $F_α^{-1}$ or indeed any sublinear function. The proof relies on a pumping lemma for runs of GVASes that is of independent interest.
△ Less
Submitted 17 December, 2019; v1 submitted 8 April, 2019;
originally announced April 2019.
-
Occam's Razor Applied to the Petri Net Coverability Problem
Authors:
Thomas Geffroy,
Jérôme Leroux,
Grégoire Sutre
Abstract:
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 appro…
▽ More
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.
△ Less
Submitted 18 July, 2016;
originally announced July 2016.
-
On Boundedness Problems for Pushdown Vector Addition Systems
Authors:
Jérôme Leroux,
Grégoire Sutre,
Patrick Totzke
Abstract:
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…
▽ More
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.
△ Less
Submitted 27 July, 2015;
originally announced July 2015.
-
On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension
Authors:
Jérôme Leroux,
Grégoire Sutre,
Patrick Totzke
Abstract:
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…
▽ More
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.
△ Less
Submitted 29 April, 2015; v1 submitted 13 March, 2015;
originally announced March 2015.
-
Reachability of Communicating Timed Processes
Authors:
Lorenzo Clemente,
Frédéric Herbreteau,
Amélie Stainer,
Grégoire Sutre
Abstract:
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 topolog…
▽ More
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.
△ Less
Submitted 17 October, 2012; v1 submitted 4 September, 2012;
originally announced September 2012.
-
Reachability Analysis of Communicating Pushdown Systems
Authors:
Alexander Heussner,
Jérôme Leroux,
Anca Muscholl,
Grégoire Sutre
Abstract:
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-compl…
▽ More
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.
△ Less
Submitted 28 September, 2012; v1 submitted 3 September, 2012;
originally announced September 2012.
-
Accelerated Data-Flow Analysis
Authors:
Jérôme Leroux,
Gregoire Sutre
Abstract:
Acceleration in symbolic verification consists in computing the exact effect of some control-flow loops in order to speed up the iterative fix-point computation of reachable states. Even if no termination guarantee is provided in theory, successful results were obtained in practice by different tools implementing this framework. In this paper, the acceleration framework is extended to data-flow…
▽ More
Acceleration in symbolic verification consists in computing the exact effect of some control-flow loops in order to speed up the iterative fix-point computation of reachable states. Even if no termination guarantee is provided in theory, successful results were obtained in practice by different tools implementing this framework. In this paper, the acceleration framework is extended to data-flow analysis. Compared to a classical widening/narrowing-based abstract interpretation, the loss of precision is controlled here by the choice of the abstract domain and does not depend on the way the abstract value is computed. Our approach is geared towards precision, but we don't loose efficiency on the way. Indeed, we provide a cubic-time acceleration-based algorithm for solving interval constraints with full multiplication.
△ Less
Submitted 10 December, 2008;
originally announced December 2008.
