---
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@
...