## Axioms for Real-Time Logics

*Jean-Francois Raskin, Pierre-Yves Schobbens, and
Thomas A. Henzinger*

This paper presents a complete axiomatization of two decidable propositional
real-time linear temporal logics: Event Clock Logic (ECL) and Metric Interval
Temporal Logic with past (MITL). The completeness proof consists of an
effective proof building procedure for ECL. From this result we obtain a
complete axiomatization of MITL by providing axioms translating MITL formulae
into ECL formulae, the two logics being equally expressive. Our proof is
structured to yield axiomatizations also for interesting fragments of these
logics, such as the linear temporal logic of the real numbers (LTR).

*Theoretical Computer Science* 274:151-182, 2002.
A preliminary version appeared in the
*Proceedings of the Ninth International Conference on Concurrency Theory*
(CONCUR),
Lecture Notes in Computer Science 1466,
Springer, 1998, pp. 219-236.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1998 Springer,
2002 Elsevier.