--- res: bibo_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.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Dejan foaf_name: Nickovic, Dejan foaf_surname: Nickovic foaf_workInfoHomepage: http://www.librecat.org/personId=41BCEE5C-F248-11E8-B48F-1D18A9856A87 - foaf_Person: foaf_givenName: Nir foaf_name: Piterman, Nir foaf_surname: Piterman bibo_doi: 10.1007/978-3-642-15297-9_13 bibo_volume: 6246 dct_date: 2010^xs_gYear dct_language: eng dct_publisher: Springer@ dct_title: From MTL to deterministic timed automata@ ...