"Direct" Model Checking of Temporal Properties
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.