Model Checking Partially Ordered State Spaces

The state explosion problem is the fundamental limitation of verification through model checking. In many cases, representing the state space of a system as a lattice is an effective way of ameliorating this problem. The partial order of the state space lattice represents an information ordering. The paper shows why using a lattice structure is desirable, and why a quaternary temporal logic rather than a traditional binary temporal logic is suitable for describing properties in systems represented this way. The quaternary logic not only has necessary technical properties, it also expresses degrees of truth. This is useful to do when dealing with a state space with an information ordering defined on it, where in some states there may be insufficient or contradictory information available. The paper presents the syntax and semantics of a quaternary valued temporal logic. Symbolic trajectory evaluation (STE) has been used to model check partially ordered state spaces with some success. The limitation of STE so far has been that the temporal logic used (a two-valued logic) has been restricted, whereas a more expressive temporal logic is often useful. This paper generalises the theory of symbolic trajectory evaluation to the quaternary temporal logic, which potentially provides an effective method of model checking an important class of formulas of the logic. Some practical model checking algorithms are briefly described and their use illustrated. This shows that not only can STE be used to check more expressive logics in principle, but that it is feasible to do so.