Sciweavers

88
Voted
FOSSACS
2008
Springer

Robust Analysis of Timed Automata via Channel Machines

14 years 10 months ago
Robust Analysis of Timed Automata via Channel Machines
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.
Patricia Bouyer, Nicolas Markey, Pierre-Alain Reyn
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Where FOSSACS
Authors Patricia Bouyer, Nicolas Markey, Pierre-Alain Reynier
Comments (0)