"Direct" Model Checking of Temporal Properties
Mr. Ramesh Bharadwaj
Software Engineering Research Group
CRL, McMaster University,
Hamilton, Ontario, Canada L8S 4K1
In this paper, we address the problem of model checking temporal properties of finite-state programs.
This problem is usually solved by modelling the program as well as the negation of the desired temporal
property as automata on infinite words (Buchi automata) and checking for emptiness of the automaton
resulting from the synchronous product of the program automation and the negated property automaton.
To check properties expressed in Linear-time Temporal Logic (LTL) [MP91b] involves a construction
which produces an automaton with states exponential in the size of the formula [Wol89]. This poses a
problem especially when model checking under fairness assumptions - the formulae tend to be very long
in these cases. In this paper, we present a method to directly check properties expressed in LTL for
programs written in UNITY-like notation. In our approach, there is no need to construct equivalent Buchi
automata. Another advantage is our ability to handle fairness in a straightforward way. Our method
combines a model checking and theorem proving in a unified framework, and is computable with on-the-
fly techniques such as bit-state hashing.