A clock-optimal hierarchical monitoring automaton construction for MITL

Raj Mohan, Deepak D'souza

In this paper we present an inductive monitoring automaton construction for MITL formulas. The construction is in the spirit of the one given by Maler et al. in FORMATS 2006, but handles the full fragment of MITL. Our construction is more efficient in the use of clocks for the timed modalities and uses one clock less than the constructions given by both Maler et al., and Alur et al. (J. ACM 1996). Further, our construction is shown to be clock-optimal, in that any inductive construction of a monitoring automaton must use at least as many clocks in each inductive step.