zbMATH — the first resource for mathematics

On timed automata with input-determined guards. (English) Zbl 1109.68503
Lakhnech, Yassine (ed.) et al., Formal techniques, modelling and analysis of timed and fault-tolerant systems. Joint international conferences on formal modelling and analysis of timed systems, FORMATS 2004, and formal techniques in real-time and fault-tolerant systems, FTRTFT 2004, Grenoble, France, September 22–24, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23167-6/pbk). Lecture Notes in Computer Science 3253, 68-83 (2004).
Summary: 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. D’Souza, “A logical characterisation of event clock automata”, Int. J. Found. Comput. Sci. 14, No. 4, 625–639 (2003; Zbl 1101.68647)], 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 [T. A. Henzinger, J.-F. Raskin and P.-Y. Schobbens, “The regular real-time languages”, Lect. Notes Comput. Sci. 1443, 580–591 (1998)], 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 [R. Alur, T. Feder and T. A. Henzinger, “The benefits of relaxing punctuality”, J. ACM 43, No. 1, 116–146 (1996; Zbl 0882.68021)] is expressively complete with respect to an MSO corresponding to an appropriate set of input-determined operators.
For the entire collection see [Zbl 1061.68004].

68Q45 Formal languages and automata
03D05 Automata and formal grammars in connection with logical questions
Full Text: DOI