On-the-fly Verification

On-the-fly Verification for Product-LTL

D. D'Souza and P. Madhusudan

Proc. Seventh NSTCS, Madras. (1997)


Automatic Verification using temporal logic is limited by space considerations. In [GPVW 95] the authors give a space-efficient algorithm to generate the formula automaton for a given LTL formula. We extend this algorithm for the logic Product-LTL proposed in [T 95].

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