Whereas formal verification of timed systems has become a very active field of research, the idealised mathematical semantics of timed automata cannot be faithfully implemented. Several works have thus focused on a modified semantics of timed automata which ensures implementability, and robust model-checking algorithms for safety, and later LTL properties have been designed. Recently, a new approach has been proposed, which reduces (standard) model-checking of timed automata to other verification problems on channel machines. Thanks to a new encoding of the modified semantics as a network of timed systems, we propose an original combination of both approaches, and prove that robust model-checking for coFlat-MTL, a large fragment of MTL, is EXPSPACE-Complete. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Bouyer, P., Markey, N., & Reynier, P. A. (2008). Robust analysis of timed automata via channel machines. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4962 LNCS, pp. 157–171). https://doi.org/10.1007/978-3-540-78499-9_12
Mendeley helps you to discover research relevant for your work.