On timed automata with input-determined guards

TL;DR

This paper introduces a generalized class of timed automata with input-determined guards, establishing a robust logical framework and demonstrating the expressive completeness of MITL within this setting.

Contribution

It extends timed automata with input-determined guards and recursive operators, providing a logical characterization and showing MITL's expressive completeness in this context.

Findings

Timed automata with input-determined guards admit a monadic second order logic characterization.

Recursive operators enable a similar logical framework for generalized automata.

MITL is expressively complete with respect to an MSO logic in this setting.

Abstract

We consider a general notion of timed automata with input-determined guards and show that they admit a robust logical framework along the lines of [D 'Souza03], in terms of a monadic second order logic characterisation and an expressively complete timed temporal logic. We then generalize these automata using the notion of recursive operators introduced by Henzinger, Raskin, and Schobbens, and show that they admit a similar logical framework. These results hold in the ``pointwise'' semantics. We finally use this framework to show that the real-time logic MITL of Alur et al is expressively complete with respect to an MSO corresponding to an appropriate input-determined operator.