We propose an algorithm for the analysis of robustness of timed automata, that is, the correctness of a model in the presence of small drifts of the clocks. The algorithm is an extension of the region-based algorithm of Puri and uses the idea of stable zones as introduced by Daws and Kordy. Similarly to the assumptions made by Puri, we restrict our analysis to the class of timed automata with closed guards, progress cycles, and bounded clocks. We have implemented the algorithm and applied it to several benchmark specifications. The algorithm is a depth-first search based on on-the-fly reachability using zones. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Kordy, P., Langerak, R., Mauw, S., & Polderman, J. W. (2014). A symbolic algorithm for the analysis of robust timed automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8442 LNCS, pp. 351–366). Springer Verlag. https://doi.org/10.1007/978-3-319-06410-9_25
Mendeley helps you to discover research relevant for your work.