Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2404.18584 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917652482490368 |
|---|---|
| author | Barbot, Benoît Busatto-Gaston, Damien Dima, Catalin Oualhadj, Youssouf |
| author_facet | Barbot, Benoît Busatto-Gaston, Damien Dima, Catalin Oualhadj, Youssouf |
| contents | We consider the synthesis problem on timed automata with Büchi objectives, where delay choices made by a controller are subjected to small perturbations. Usually, the controller needs to avoid punctual guards, such as testing the equality of a clock to a constant. In this work, we generalize to a robustness setting that allows for punctual transitions in the automaton to be taken by controller with no perturbation. In order to characterize cycles that resist perturbations in our setting, we introduce a new structural requirement on the reachability relation along an accepting cycle of the automaton. This property is formulated on the region abstraction, and generalizes the existing characterization of winning cycles in the absence of punctual guards. We show that the problem remains within PSPACE despite the presence of punctual guards. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_18584 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Controller Synthesis in Timed Büchi Automata: Robustness and Punctual Guards Barbot, Benoît Busatto-Gaston, Damien Dima, Catalin Oualhadj, Youssouf Computer Science and Game Theory We consider the synthesis problem on timed automata with Büchi objectives, where delay choices made by a controller are subjected to small perturbations. Usually, the controller needs to avoid punctual guards, such as testing the equality of a clock to a constant. In this work, we generalize to a robustness setting that allows for punctual transitions in the automaton to be taken by controller with no perturbation. In order to characterize cycles that resist perturbations in our setting, we introduce a new structural requirement on the reachability relation along an accepting cycle of the automaton. This property is formulated on the region abstraction, and generalizes the existing characterization of winning cycles in the absence of punctual guards. We show that the problem remains within PSPACE despite the presence of punctual guards. |
| title | Controller Synthesis in Timed Büchi Automata: Robustness and Punctual Guards |
| topic | Computer Science and Game Theory |
| url | https://arxiv.org/abs/2404.18584 |