An Automata-Theoretic Decision Procedure for Propositional Temporal Logic with Since and Until¹

Article type: Research Article

Authors: Ramakrishna, Y.S. | Moser, L.E. | Dillon, L.K. | Melliar-Smith, P.M. | Kutty, G.

Affiliations: Department of Electrical and Computer Engineering, Department of Computer Science, University of California, Santa Barbara

Note: [1] This work was partially supported by NSF grant CCR-9014382 with cooperation from DARPA.

Abstract: We present an automata-theoretic decision procedure for Since/Until Temporal Logic (SUTL), a linear-time propositional temporal logic with strong non-strict since and until operators. The logic, which is intended for specifying and reasoning about computer systems, employs neither next nor previous operators. Such operators obstruct the use of hierarchical abstraction and refinement and make reasoning about concurrency difficult. A proof of the soundness and completeness of the decision procedure is given, and its complexity is analyzed.

DOI: 10.3233/FI-1992-17307

Journal: Fundamenta Informaticae, vol. 17, no. 3, pp. 271-282, 1992