From Mtl to Deterministic Timed Automata

Abstract. In this paper we propose a novel technique for constructing timed automata from properties expressed in the logic MTL, under bounded-variability assumptions. We handle full MTL and in particular do not impose bounds on the future temporal connectives. Our construction is based on separation of the continuous time monitoring of the input sequence and discrete predictions regarding the future. The separation of the continuous from the discrete allows us to further determinize our automata. This leads, for the first time, to a construction from full MTL to deterministic timed automata.

• Type: Journal
• Year: 2010
• Where: FORMATS
• Authors: Dejan Nickovic, Nir Piterman
• Keywords: Bounded-variability Assumptions, Formal Methods, FORMATS 2010, Future Temporal Connectives, Logic Mtl