"Direct" Model Checking of Temporal Properties

(Version 2)

Ramesh Bharadwaj

Dr. Jeffery Zucker

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 modeling 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 automaton and the negated property automaton. To check properties expressed in Linear-time Temporal Logic (LTL) involves a construction which produces an automaton with states exponential in the size of the formula. 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. We do this by adapting well-known LTL proof rules to model checking. In our approach, there is no need to construct equivalent Buchi automata. Another advantage is our ability to handle fairness in a straight forward way. Our method combines a model checking and theorem proving in a unified framework, and may be used for practical verifications.