Algorithms.

Finite-state systems turn out to be amenable to automatic verification, since their observable behavior can be finitely represented. These systems arise in practice in areas such as hardware design and communication protocols; this fact has spurred interest in the development of verification algorithms for temporal logic and relation-based specifications.

The task of determining automatically whether a system satisfies a temporal formula is usually referred to as model checking. One may identify two basic approaches to model checking. The first, which grew out of the branching-time logic community, relies on an analysis of the structure of the formula to determine which system states satisfy the formula. The second, which arose from the linear-time community, is automaton-based; one constructs an automaton from the negation of the formula in question and then determines whether or not the intersection of this automaton and the automaton representing the system is empty (if so, the system is correct). The two approaches turn out to be related, and indeed automaton-based approaches have been developed for branching-time logics and ``structure-based'' ones have been devised for linear-time logics. The time complexities of the best algorithms in each case are proportional to the product of the number of system states and the size of the formula (branching-time) or an exponential of the size of the formula (linear-time).

Algorithms have also been devised for calculating whether systems are related by semantic relations. Traditional approaches for calculating equivalences combine partition-based algorithms for bisimulation equivalence with automaton transformations that modify the automata corresponding to the systems being checked. Methods for computing preorders follow a similar scheme, with the ``base'' relation being a variant of the simulation preorder.

The key impediment to the practical application of these algorithms is the state-explosion problem. In general, the number of states a system has will be exponential in the number of concurrent processes; as this number grows, the possibility of enumerating all possible system states rapidly becomes infeasible. Much of the recent work on model and relation checking has been devoted to techniques for ameliorating the effects of state explosion. Some of the techniques that have been developed include:

Symbolic representations

of state spaces via e.g. binary decision diagrams, as a means of encoding system states more compactly;

On-the-fly algorithms

rely on a demand-driven generation of states to avoid the construction of irrelevant system configurations;

Redundancy elimination

strives to reduce the number of redundant system states that algorithms analyze, and includes partial-order techniques, semantic minimization, and symmetry-based approaches.

Finally, researchers have also developed techniques for handling certain kinds of infinite-state systems, including context-free processes and those based on dense real-time.