On Construction of Safety Signal Automata for Using Temporal Projections

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

.