Robust Reachability in Timed Automata: A Game-Based Approach - Université de Rennes Accéder directement au contenu
Article Dans Une Revue Theoretical Computer Science Année : 2015

Robust Reachability in Timed Automata: A Game-Based Approach

Résumé

Reachability checking is one of the most basic problems in verification. By solving this problem in a game, one can synthesize a strategy that dictates the actions to be performed for ensuring that the target location is reached. In this work, we are interested in synthesizing "robust" strategies for ensuring reachability of a location in timed automata. By robust, we mean that it must still ensure reachability even when the delays are perturbed by the environment. We model this perturbed semantics as a game between the controller and its environment, and solve the parameterized robust reachability problem: we show that the existence of an upper bound on the perturbations under which there is a strategy reaching a target location is EXPTIME-complete. We also extend our algorithm, with the same complexity, to turn-based timed games, where the successor state is entirely determined by the environment in some locations.
Fichier principal
Vignette du fichier
BMS-tcs14.pdf (687.27 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01105077 , version 1 (19-01-2015)

Identifiants

Citer

Patricia Bouyer, Nicolas Markey, Ocan Sankur. Robust Reachability in Timed Automata: A Game-Based Approach. Theoretical Computer Science, 2015, 563, pp.43-74. ⟨10.1016/j.tcs.2014.08.014⟩. ⟨hal-01105077⟩
297 Consultations
237 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More