Model Checking Real Time Systems

Overview

Real-time systems are often specified as timed automata [AD94]. A timed automaton consists of a set of locations (analogous to states in a finite automaton), and a set of edges between locations denoting transitions. Locations as well as transitions may be decorated with constraints on clocks. An example of a timed automaton appears below:

A state of a timed automaton comprises a location and an assignment of values to clock variables. Clearly, since clocks range over infinite domains, timed automata are infinite-state automata.

Real-time extensions to temporal logics, such as timed extensions of the modal mu-calculus [ACD93, HNSY94, SS95], are used to specify the properties of interest.

Traditional model-checking algorithms do not directly work in the case of real-time systems since the underlying state-space is infinite. The key then is to consider only finitely many regions of the state space. In [AD94] it is shown that when the constraints on clocks are restricted to those of the form X < Y + c where X and Y are clock variables and c is a constant, the state space of a timed automaton can be partitioned into finitely many stable regions-- sets of indistinguishable elements of the state space.

In [SS95], a local algorithm for model checking real-time systems was presented, where the finite discretization of the state space is done on demand, and only to the extent needed to prove or disprove the formula at hand. We are currently investigating how the essence of the above algorithm can be encoded as a tabled constraint logic program. In addition to a predicate that expresses when a region satisfies a timed temporal formula (analogous to the models/2 predicate in the XMC system), it appears that the real time model checking algorithm can be encoded using two other relations: refinesto/2, which relates a region with its partitions (obtained during finite discretization), and edge/3, which captures the transitions between regions.

Refinement creates new regions, and hence introduces new edges. The presence or absence of such edges may force further refinement. Therefore, refinesto and edge are mutually recursive predicates. Regions themselves are represented as a set of linear constraints, and operations on regions (such as splitting, which is needed when two points in a region can be distinguished) manipulate these constraints. Thus the resultant program is a tabled constraint logic program. Such programs can be evaluated in XSB using a meta interpreter, without modifying XSB's SLG-resolution engine. For better performance, however, we plan to directly augment the engine with a constraint-handling facility.

References

ACD93

R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. Information and Computation, 104(1):2-34, 1993.

AD94

R. Alur and D. Dill. The theory of timed automata. Theoretical Computer Science, 126(2), 1994.

HNSY94

T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2), 1994.

SS95

O. Sokolsky and S. A. Smolka. Local model checking for real-time systems. In Proceedings of the 7th International Conference on Computer-Aided Verification. American Mathematical Society, 1995.