Realizability of Real-Time Logics

13 years 9 months ago
Realizability of Real-Time Logics
Abstract. We study the realizability problem for specifications of reactive systems expressed in real-time linear temporal logics. The logics we consider are subsets of MITL (Metric Interval Temporal Logic), a logic for which the satisfiability and validity problems are decidable, a necessary condition for the realizability problem to be decidable. On the positive side, we show that the realizability of LTL extended with past real-time formulas is decidable in 2EXPTIME, with a matching lower bound. On the negative side, we show that a simple extension of this decidable fragment with future real-time formulas leads to undecidability. In particular, our results imply that the realizability problem is undecidable for ECL (Event Clock Logic), and therefore also for MITL.
Laurent Doyen, Gilles Geeraerts, Jean-Franç
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Authors Laurent Doyen, Gilles Geeraerts, Jean-François Raskin, Julien Reichert
Comments (0)