Author name cluster

Jérôme Leroux

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

13 papers

2 author rows

MFCS Conference 2025 Conference Paper

On the Reachability Problem for Two-Dimensional Branching VASS

Clotilde Bizière
Thibault Hilaire
Jérôme Leroux
Grégoire Sutre

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.

Details

Highlights Conference 2024 Conference Abstract

On the Home-Space Problem for Petri Nets

Jérôme Leroux

A set of configurations H is a home-space for a set of configurations X of a Petri 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 presentation, 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.

Details

GandALF Workshop 2021 Workshop Paper

New Algorithms for Combinations of Objectives using Separating Automata

Ashwani Anand
Nathanaël Fijalkow
Aliénor Goubault-Larrecq
Jérôme Leroux
Pierre Ohlmann

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.

PDF Details DOI

Highlights Conference 2021 Conference Abstract

The Reachability Problem for Petri Nets is Not Primitive Recursive

Jérôme Leroux

We present a way to lift up the Tower complexity lower bound of the reachability problem for Petri nets to match the Ackermannian upper bound closing a long standing open problem. We also prove that the reachability problem in dimension 17 is not elementary.

Details

FOCS Conference 2021 Conference Paper

The Reachability Problem for Petri Nets is Not Primitive Recursive

Jérôme Leroux

Details

MFCS Conference 2019 Conference Paper

Petri Net Reachability Problem (Invited Talk)

Jérôme Leroux

Details

STOC Conference 2019 Conference Paper

The reachability problem for Petri nets is not elementary

Wojciech Czerwinski
Slawomir Lasota 0001
Ranko Lazic 0001
Jérôme Leroux
Filip Mazowiecki

Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verification. Decidability was proved by Mayr in his seminal STOC 1981 work, and the currently best published upper bound is non-primitive recursive Ackermannian of Leroux and Schmitz from LICS 2019. We establish a non-elementary lower bound, i.e. that the reachability problem needs a tower of exponentials of time and space. Until this work, the best lower bound has been exponential space, due to Lipton in 1976. The new lower bound is a major breakthrough for several reasons. Firstly, it shows that the reachability problem is much harder than the coverability (i.e., state reachability) problem, which is also ubiquitous but has been known to be complete for exponential space since the late 1970s. Secondly, it implies that a plethora of problems from formal languages, logic, concurrent systems, process calculi and other areas, that are known to admit reductions from the Petri nets reachability problem, are also not elementary. Thirdly, it makes obsolete the currently best lower bounds for the reachability problems for two key extensions of Petri nets: with branching and with a pushdown stack. At the heart of our proof is a novel gadget so called the factorial amplifier that, assuming availability of counters that are zero testable and bounded by k , guarantees to produce arbitrarily large pairs of values whose ratio is exactly the factorial of k . We also develop a novel construction that uses arbitrarily large pairs of values with ratio R to provide zero testable counters that are bounded by R . Repeatedly composing the factorial amplifier with itself by means of the construction then enables us to compute in linear time Petri nets that simulate Minsky machines whose counters are bounded by a tower of exponentials, which yields the non-elementary lower bound. By refining this scheme further, we in fact establish hardness for h -exponential space already for Petri nets with h + 13 counters.

Details

TCS Journal 2018 Journal Article

Occam's Razor applied to the Petri net coverability problem

Thomas Geffroy
Jérôme Leroux
Grégoire Sutre

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 presented at TACAS in 2016. 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.

Details DOI

Highlights Conference 2018 Conference Abstract

Polynomial Vector Addition Systems With States

Jérôme Leroux

ABSTRACT. The reachability problem for vector addition systems is one of the most diffic ult and central problems in theoretical computer science. The problem is known to be decidable, but despite intense investigation during the last four decades, the exact complexity is still open. For some sub-classes, the complexity of the reachability problem is known. Structurally bounded vector addition systems, the class of vector addition systems with finite reachability sets from any initial configuration, is one of those classes. In fact, the reachability problem was shown to be polynomial-space complete for that class by Praveen and Lodaya in 2008. Surprisingly, extending this property to vector addition systems with states is open. In fact, there exist vector addition systems with states that are structurally bounded but with Ackermannian large sets of reachable configurations. It follows that the reachability problem for that class is between exponential space and Ackermannian. In this paper we introduce the class of polynomial vector addition systems with states, defined as the class of vector addition systems with states with size of reachable configurations bounded polynomially in the size of the initial ones. We prove that the reachability problem for polynomial vector addition systems is exponential-space complete. Additionally, we show that we can decide in polynomial time if a vector addition system with states is polynomial. This characterization introduces the notion of iteration scheme with potential applications to the reachability problem for general vector addition systems.

