TY - JOUR
AB - We show how to construct temporal testers for the logic MITL, a prominent linear-time logic for real-time systems. A temporal tester is a transducer that inputs a signal holding the Boolean value of atomic propositions and outputs the truth value of a formula along time. Here we consider testers over continuous-time Boolean signals that use clock variables to enforce duration constraints, as in timed automata. We first rewrite the MITL formula into a “simple” formula using a limited set of temporal modalities. We then build testers for these specific modalities and show how to compose testers for simple formulae into complex ones. Temporal testers can be turned into acceptors, yielding a compositional translation from MITL to timed automata. This construction is much simpler than previously known and remains asymptotically optimal. It supports both past and future operators and can easily be extended.
AU - Ferrere, Thomas
AU - Maler, Oded
AU - Ničković, Dejan
AU - Pnueli, Amir
ID - 7109
IS - 3
JF - Journal of the ACM
SN - 0004-5411
TI - From real-time logic to timed automata
VL - 66
ER -