COMPLETENESS AND SOUNDNESS OF AXIOMATIZATIONS FOR TEMPORAL LOGICS WITHOUT NEXT
L.E. Moser, Peter Michael Melliar-Smith, G. Kutty, Y. S. Ramakrishna · Fundamenta Informaticae · 1994
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 obs