Axioms for real-time logics Journal Article


Author(s): Raskin, Jean-François; Schobbens, Pierre Y; Henzinger, Thomas A
Article Title: Axioms for real-time logics
Affiliation
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 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).
Journal Title: Theoretical Computer Science
Volume: 274
Issue 1-2
ISSN: 0304-3975
Publisher: Elsevier  
Date Published: 2002-03-01
Start Page: 151
End Page: 182
DOI: 10.1016/S0304-3975(00)00308-X
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work