Real Time Temporal Logic: Past, Present, Future

This paper attempts to improve our understanding of timed languages and their relation to timed automata. We start by giving a constructive proof of the folk theorem stating that timed languages specified by the past fragment of MITL, can be accepted by deterministic timed automata. On the other hand we provide a proof that certain languages expressed in the future fragment of MITL are not deterministic,4 and analyze the reason for this asymmetry.

• Type: Conference
• Year: 2005
• Where: FORMATS
• Authors: Oded Maler, Dejan Nickovic, Amir Pnueli
• Keywords: Constructive Proof, Deterministic Timed Automata, FORMATS 2005, Timed Languages