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].