Axioms for Real-Time Logics

This paper presents a complete axiomatization of two decidable propositional realtime linear temporal logics: Event Clock Logic (EventClockTL) and Metric Interval Temporal Logic with past (MetricIntervalTL). The completeness proof consists of an e ective 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). Key words: Temporal logic, real-time, axiomatization, completeness.

• Type: Conference
• Year: 1998
• Where: CONCUR
• Authors: Jean-François Raskin, Pierre-Yves Schobbens, Thomas A. Henzinger
• Keywords: Complete Axiomatization, CONCUR 1998, Distributed And Parallel Computing, Linear Temporal Logic, Temporal Logic