Details

Highlights Conference 2014 Conference Abstract

Hyper-Ackermannian Bounds for Pushdown Vector Addition Systems

Jérôme Leroux

This paper studies the boundedness and termination problems for vector addition systems equipped with one stack. We introduce an algorithm, inspired by the Karp & Miller algorithm, that solves both problems for the larger class of well-structured pushdown systems. We show that the worst-case running time of this algorithm is hyper-Ackermannian for pushdown vector addition systems. For the upper bound, we introduce the notion of bad nested words over a well-quasi-ordered set, and we provide a general scheme of induction for bounding their lengths. We derive from this scheme a hyper-Ackermannian upper bound for the length of bad nested words over vectors of natural numbers. For the lower bound, we exhibit a family of pushdown vector addition systems with finite but large reachability sets (hyper-Ackermannian). This is a joint work with M. Praveen and Grégoire Sutre. The full paper is available as a CSL-LICS '14 paper.

PDF Details

Highlights Conference 2013 Conference Abstract

Tutorial: The reachability problem for Petri nets

Jérôme Leroux

Systems equipped with counters are central when modeling distributed protocols, programs with recursive parallel threads, programs with pointers, broadcast protocols, databases, etc. When it comes to model-checking counter systems and their variants, the main results are that verification is undecidable when zero-tests are allowed, while several problems can be decided when zero-tests are forbidden - one speaks of VASS, for "vector addition systems with states", or equivalently "Petri nets". In the case of Petri nets, reachability was shown decidable in 1982, and the reachability problem for Petri nets and related decidable problems on subclasses of counter systems are pivot problems not only for the verification of infinite-state systems but also for problems appearing in very active research areas related to various logics and automata for data words/trees. Hence, the design of efficient algorithms for the reachability problem for VASS may have a great impact, not only in the realm of formal verification. It is however a very difficult problem. Therefore, improving the computational cost for solving the reachability problem for Petri nets would also improve the complexity of the formal verification of numerous classes of infinite-state systems. Strikingly, the decision algorithm for Petri net reachability has never been implemented. This is because of its high complexity, both conceptual (the algorithm is very hard to understand and to describe) and computational (it is assumed that the complexity of the algorithm is not primitive-recursive). The general problem is known to be decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition (KLMTS decomposition). Recently, from this decomposition, it was proved that a final configuration is not reachable from an initial one if, and only if, there exists a Presburger inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Presburger formula denotes an inductive invariant, we deduce from this result that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general Petri net reachability problem based on two semi-algorithms. A first one that tries to prove reachability by enumerating finite sequences of actions and a second one that tries to prove non-reachability by enumerating Presburger formulas. In this presentation, we provide a simple proof of the Petri net reachability problem that is not based on the KLMST decomposition. The proof is based on the notion of production relations, inspired from Hauschildt, that directly proves the existence of Presburger inductive invariants. 13: 00 14: 30 Lunch

PDF Details

TIME Conference 2008 Conference Paper

Decomposition of Decidable First-Order Logics over Integers and Reals

Florent Bouchy
Alain Finkel
Jérôme Leroux

We tackle the issue of representing infinite sets of real- valued vectors. This paper introduces an operator for combining integer and real sets. Using this operator, we decompose three well-known logics extending Presburger with reals. Our decomposition splits a logic into two parts: one integer, and one decimal (i. e. on the interval [0, 1]). We also give a basis for an implementation of our representation.

Details

TCS Journal 2008 Journal Article

Structural Presburger digit vector automata

Jérôme Leroux

The least significant digit first decomposition of integer vectors into words of digit vectors provides a natural way for representing sets of integer vectors by automata. In this paper, the minimal automata representing Presburger sets are proved structurally Presburger: automata obtained by moving the initial state and replacing the accepting condition represent Presburger sets.

Details DOI