LFCS Seminar: 7 November 2018 - Ranko Lazic Title: The Reachability Problem for Petri Nets is not Elementary Abstract: 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 cubic-Ackermannian of Leroux and Schmitz from LICS 2015. 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. Joint work with Wojciech Czerwinski, Slawomir Lasota, Jerome Leroux and Filip Mazowiecki. Paper available at: https://arxiv.org/abs/1809.07115. Nov 07 2018 14.00 - 15.00 LFCS Seminar: 7 November 2018 - Ranko Lazic Speaker: Ranko Lazic
LFCS Seminar: 7 November 2018 - Ranko Lazic Title: The Reachability Problem for Petri Nets is not Elementary Abstract: 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 cubic-Ackermannian of Leroux and Schmitz from LICS 2015. 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. Joint work with Wojciech Czerwinski, Slawomir Lasota, Jerome Leroux and Filip Mazowiecki. Paper available at: https://arxiv.org/abs/1809.07115. Nov 07 2018 14.00 - 15.00 LFCS Seminar: 7 November 2018 - Ranko Lazic Speaker: Ranko Lazic
