×

zbMATH — the first resource for mathematics

Robust controller synthesis in timed automata. (English) Zbl 1390.68416
D’Argenio, Pedro R. (ed.) et al., CONCUR 2013 – concurrency theory. 24th international conference, CONCUR 2013, Buenos Aires, Argentina, August 27–30, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-40183-1/pbk). Lecture Notes in Computer Science 8052, 546-560 (2013).
Summary: We consider 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.
For the entire collection see [Zbl 1269.68020].

MSC:
68Q45 Formal languages and automata
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q55 Semantics in the theory of computing
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
91A80 Applications of game theory
PDF BibTeX Cite
Full Text: DOI