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.