M.Phil Dissertation

###
On-the-fly Verification for Linear Time Temporal Logic

Deepak D'Souza
* M.Phil Dissertation, submitted to BITS, Pilani (1997).
*

**Abstract**
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*).