Reachability problem

Last updated
The reachability problem consists of attaining a final situation from an initial situation. Probleme accessibilite.png
The reachability problem consists of attaining a final situation from an initial situation.

Reachability is a fundamental problem that appears in several different contexts: finite- and infinite-state concurrent systems, computational models like 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. [1]

Contents

In general the reachability problem can be formulated as follows: Given a computational (potentially infinite state) 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.

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.

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.

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. [2]

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. [3] Since 1976, it is known that this problem is EXPSPACE-hard. [4] There are results on how much to implement this problem in practice. [5] In 2018, the problem was shown to be a nonelementary problem. [6] In 2022 it was shown to be complete for Ackermann function time complexity. [7] [8]

Vector addition systems

In 2022 reachability in vector addition systems was shown to be Ackermann-complete and therefore a nonelementary problem. [9] [8]

Open problems

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.

Related Research Articles

<span class="mw-page-title-main">Search algorithm</span> Any algorithm which solves the search problem

In computer science, a search algorithm is an algorithm designed to solve a search problem. Search algorithms work to retrieve information stored within particular data structure, or calculated in the search space of a problem domain, with either discrete or continuous values.

In computational complexity theory, EXPSPACE is the set of all decision problems solvable by a deterministic Turing machine in exponential space, i.e., in space, where is a polynomial function of . Some authors restrict to be a linear function, but most authors instead call the resulting class ESPACE. If we use a nondeterministic machine instead, we get the class NEXPSPACE, which is equal to EXPSPACE by Savitch's theorem.

Computer science is the study of the theoretical foundations of information and computation and their implementation and application in computer systems. One well known subject classification system for computer science is the ACM Computing Classification System devised by the Association for Computing Machinery.

<span class="mw-page-title-main">Petri net</span> One of several mathematical modeling systems for the description of distributed systems

A Petri net, also known as a place/transition (PT) net, is one of several mathematical modeling languages for the description of distributed systems. It is a class of discrete event dynamic system. A Petri net is a directed bipartite graph that has two types of elements: places and transitions. Place elements are depicted as white circles and transition elements are depicted as rectangles. A place can contain any number of tokens, depicted as black circles. A transition is enabled if all places connected to it as inputs contain at least one token. Some sources state that Petri nets were invented in August 1939 by Carl Adam Petri—at the age of 13—for the purpose of describing chemical processes.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification is a key incentive for formal specification of systems, and is at the core of formal methods. It represents an important dimension of analysis and verification in electronic design automation and is one approach to software verification. The use of formal verification enables the highest Evaluation Assurance Level (EAL7) in the framework of common criteria for computer security certification.

<span class="mw-page-title-main">Model checking</span> Computer science field

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.

A hybrid system is a dynamical system that exhibits both continuous and discrete dynamic behavior – a system that can both flow and jump. Often, the term "hybrid dynamical system" is used, to distinguish over hybrid systems such as those that combine neural nets and fuzzy logic, or electrical and mechanical drivelines. A hybrid system has the benefit of encompassing a larger class of systems within its structure, allowing for more flexibility in modeling dynamic phenomena.

<span class="mw-page-title-main">Concurrency (computer science)</span> Ability to execute a task in a non-serial manner

In computer science, concurrency is the ability of different parts or units of a program, algorithm, or problem to be executed out-of-order or in partial order, without affecting the outcome. This allows for parallel execution of the concurrent units, which can significantly improve overall speed of the execution in multi-processor and multi-core systems. In more technical terms, concurrency refers to the decomposability of a program, algorithm, or problem into order-independent or partially-ordered components or units of computation.

In computational complexity theory, a nonelementary problem is a problem that is not a member of the class ELEMENTARY. As a class it is sometimes denoted as NONELEMENTARY.

Dualistic Petri nets (dPNs) are a process-class variant of Petri nets. Like Petri nets in general and many related formalisms and notations, they are used to describe and analyze process architecture.

Business process discovery (BPD) related to business process management and process mining is a set of techniques that manually or automatically construct a representation of an organisations' current business processes and their major process variations. These techniques use data recorded in the existing organisational methods of work, documentations, and technology systems that run business processes within an organisation. The type of data required for process discovery is called an event log. Any record of data that contains the case id, activity name, and timestamp. Such a record qualifies for an event log and can be used to discover the underlying process model. The event log can contain additional information related to the process, such as the resources executing the activity, the type or nature of the events, or any other relevant details. Process discovery aims to obtain a process model that describes the event log as closely as possible. The process model acts as a graphical representation of the process. The event logs used for discovery could contain noise, irregular information, and inconsistent/incorrect timestamps. Process discovery is challenging due to such noisy event logs and because the event log contains only a part of the actual process hidden behind the system. The discovery algorithms should solely depend on a small percentage of data provided by the event logs to develop the closest possible model to the actual behaviour.

