The Experts below are selected from a list of 360 Experts worldwide ranked by ideXlab platform
Jérôme Leroux - One of the best experts on this subject based on the ideXlab platform.
-
the Reachability Problem for petri nets is not primitive recursive
arXiv: Logic in Computer Science, 2021Co-Authors: Jérôme LerouxAbstract: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.
-
the Reachability Problem for petri nets is not elementary
Journal of the ACM, 2020Co-Authors: Wojciech Czerwinski, Jérôme Leroux, Slawomir Lasota, Ranko Lazic, Filip MazowieckiAbstract:Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modeling 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, currently, the best published upper bound is non-primitive recursive Ackermannian of Leroux and Schmitz from Symposium on Logic in Computer Science 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, which are known to admit reductions from the Petri nets Reachability Problem, are also not elementary. Thirdly, it makes obsolete the current best lower bounds for the Reachability Problems for two key extensions of Petri nets: with branching and with a pushdown stack. We develop a construction that uses arbitrarily large pairs of values with ratio R to provide zero testable counters that are bounded by R. At the heart of our proof is then a novel gadget, the so-called 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. Repeatedly composing the factorial amplifier with itself by means of the former construction 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, already establish hardness for h-exponential space for Petri nets with h + 13 counters.
-
Reachability in fixed dimension vector addition systems with states
International Conference on Concurrency Theory, 2020Co-Authors: Wojciech Czerwinski, Jérôme Leroux, Slawomir Lasota, Ranko Lazic, Filip MazowieckiAbstract:The Reachability Problem is a central decision Problem in verification of vector addition systems with states (VASS). 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 obtain three main results for VASS of fixed dimension. 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 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 ones. 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 runs. The smallest dimension for which this was previously known is 14.
-
the Reachability Problem for petri nets is not elementary
Symposium on the Theory of Computing, 2019Co-Authors: Wojciech Czerwinski, Jérôme Leroux, Slawomir Lasota, Ranko Lazic, Filip MazowieckiAbstract: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.
-
petri net Reachability Problem invited talk
Mathematical Foundations of Computer Science, 2019Co-Authors: Jérôme LerouxAbstract: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. In this presentation, we overview decidability and complexity results over the last fifty years about the Petri net Reachability Problem.
Slawomir Lasota - One of the best experts on this subject based on the ideXlab platform.
-
improved ackermannian lower bound for the petri nets Reachability Problem
arXiv: Formal Languages and Automata Theory, 2021Co-Authors: Slawomir LasotaAbstract:Petri nets, equivalently presentable as vector addition systems with states, are an established model of concurrency with widespread applications. The Reachability Problem, where we ask whether from a given initial configuration there exists a sequence of valid execution steps reaching a given final configuration, is the central algorithmic Problem for this model. The complexity of the Problem has remained, until recently, one of the hardest open questions in verification of concurrent systems. A first upper bound has been provided only in 2015 by Leroux and Schmitz, then refined by the same authors to non-primitive recursive Ackermannian upper bound in 2019. The exponential space lower bound, shown by Lipton already in 1976, remained the only known for over 40 years until a breakthrough non-elementary lower bound by Czerwi{n}ski, Lasota, Lazic, Leroux and Mazowiecki in 2019. Finally, a matching Ackermannian lower bound announced this year by Czerwi{n}ski and Orlikowski, and independently by Leroux, established the complexity of the Problem. Our contribution is an improvement of the former construction, making it conceptually simpler and more direct. On the way we improve the lower bound for vector addition systems with states in fixed dimension (or, equivalently, Petri nets with fixed number of places): while Czerwi{n}ski and Orlikowski prove $F_k$-hardness (hardness for $k$th level in Grzegorczyk Hierarchy) in dimension $6k$, and Leroux in dimension $4k+5$, our simplified construction yields $F_k$-hardness already in dimension $3k+2$.
-
improved ackermannian lower bound for the vass Reachability Problem
arXiv: Formal Languages and Automata Theory, 2021Co-Authors: Slawomir LasotaAbstract:This draft is a follow-up of the Ackermannian lower bound for the Reachability Problem in vector addition systems with states (VASS), recently announced by Czerwinski and Orlikowski. Independently, the same result has been announced by Leroux, but with a significantly different proof. We provide a simplification of the former construction, thus improving the lower bound for VASS in fixed dimension: while Czerwinski and Orlikowski prove $F_k$-hardness in dimension $6k$, and Leroux in dimension $4k+9$, the simplified construction yields $F_k$-hardness already in dimension $3k+2$.
-
the Reachability Problem for petri nets is not elementary
Journal of the ACM, 2020Co-Authors: Wojciech Czerwinski, Jérôme Leroux, Slawomir Lasota, Ranko Lazic, Filip MazowieckiAbstract:Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modeling 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, currently, the best published upper bound is non-primitive recursive Ackermannian of Leroux and Schmitz from Symposium on Logic in Computer Science 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, which are known to admit reductions from the Petri nets Reachability Problem, are also not elementary. Thirdly, it makes obsolete the current best lower bounds for the Reachability Problems for two key extensions of Petri nets: with branching and with a pushdown stack. We develop a construction that uses arbitrarily large pairs of values with ratio R to provide zero testable counters that are bounded by R. At the heart of our proof is then a novel gadget, the so-called 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. Repeatedly composing the factorial amplifier with itself by means of the former construction 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, already establish hardness for h-exponential space for Petri nets with h + 13 counters.
-
Reachability in fixed dimension vector addition systems with states
International Conference on Concurrency Theory, 2020Co-Authors: Wojciech Czerwinski, Jérôme Leroux, Slawomir Lasota, Ranko Lazic, Filip MazowieckiAbstract:The Reachability Problem is a central decision Problem in verification of vector addition systems with states (VASS). 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 obtain three main results for VASS of fixed dimension. 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 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 ones. 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 runs. The smallest dimension for which this was previously known is 14.
-
the Reachability Problem for petri nets is not elementary
Symposium on the Theory of Computing, 2019Co-Authors: Wojciech Czerwinski, Jérôme Leroux, Slawomir Lasota, Ranko Lazic, Filip MazowieckiAbstract: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.
Wojciech Czerwinski - One of the best experts on this subject based on the ideXlab platform.
-
the Reachability Problem for petri nets is not elementary
Journal of the ACM, 2020Co-Authors: Wojciech Czerwinski, Jérôme Leroux, Slawomir Lasota, Ranko Lazic, Filip MazowieckiAbstract:Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modeling 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, currently, the best published upper bound is non-primitive recursive Ackermannian of Leroux and Schmitz from Symposium on Logic in Computer Science 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, which are known to admit reductions from the Petri nets Reachability Problem, are also not elementary. Thirdly, it makes obsolete the current best lower bounds for the Reachability Problems for two key extensions of Petri nets: with branching and with a pushdown stack. We develop a construction that uses arbitrarily large pairs of values with ratio R to provide zero testable counters that are bounded by R. At the heart of our proof is then a novel gadget, the so-called 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. Repeatedly composing the factorial amplifier with itself by means of the former construction 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, already establish hardness for h-exponential space for Petri nets with h + 13 counters.
-
Reachability in fixed dimension vector addition systems with states
International Conference on Concurrency Theory, 2020Co-Authors: Wojciech Czerwinski, Jérôme Leroux, Slawomir Lasota, Ranko Lazic, Filip MazowieckiAbstract:The Reachability Problem is a central decision Problem in verification of vector addition systems with states (VASS). 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 obtain three main results for VASS of fixed dimension. 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 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 ones. 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 runs. The smallest dimension for which this was previously known is 14.
-
the Reachability Problem for petri nets is not elementary
Symposium on the Theory of Computing, 2019Co-Authors: Wojciech Czerwinski, Jérôme Leroux, Slawomir Lasota, Ranko Lazic, Filip MazowieckiAbstract: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.
-
the Reachability Problem for petri nets is not elementary extended abstract
2018Co-Authors: Wojciech Czerwinski, Jérôme Leroux, Slawomir Lasota, Ranko Lazic, Filip MazowieckiAbstract: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.
-
Reachability Problem for weak multi pushdown automata
Logical Methods in Computer Science, 2013Co-Authors: Wojciech Czerwinski, Piotr Hofman, Slawomir LasotaAbstract:This paper is about Reachability analysis in a restricted subclass of multi-pushdown automata. We assume that the control states of an automaton are partially ordered, and all transitions of an automaton go downwards with respect to the order. We prove decidability of the Reachability Problem, and computability of the backward Reachability set. As the main contribution, we identify relevant subclasses where the Reachability Problem becomes NP-complete. This matches the complexity of the same Problem for communication-free vector addition systems, a special case of stateless multi-pushdown automata.
Sukanta Das - One of the best experts on this subject based on the ideXlab platform.
-
Reachability Problem in non uniform cellular automata
Information Sciences, 2021Co-Authors: Sumit Adak, Sukanya Mukherjee, Sukanta DasAbstract:Abstract This paper deals with the CREP (Configuration Reachability Problem) for non-uniform cellular automata (CAs). The cells of non-uniform CAs, we have considered here, can use different Wolfram’s rules to generate their next states. We report an algorithm which decides whether or not a configuration of a given (non-uniform) cellular automaton is reachable from another configuration. We develop a characterization tool, named Reachability tree, is used to develop theories and the decision algorithm for the CREP. Though the worst case complexity of the algorithm is exponential in time and space, but the average performance is very good.
-
Reachability Problem in non uniform cellular automata
arXiv: Computational Complexity, 2019Co-Authors: Sumit Adak, Sukanya Mukherjee, Sukanta DasAbstract:This paper deals with the CREP (Configuration Reachability Problem) for non-uniform cellular automata (CAs). The cells of non-uniform CAs, we have considered here, can use different Wolfram's rules to generate their next states. We report an algorithm which decides whether or not a configuration of a given (non-uniform) cellular automaton is reachable from another configuration. A characterization tool, named Reachability tree, is used to develop theories and the decision algorithm for the CREP. Though the worst case complexity of the algorithm is exponential in time and space, but the average performance is very good.
Ranko Lazić - One of the best experts on this subject based on the ideXlab platform.
-
The Reachability Problem for vector addition systems with a stack is not elementary
arXiv: Formal Languages and Automata Theory, 2013Co-Authors: Ranko LazićAbstract:By adapting the iterative yardstick construction of Stockmeyer, we show that the Reachability Problem for vector addition systems with a stack does not have elementary complexity. As a corollary, the same lower bound holds for the satisfiability Problem for a two-variable first-order logic on trees in which unbounded data may label only leaf nodes. Whether the two Problems are decidable remains an open question.
-
The Reachability Problem for branching vector addition systems requires doubly-exponential space
Information Processing Letters, 2010Co-Authors: Ranko LazićAbstract:Branching vector addition systems are an extension of vector addition systems where new reachable vectors may be obtained by summing two reachable vectors and adding an integral vector from a fixed finite set. The Reachability Problem for them is shown hard for doubly-exponential space. For an alternative extension of vector addition systems, where reachable vectors may be combined by subtraction, most decision Problems of interest are shown undecidable.
