Axioms for real-time logics Conference Paper


Author(s): Raskin, Jean-François; Schobbens, Pierre Y; Henzinger, Thomas A
Title: Axioms for real-time logics
Title Series: LNCS
Affiliation
Abstract: 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 translating 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 these logics, such as the linear temporal logic of the real numbers (LTR).
Conference Title: CONCUR: Concurrency Theory
Volume: 1466
Conference Dates: September 8–11, 1998
Conference Location: Nice, France
ISBN: 978-3-95977-017-0
Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik  
Date Published: 1998-01-01
Start Page: 219
End Page: 236
DOI: 10.1007/BFb0055625
Notes: This work is supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the DARPA/NASA grant NAG2-1214, by the ARO MURI grant DAAH-04-96-1-0341, by the SRC contract 97-DC-324.041, the Belgian National Fund for Scientific Research (FNRS), the European Commission under WGs Aspire and Fireworks, the Portuguese FCT, and by Belgacom.
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work