From MTL to deterministic timed automata

Ničković, Dejan and Piterman, Nir (2010) From MTL to deterministic timed automata. In: FORMATS: Formal Modeling and Analysis of Timed Systems, September 8-10, 2010, Klosterneuburg, Austria.

[img] Text
From_MTL_to_deterministic_timed_automata.pdf - Accepted Version
Download (243Kb)
Official URL:


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 include all future operators. 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 determinize our automata in an exponential construction that does not increase the number of clocks. This leads to a doubly exponential construction from mtl to deterministic timed automata, compared with triply exponential using existing approaches. We offer an alternative to the existing approach to linear real-time model checking, which has never been implemented. It further offers a unified framework for model checking, runtime monitoring, and synthesis, in an approach that can reuse tools, implementations, and insights from the discrete setting.

Item Type: Conference or Workshop Item (Paper)
Subjects: 000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems > 004 Data processing & computer science
SWORD Depositor: Sword Import User
Depositing User: Sword Import User
Date Deposited: 03 Oct 2012 09:03
Last Modified: 19 Sep 2017 15:36

Actions (login required)

View Item View Item