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

EECS Department
University of California, Berkeley
Technical Report No. UCB/CSD-99-1076
November 1999

http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/CSD-99-1076.pdf

This paper presents a complete axiomatization of two decidable propositional real-time linear temporal logics: Event Clock Logic (EventClockTL) and Metric Interval Temporal Logic with past (MetricIntervalTL). The completeness proof consists of an effective proof building procedure for EventClockTL. From this result we obtain a complete axiomatization of MetricIntervalTL by providing axioms translating MITL formulae into EventClockTL 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).

BibTeX citation:

@techreport{Schobbens:CSD-99-1076,
    Author = {Schobbens, Pierre-Yves and Raskin, Jean-Francois and Henzinger, Thomas A. and Ferier, L.},
    Title = {Axioms for Real-Time Logics},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {1999},
    Month = {Nov},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/5712.html},
    Number = {UCB/CSD-99-1076},
    Abstract = {This paper presents a complete axiomatization of two decidable propositional real-time linear temporal logics: Event Clock Logic (EventClockTL) and Metric Interval Temporal Logic with past (MetricIntervalTL). The completeness proof consists of an effective proof building procedure for EventClockTL. From this result we obtain a complete axiomatization of MetricIntervalTL by providing axioms translating MITL formulae into EventClockTL 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).}
}

EndNote citation:

%0 Report
%A Schobbens, Pierre-Yves
%A Raskin, Jean-Francois
%A Henzinger, Thomas A.
%A Ferier, L.
%T Axioms for Real-Time Logics
%I EECS Department, University of California, Berkeley
%D 1999
%@ UCB/CSD-99-1076
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/1999/5712.html
%F Schobbens:CSD-99-1076