On Construction of Safety Signal Automata for $MITL[\:\mathcal{U},\:\mathcal{S}]$ Using Temporal Projections

Abstract

Construction of automata for Metric Temporal Logics has been an active but challenging area of research. We consider here the continuous time Metric temporal logic $\mathsf{MTL}[\:\mathcal{U}_I,\:\mathcal{S}_I]$ as well as corresponding signal automata. In previous works by Maler, Nickovic and Pnueli, the signal automaton synthesis has mainly addressed MTL under an assumption of bounded variability. In this paper, we propose a novel technique of “Temporal Projections” that allows easy synthesis of safety signal automata for continuous time $\mathsf{MITL}[\:\mathcal{U}_I,\:\mathcal{S}_I]$ over finite signals without assuming bounded variability. Using the same technique, we also give synthesis of safety signal automata for $\mathsf{MITL}[\:\mathcal{U}_I,\:\mathcal{S}_I]$ with bounded future operators over infinite signals. For finite signals, the Temporal Projections allow us to syntactically transform an MITL formula φ(Q) over a set of propositions Q to a pure past time MITL formula ψ(P,Q) with extended set of propositions (P,Q) which is language equivalent “modulo temporal projection”, i.e. $L(\phi) = L(\exists P. \boxdot \psi)$. A similar such transformation over infinite signals is also formulated for $\mathsf{MITL}[\:\mathcal{U}_I,\:\mathcal{S}_I]$ restricted to Bounded Future formlae where the Until operators use only bounded (i.e.non-infinite) intervals. It is straightforward to construct safety-signal-automaton for the transformed formula. We give complexity bounds for the resulting automaton. Our temporal projections are inspired by the use of projections by D’Souza et al for eliminating past in MTL.