Reachability problem
{{Short description|Problem in math and computer science}}
File:Probleme accessibilite.png
Reachability is a fundamental problem which can be formulated as follows: Given a computational system with a set of allowed rules or transformations, decide whether a certain state of a system is reachable from a given initial state of the system.
It appears in several different contexts: finite- and infinite-state concurrent systems, cellular automata and Petri nets, program analysis, discrete and continuous systems, time critical systems, hybrid systems, rewriting systems, probabilistic and parametric systems, and open systems modelled as games.Giorgio Delzanno, Igor Potapov (Eds.): Reachability Problems - 5th International Workshop, RP 2011, Genoa, Italy, September 28–30, 2011. Proceedings. Lecture Notes in Computer Science 6945, Springer 2011, {{ISBN|978-3-642-24287-8}}
Variants of the reachability problem may result from additional constraints on the initial or final states, specific requirement for reachability paths as well as for iterative reachability or changing the questions into analysis of winning strategies in infinite games or unavoidability of some dynamics. John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman (Eds.): Introduction to Automata Theory, Languages, and Computation - 3rd International Workshop, RP 2011, Massachusetts, United States, 2006. {{ISBN|978-0321455369}}
Typically, for a fixed system description given in some form (reduction rules, systems of equations, logical formulas, etc.) a reachability problem consists of checking whether a given set of target states can be reached starting from a fixed set of initial states. The set of target states can be represented explicitly or via some implicit representation (e.g., a system of equations, a set of minimal elements with respect to some ordering on the states). Sophisticated quantitative and qualitative properties can often be reduced to basic reachability questions. Decidability and complexity boundaries, algorithmic solutions, and efficient heuristics are all important aspects to be considered in this context. Algorithmic solutions are often based on different combinations of exploration strategies, symbolic manipulations of sets of states, decomposition properties, or reduction to linear programming problems, and they often benefit from approximations, abstractions, accelerations and extrapolation heuristics. Ad hoc solutions as well as solutions based on general purpose constraint solvers and deduction engines are often combined in order to balance efficiency and flexibility. Christel Baier, Joost-Pieter Katoen (Eds.): Principles of Model Checking - MIT Press, Massachusetts, United States. June, 2008. {{ISBN|978-0262026499}}
Variants of reachability problems
= Finite explicit graph =
The reachability problem in an oriented graph described explicitly is NL-complete. Reingold, in a 2008 article, proved that the reachability problem for a non-oriented graph is in LOGSPACE.{{Cite web|last=Reingold|first=Omer|date=3 May 2008|title=Undirected Connectivity in Log-Space|url=https://omereingold.files.wordpress.com/2014/10/sl.pdf/index.html|archive-url=https://archive.wikiwix.com/cache/index2.php?url=https%3A%2F%2Fomereingold.files.wordpress.com%2F2014%2F10%2Fsl.pdf%2Findex.html|url-status=dead|archive-date=2007-06-15|access-date=9 December 2021|website=omereingold.files.wordpress.com}}
In model checking, reachability corresponds to a property of liveliness.
= Finite implicit graph =
In planning, more precisely in classical planning, one is interested in knowing if one can attain a state from an initial state from a description of actions. The description of actions defines a graph of implicit states, which is of exponential size in the size of the description.
In symbolic model checking, the model (the underlying graph) is described with the aid of a symbolic representation such as binary decision diagrams.
= Petri nets =
The reachability problem in a Petri net is decidable.{{Cite book|last=Mayr|first=Ernst W.|title=Proceedings of the thirteenth annual ACM symposium on Theory of computing - STOC '81 |chapter=An algorithm for the general Petri net reachability problem |date=1981-05-11|chapter-url=https://doi.org/10.1145/800076.802477|location=New York, NY, USA|publisher=Association for Computing Machinery|pages=238–246|doi=10.1145/800076.802477|isbn=978-1-4503-7392-0|s2cid=15409115}} Since 1976, it is known that this problem is EXPSPACE-hard.{{citation|mode=cs1|first=R.|last=Lipton|author-link=Richard Lipton|title=The Reachability Problem Requires Exponential Space|series=Technical Report 62|year=1976|publisher=Department of Computer Science, Yale University}} There are results on how much to implement this problem in practice.{{Cite book|last=Küngas|first=Peep|title=Abstraction, Reformulation and Approximation |chapter=Petri Net Reachability Checking is Polynomial with Optimal Abstraction Hierarchies |date=2005|editor-last=Zucker|editor-first=Jean-Daniel|editor2-last=Saitta|editor2-first=Lorenza|editor2-link=Lorenza Saitta|chapter-url=https://link.springer.com/chapter/10.1007/11527862_11|series=Lecture Notes in Computer Science|volume=3607|language=en|location=Berlin, Heidelberg|publisher=Springer|pages=149–164|doi=10.1007/11527862_11|isbn=978-3-540-31882-8}} In 2018, the problem was shown to be a nonelementary problem.{{cite arXiv|last1=Czerwinski|first1=Wojciech|last2=Lasota|first2=Slawomir|last3=Lazic|first3=Ranko|last4=Leroux|first4=Jerome|last5=Mazowiecki|first5=Filip|date=2019-04-11|title=The Reachability Problem for Petri Nets is Not Elementary|class=cs.FL|eprint=1809.07115}} In 2022 it was shown to be complete for Ackermann function time complexity.{{Cite book |last=Leroux |first=Jerome |chapter=The Reachability Problem for Petri Nets is Not Primitive Recursive |date=February 2022 |title=2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS) |chapter-url=https://ieeexplore.ieee.org/document/9719763 |publisher=IEEE |pages=1241–1252 |doi=10.1109/FOCS52979.2021.00121 |isbn=978-1-6654-2055-6|arxiv=2104.12695 }}{{Cite web |last=Brubaker |first=Ben |date=4 December 2023 |title=An Easy-Sounding Problem Yields Numbers Too Big for Our Universe |url=https://www.quantamagazine.org/an-easy-sounding-problem-yields-numbers-too-big-for-our-universe-20231204/ |website=Quanta Magazine}}
= Vector addition systems =
In 2022 reachability in vector addition systems was shown to be Ackermann-complete and therefore a nonelementary problem.{{cite conference |last1=Czerwiński |first1=Wojciech |last2=Orlikowski |first2=Łukasz |date=2021 |title=Reachability in Vector Addition Systems is Ackermann-complete |conference=2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS) |arxiv=2104.13866}}
Open problems
{{Empty section|date=April 2013}}
International Conference on Reachability Problems (RP)
The International Conference on Reachability Problems series, previously known as Workshop on Reachability Problems, is an annual academic conference which gathers together researchers from diverse disciplines and backgrounds interested in reachability problems that appear in algebraic structures, computational models, hybrid systems, infinite games, logic and verification. The workshop tries to fill the gap between results obtained in different fields but sharing common mathematical structure or conceptual difficulties.
References
{{Reflist}}