"Direct" Model Checking of Temporal Properties

Mr. Ramesh Bharadwaj

Software Engineering Research Group
CRL, McMaster University,
Hamilton, Ontario, Canada L8S 4K1


Abstract

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.