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.

• Type: Conference
• Year: 2009
• Where: FORMATS
• Authors: Laurent Doyen, Gilles Geeraerts, Jean-François Raskin, Julien Reichert
• Keywords: Formal Methods, FORMATS 2009, Real-time Formulas, Realizability Problem, Temporal Logic