Résumé
This paper presents a complete axiomatization of fully
decidable propositional real-time linear temporal logics with
past: the Event Clock Logic (ECL) and the 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 that allows the translation
of MITL formulae into ECL formulae, the
two logics being equally expressive. Our proof is structured to yield a
similar axiomatization and procedure for
interesting fragments of this logic: the linear temporal logic of the
real numbers (LTR), the fragment with only past
clocks.
langue originale | Anglais |
---|---|
titre | CONCUR'98 |
Sous-titre | 9th International Conference on Concurrency Theory |
rédacteurs en chef | D Sangiorgi, R de |
Editeur | Springer Verlag |
Volume | 1466 |
Etat de la publication | Publié - 1998 |