From MTL to deterministic timed automata Conference Paper

Author(s): Ničković, Dejan; Piterman, Nir
Title: From MTL to deterministic timed automata
Title Series: LNCS
Affiliation IST Austria
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 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.
Conference Title: FORMATS: Formal Modeling and Analysis of Timed Systems
Volume: 6246
Conference Dates: September 8-10, 2010
Conference Location: Klosterneuburg, Austria
Publisher: Springer  
Location: Berlin, Heidelberg
Date Published: 2010-09-08
Start Page: 152
End Page: 167
Sponsor: Part of this work was done while both authors were at Verimag, France. The first author is supported in part by the EU project COMBEST and the EU Network of Excellence ARTIST-DESIGN. The second author is supported by the grant UK EPSRC EP/E028985/1.
DOI: 10.1007/978-3-642-15297-9_13
Notes: We would like to thank Dana Fisman and Oded Maler for their insightful suggestions that helped us improve the clarity of the manuscript.
Open access: yes (repository)
IST Austria Authors
Related IST Austria Work