In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's theorem, which provides algorithms for evaluating monadic second-order formulas over graphs of bounded treewidth. It is also of fundamental importance in automata theory, where the Büchi–Elgot–Trakhtenbrot theorem gives a logical characterization of the regular languages.

<span class="mw-page-title-main">Construction and Analysis of Distributed Processes</span>

CADP is a toolbox for the design of communication protocols and distributed systems. CADP is developed by the CONVECS team at INRIA Rhone-Alpes and connected to various complementary tools. CADP is maintained, regularly improved, and used in many industrial projects.

Stochastic Petri nets are a form of Petri net where the transitions fire after a probabilistic delay determined by a random variable.

<span class="mw-page-title-main">Vector addition system</span> Mathematical modeling language

A vector addition system (VAS) is one of several mathematical modeling languages for the description of distributed systems. Vector addition systems were introduced by Richard M. Karp and Raymond E. Miller in 1969, and generalized to vector addition systems with states (VASS) by John E. Hopcroft and Jean-Jacques Pansiot in 1979. Both VAS and VASS are equivalent in many ways to Petri nets introduced earlier by Carl Adam Petri.

In computer science, especially model checking and abstract interpretation, widening refers to at least two different techniques in the analysis of abstract transition systems where infinite progressions of abstract states are replaced by a least fixed point. The use of the term in model checking is closely related to acceleration techniques, some authors reserving acceleration for exact computations.

This glossary of artificial intelligence is a list of definitions of terms and concepts relevant to the study of artificial intelligence, its sub-disciplines, and related fields. Related glossaries include Glossary of computer science, Glossary of robotics, and Glossary of machine vision.

Signal Transition Graphs (STGs) are typically used in electronic engineering and computer engineering to describe dynamic behaviour of asynchronous circuits, for the purposes of their analysis or synthesis.

Counterexample-guided abstraction refinement (CEGAR) is a technique for symbolic model checking. It is also applied in modal logic tableau calculi algorithms to optimise their efficiency.

References

  1. ↑ 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
  2. ↑ Reingold, Omer (3 May 2008). "Undirected Connectivity in Log-Space". omereingold.files.wordpress.com. Retrieved 9 December 2021.
  3. ↑ Mayr, Ernst W. (1981-05-11). "An algorithm for the general Petri net reachability problem". Proceedings of the thirteenth annual ACM symposium on Theory of computing - STOC '81. New York, NY, USA: Association for Computing Machinery. pp. 238–246. doi:10.1145/800076.802477. ISBN   978-1-4503-7392-0. S2CID   15409115.
  4. ↑ Lipton, R. (1976). The Reachability Problem Requires Exponential Space. Technical Report 62. Department of Computer Science, Yale University.
  5. ↑ Küngas, Peep (2005). "Petri Net Reachability Checking is Polynomial with Optimal Abstraction Hierarchies". In Zucker, Jean-Daniel; Saitta, Lorenza (eds.). Abstraction, Reformulation and Approximation. Lecture Notes in Computer Science. Vol. 3607. Berlin, Heidelberg: Springer. pp. 149–164. doi:10.1007/11527862_11. ISBN   978-3-540-31882-8.
  6. ↑ Czerwinski, Wojciech; Lasota, Slawomir; Lazic, Ranko; Leroux, Jerome; Mazowiecki, Filip (2019-04-11). "The Reachability Problem for Petri Nets is Not Elementary". arXiv: 1809.07115 [cs.FL].
  7. ↑ Leroux, Jerome (February 2022). "The Reachability Problem for Petri Nets is Not Primitive Recursive". IEEE Xplore. IEEE: 1241–1252. arXiv: 2104.12695 . doi:10.1109/FOCS52979.2021.00121. ISBN   978-1-6654-2055-6.
  8. 1 2 Brubaker, Ben (4 December 2023). "An Easy-Sounding Problem Yields Numbers Too Big for Our Universe". Quanta Magazine .
  9. ↑ Czerwiński, Wojciech; Orlikowski, Łukasz (2021). Reachability in Vector Addition Systems is Ackermann-complete. 2021 IEEE 62nd Annual Symposium on Foundations of Computer Science (FOCS). arXiv: 2104.13866 .
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.