Model Checking Partially Ordered State Spaces

S. Hazelhurst and C.-J. H. Seger
Integrated Systems Design Laboratory
Department of Computer Science
University of British Columbia
Vancouver, B.C., Canada V6T 1Z4

21 July 1995

Abstract

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) [32] 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.

Keywords: symbolic trajectory evaluation, quaternary logic, model checking, temporal logic, bilattices

1 Introduction

Model-checking is a well-known automatic verification method that can determine whether a system has a certain set of properties. The nature of the model that represents the system and the type of logic used to express properties are choices open to the verifier. Different choices have

This research was supported by operating grant OGPO 109688 from the Natural Sciences and Engineering Research Council of Canada, a fellowship from the B.C. Advanced Systems Institute, and by equipment grants from Sun Microsystems Canada Ltd. and Digital Equipment of Canada Ltd. Support was also received from the Semiconductor Research Corporation. This paper has been submitted for review for publication, and so may be subject to copyright.