Whereas formal verification of timed systems has become a very active field of research, the idealized mathematical semantics of timed automata cannot be faithfully implemented. Recently, several works have studied a parametric semantics of timed automata related to implementability: if the specification is met for some positive value of the parameter, then there exists a correct implementation. In addition, the value of the parameter gives lower bounds on sufficient resources for the implementation. In this work, we present a symbolic algorithm for the computation of the parametric reachability set under this semantics for flat timed automata. As a consequence, we can compute the largest value of the parameter for a timed automaton to be safe. © 2011 Springer-Verlag.
CITATION STYLE
Jaubert, R., & Reynier, P. A. (2011). Quantitative robustness analysis of flat timed automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6604 LNCS, pp. 229–244). Springer Verlag. https://doi.org/10.1007/978-3-642-19805-2_16
Mendeley helps you to discover research relevant for your work.