COMPLETENESS AND SOUNDNESS OF AXIOMATIZATIONS FOR TEMPORAL LOGICS WITHOUT NEXT

Article type: Research Article

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

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

Abstract: We present axiomatizations for Until Temporal Logic (UTL) and for Since/Until Temporal Logic (SUTL). These logics are intended for use in specifying and reasoning about concurrent systems. They employ neither a next nor a previous operator, which obstruct the use of hierarchical abstraction and refinement, and make reasoning about concurrency difficult. We also provide a procedure for translating SUTL formulas into UTL formulas, and demonstrate that the axiomatizations are sound and complete with respect to the class of ω-sequences. We show, however, that the axiomatization of UTL admits models that the axiomatization of SUTL does not, thereby demonstrating that the logics are not equivalent.

DOI: 10.3233/FI-1994-2141

Journal: Fundamenta Informaticae, vol. 21, no. 4, pp. 257-305, 1994