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 , 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 set of input-determined operators.
Weitere Kapitel dieses Buchs durch Wischen aufrufen
- On Timed Automata with Input-Determined Guards
- Springer Berlin Heidelberg
Neuer Inhalt/© ITandMEDIA