arXiv subjects

Jérôme Leroux

Publications and source records attributed to Jérôme Leroux.

At least 19 recordsLinked to original sources

arXiv2026

Structural Liveness of Conservative Petri Nets

We show that the EXPSPACE-hardness result for structural liveness of Petri nets [Jancar and Purser, 2019] holds even for a simple subclass of conservative nets. As our main result, we prove that for structurally live conservative nets, the values of the minimal live markings are at most doubly exponential in the size of the net. This implies the EXPSPACE-completeness of structural liveness for conservative Petri nets. The result also applies to structurally bounded Petri nets, whereas the complexity of the general case remains open. As a proof ingredient of independent interest, we present an extension of known results on the bounds of minimal integer solutions to Boolean combinations of linear equalities, inequalities, and divisibility constraints.

cs.LO↗

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

Reachability in VASS Extended with Integer Counters

We consider a variant of VASS extended with integer counters, denoted VASS+Z. These are automata equipped with N and Z counters; the N-counters are required to remain nonnegative and the Z-counters do not have this restriction. We study the complexity of the reachability problem for VASS+Z when the number of N-counters is fixed. We show that reachability is NP-complete in 1-VASS+Z (i.e. when there is only one N-counter) regardless of unary or binary encoding. For $d \geq 2$, using a KLMST-based algorithm, we prove that reachability in d-VASS+Z lies in the complexity class $\mathcal{F}_{d+2}$. Our upper bound improves on the naively obtained Ackermannian complexity by simulating the Z-counters with N-counters. To complement our upper bounds, we show that extending VASS with integer counters significantly lowers the number of N-counters needed to exhibit hardness. We prove that reachability in unary 2-VASS+Z is PSPACE-hard; without Z-counters this lower bound is only known in dimension 5. We also prove that reachability in unary 3-VASS+Z is TOWER-hard. Without Z-counters, reachability in 3-VASS has elementary complexity and TOWER-hardness is only known in dimension 8.

cs.FL↗

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

Extending the Ginsburg-Spanier Theorem to Functions and Mixed Arithmetic

We study sets and functions definable in the three additive theories $\FO(\Z,+,\leq)$, $\FO(\R,+,\leq)$, and $\FO(\R,\Z,+,\leq)$. The Ginsburg--Spanier theorem~\cite{GS66} characterizes $\FO(\Z,+,\leq)$-definable sets as exactly the semi-linear sets. We extend this characterization in two directions. First, we show that $\FO(\Z,+,\leq)$-definable \emph{functions} are exactly the piecewise linear functions (Theorem~\ref{thm:integer}), and that $\FO(\R,+,\leq)$-definable functions are also exactly the piecewise linear functions (Theorem~\ref{thm:real}). The proofs are direct algebraic arguments using only a stability lemma and the Ginsburg--Spanier theorem. Second, we introduce \emph{semi-polinear sets} as the $\FO(\R,\Z,+,\leq)$ analogue of semi-linear sets, and prove that the class of mixed-linear sets and the class of semi-polinear sets coincide (Theorem~\ref{thm:mixed-sets}). We further show that $\FO(\R,\Z,+,\leq)$-definable functions are exactly the \emph{piecewise-simple} functions (Theorem~\ref{thm:mixed-functions}), a new class of functions that are linear in the integer part and in the fractional part of the argument, but with potentially different linear coefficients for each. These algebraic characterizations unify the three theories in a single framework, and the proofs are purely algebraic, without reference to automata or machines.

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↗

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↗

arXiv2024

On the Home-Space Problem for Petri Nets and its Ackermannian Complexity

A set of configurations $H$ is a home-space for a set of configurations $X$ of aPetri net if every configuration reachable from (any configuration in) $X$ can reach (some configuration in) $H$. The semilinear home-space problem for Petri nets asks, given a Petri net and semilinear sets of configurations $X$, $H$, if $H$ is a home-space for $X$. In 1989, David de Frutos Escrig and Colette Johnen proved that the problem is decidable when $X$ is a singleton and $H$ is a finite union of linear sets with the same periods. In this paper, we show that the general (semilinear) problem is decidable. This result is obtained by proving a duality between the reachability problem and the non-home-space problem. In particular, we prove that for any Petri net and any semilinear set of configurations $H$ we can effectively compute a semilinear set $C$ of configurations, called a non-reachability core for $H$, such that for every set $X$ the set $H$ is not a home-space for $X$ if, and only if, $C$ is reachable from $X$. We show that the established relation to the reachability problem yields the Ackermann-completeness of the (semilinear) home-space problem. For this we also show that, given a Petri net with an initial marking, the set of minimal reachable markings can be constructed in Ackermannian time.

cs.LO↗

arXiv2024

Invariants for One-Counter Automata with Disequality Tests

We study the reachability problem for one-counter automata in which transitions can carry disequality tests. A disequality test is a guard that prohibits a specified counter value. This reachability problem has been known to be NP-hard and in PSPACE, and characterising its computational complexity has been left as a challenging open question by Almagor, Cohen, Pérez, Shirmohammadi, and Worrell (2020). We reduce the complexity gap, placing the problem into the second level of the polynomial hierarchy, namely into the class $\mathsf{coNP}^{\mathsf{NP}}$. In the presence of both equality and disequality tests, our upper bound is at the third level, $\mathsf{P}^{\mathsf{NP}^{\mathsf{NP}}}$. To prove this result, we show that non-reachability can be witnessed by a pair of invariants (forward and backward). These invariants are almost inductive. They aim to over-approximate only a "core" of the reachability set instead of the entire set. The invariants are also leaky: it is possible to escape the set. We complement this with separate checks as the leaks can only occur in a controlled way.

