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.
Get full access to this article
View all access options for this article.