TY - JOUR
T1 - Axioms for real-time logics
AU - Schobbens, P.-Y.
AU - Raskin, J.-F.
AU - Henzinger, T.A.
N1 - Copyright 2008 Elsevier B.V., All rights reserved.
PY - 2002/3/6
Y1 - 2002/3/6
N2 - 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 MetricIntervalTL 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 (TLR). © 2002 Published by Elsevier Science B.V.
AB - 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 MetricIntervalTL 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 (TLR). © 2002 Published by Elsevier Science B.V.
UR - http://www.scopus.com/inward/record.url?scp=0037028875&partnerID=8YFLogxK
U2 - 10.1016/S0304-3975(00)00308-X
DO - 10.1016/S0304-3975(00)00308-X
M3 - Article
VL - 274
SP - 151
EP - 182
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 1-2
ER -