M.Phil Dissertation

On-the-fly Verification for Linear Time Temporal Logic

Deepak D'Souza

M.Phil Dissertation, submitted to BITS, Pilani (1997).


Verification of finite state systems using Linear Temporal Logic (LTL) is limited by the size of the state space which arises from both the program and formula automata. In [GPVW 95] Gerth, Peled, Vardi and Wolper suggest an algorithm to build the formula automaton in a space-efficient manner. The algorithm works ``on-the-fly'' and is claimed to build, in practice, smaller automata than the classical construction of Vardi, Wolper and Sistla. In this report we take a closer look at the GPVW algorithm and present it in a more transparent manner. We give an explicit definition of the formula automaton along with the proof of its soundness and completeness. We also give an algorithm based on this definition, which traverses the automaton on-the-fly.

Available as a gzipped dvi file (37 K) or gzipped postscript file (83 K).