Symbolic Model Checking with Past and Future Temporal Modalities: Fundamentals and Algorithms

Model checking is gaining importance in verifying the partial specifications of complex synchronous systems modelled by means of a finite state machine. In this paper, we present the principles and a tool for checking their properties in a temporal logic that allows both past and future oriented modalities. After a revision of the basic concepts of the finite state machine model, and of its representation using binary decision diagrams, we present several algorithms to traverse the set of states symbolically. We then extend CTL with past oriented modalities and give properties of this extended temporal logic(TL). We give algorithms to verify TL formulas by symbolic model checking. A prototype symbolic model checker for TL, taking as input synchronous circuits written in a VHDL subset, has been implemented.