cs.FL↗

arXiv2023

New Lower Bounds for Reachability in Vector Addition Systems

We investigate the dimension-parametric complexity of the reachability problem in vector addition systems with states (VASS) and its extension with pushdown stack (pushdown VASS). Up to now, the problem is known to be $\mathcal{F}_k$-hard for VASS of dimension $3k+2$ (the complexity class $\mathcal{F}_k$ corresponds to the $k$th level of the fast-growing hierarchy), and no essentially better bound is known for pushdown VASS. We provide a new construction that improves the lower bound for VASS: $\mathcal{F}_k$-hardness in dimension $2k+3$. Furthermore, building on our new insights we show a new lower bound for pushdown VASS: $\mathcal{F}_k$-hardness in dimension $\frac k 2 + 4$. This dimension-parametric lower bound is strictly stronger than the upper bound for VASS, which suggests that the (still unknown) complexity of the reachability problem in pushdown VASS is higher than in plain VASS (where it is Ackermann-complete).

cs.FL↗

arXiv2022

Compiling Petri Net Mutual Reachability in Presburger

Petri nets are a classical model of concurrency widely used and studied in formal verification with many applications in modeling and analyzing hardware and software, data bases, and reactive systems. The reachability problem is central since many other problems reduce to reachability questions. The reachability problem is known to be decidable but its complexity is extremely high (non primitive recursive). In 2011, a variant of the reachability problem, called the mutual reachability problem, that consists in deciding if two configurations are mutually reachable was proved to be exponential-space complete. Recently, this problem found several unexpected applications in particular in the theory of population protocols. While the mutual reachability problem is known to be definable in the Preburger arithmetic, the best known upper bound of such a formula was recently proved to be non-elementary (tower). In this paper we provide a way to compile the mutual reachability relation of a Petri net with $d$ counters into a quantifier-free Presburger formula given as a doubly exponential disjunction of $O(d)$ linear constraints of exponential size. We also provide some first results about Presburger formulas encoding bottom configurations.

cs.LO↗

arXiv2022

Lower Bounds on the State Complexity of Population Protocols

Population protocols are a model of computation in which an arbitrary number of indistinguishable finite-state agents interact in pairs. The goal of the agents is to decide by stable consensus whether their initial global configuration satisfies a given property, specified as a predicate on the set of configurations. The state complexity of a predicate is the number of states of a smallest protocol that computes it. Previous work by Blondin \textit{et al.} has shown that the counting predicates $x \geq η$ have state complexity $\mathcal{O}(\log η)$ for leaderless protocols and $\mathcal{O}(\log \log η)$ for protocols with leaders. We obtain the first non-trivial lower bounds: the state complexity of $x \geq η$ is $Ω(\log\log η)$ for leaderless protocols, and the inverse of a non-elementary function for protocols with leaders.

cs.DC↗

arXiv2022

State Complexity of Protocols With Leaders

Population protocols are a model of computation in which an arbitrary number of anonymous finite-memory agents are interacting in order to decide by stable consensus a predicate. In this paper, we focus on the counting predicates that asks, given an initial configuration, whether the number of agents in some initial state $i$ is at least $n$. In 2018, Blondin, Esparza, and Jaax shown that with a fix number of leaders and interaction-width, there exists infinitely many $n$ for which the counting predicate is stably computable by a protocol with at most $O(\log\log(n))$ states. We provide in this paper a matching lower-bound (up to a square root) that improves the inverse-Ackermannian lower-bound presented at PODC in 2021.

cs.LO↗

arXiv2021

New Algorithms for Combinations of Objectives using Separating Automata

The notion of separating automata was introduced by Bojanczyk and Czerwinski for understanding the first quasipolynomial time algorithm for parity games. In this paper we show that separating automata is a powerful tool for constructing algorithms solving games with combinations of objectives. We construct two new algorithms: the first for disjunctions of parity and mean payoff objectives, matching the best known complexity, and the second for disjunctions of mean payoff objectives, improving on the state of the art. In both cases the algorithms are obtained through the construction of small separating automata, using as black boxes the existing constructions for parity objectives and for mean payoff objectives.

cs.GT↗

arXiv2021

The Reachability Problem for Petri Nets is Not Primitive Recursive

We provide an Ackermannian complexity lower bound for the reachability problem for checking programs, a model equivalent to Petri nets. Moreover in fixed dimension $2d+4$, we show that the problem is $\mathbb{F}_d$-hard. As a direct corollary, the reachability problem in dimension 10 is not elementary.

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↗

arXiv2020

Reachability in fixed dimension vector addition systems with states

The reachability problem is a central decision problem for formal verification based on vector addition systems with states (VASS), which are equivalent to Petri nets and form one of the most studied and applied models of concurrency. Reachability for VASS is also inter-reducible with a plethora of problems from a number of areas of computer science. In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We consider VASS of fixed dimension, and obtain three main results. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest reachability witnessing runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional VASS. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest reachability witnessing runs. The smallest dimension for which this was previously known is 14.

cs.FL↗

arXiv2019

Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification

This volume contains the proceedings of the Tenth International Symposium on Games, Automata, Logic and Formal Verification (GandALF 2019). The symposium took place in Bordeaux, France, from the 2nd to the 3rd of September 2010. The GandALF symposium was established by a group of Italian computer scientists interested in mathematical logic, automata theory, game theory, and their applications to the specification, design, and verification of complex systems. Its aim is to provide a forum where people from different areas, and possibly with different backgrounds, can fruitfully interact. GandALF has a truly international spirit, as witnessed by the composition of the program and steering committee and by the country distribution of the submitted papers.

cs.GT↗