On MITL and alternating timed automata

TL;DR

This paper introduces a new semantics for one clock alternating timed automata (OCATA) using interval clock valuations, enabling effective model-checking of MITL formulas against timed automata.

Contribution

It proposes a novel interval-based semantics for OCATA, bounding clock copies needed for recognizing MITL models, and presents a new translation algorithm from MITL to timed automata.

Findings

Bounded number of clock copies for OCATA recognizing MITL models

New algorithm for translating MITL formulas into timed automata

Foundations for developing new model checking algorithms for MITL

Abstract

One clock alternating timed automata OCATA have been recently introduced as natural extension of (one clock) timed automata to express the semantics of MTL (Ouaknine, Worrell 2005). We consider the application of OCATA to problem of model-checking MITL formulas (a syntactic fragment of MTL) against timed automata. We introduce a new semantics for OCATA where, intuitively, clock valuations are intervals instead of single real values. Thanks to this new semantics, we show that we can bound the number of clock copies that are necessary to allow an OCATA to recognise the models of an MITL formula. Equipped with this technique, we propose a new algorithm to translate an MITL formula into a timed automaton, and we sketch several ideas to define new model checking algorithms for MITL.