Reachability problem
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.