Ocan Sankur, Patricia Bouyer, Nicolas Markey and Pierre-Alain Reynier
24th International Conference on Concurrency Theory (CONCUR), Buenos Aires, Argentina, 2013, pages 546-560.
Used by the Cassting project
Timed automata are a convenient model for representing real-time systems. However, their semantics is a mathematical idealization of physical systems, and the properties that hold true in a model might fail to hold in its implementations. Taking timing imprecisions into account is an important step towards a broader usability of timed automata in verification and synthesis. This paper considers the fundamental problem of Büchi acceptance in timed automata in a robust setting. The problem is formalised in terms of controller synthesis: timed automata are equipped with a parametrised game-based semantics that models the possible perturbations of the decisions taken by the controller. We characterise timed automata that are robustly controllable for some parameter, with a simple graph theoretic condition, by showing the equivalence with the existence of an aperiodic lasso that satisfies the winning condition (aperiodicity was defined and used earlier in different contexts to characterise convergence phenomena in timed automata). We then show decidability and PSPACE-completeness of our problem.