Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Controller Synthesis in Timed Büchi Automata: Robustness and Punctual Guards

Benoît Barbot, Damien Busatto-Gaston, Catalin Dima, Youssouf Oualhadj

TL;DR

The paper advances robust controller synthesis for timed Büchi automata by allowing punctual guards to be used without perturbation while non-punctual transitions undergo a small timing perturbation, and it formalizes a two-player game $\mathcal{G}_{\delta}(\mathcal{A})$ to study this setting. It introduces a region- and corners-based framework, including orbit and folded orbit graphs, to characterize perturbation-robust cycles via a cluster-graph condition, and develops slicing techniques to partition regions into reachability-equivalent classes. A central result shows that the robust Büchi-synthesis problem is $PSPACE$-complete, and the algorithm relies on on-the-fly construction of robust lassos whose folded orbit graphs form cluster graphs. This work extends prior robustness analyses by integrating punctual guards and providing a symbolic, DBM-based approach that preserves tractability and enables precise analysis of timed-automata with mixed reliable and perturbable transitions.

Abstract

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.

Controller Synthesis in Timed Büchi Automata: Robustness and Punctual Guards

TL;DR

The paper advances robust controller synthesis for timed Büchi automata by allowing punctual guards to be used without perturbation while non-punctual transitions undergo a small timing perturbation, and it formalizes a two-player game to study this setting. It introduces a region- and corners-based framework, including orbit and folded orbit graphs, to characterize perturbation-robust cycles via a cluster-graph condition, and develops slicing techniques to partition regions into reachability-equivalent classes. A central result shows that the robust Büchi-synthesis problem is -complete, and the algorithm relies on on-the-fly construction of robust lassos whose folded orbit graphs form cluster graphs. This work extends prior robustness analyses by integrating punctual guards and providing a symbolic, DBM-based approach that preserves tractability and enables precise analysis of timed-automata with mixed reliable and perturbable transitions.

Abstract

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.
Paper Structure (15 sections, 4 theorems, 2 equations, 4 figures)

This paper contains 15 sections, 4 theorems, 2 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Partial robustness semantics
  3. Timed automata
  4. Game semantics
  5. Preliminaries
  6. The region abstraction
  7. Corners
  8. Orbit graphs
  9. Folded orbit graphs
  10. Graph terminology
  11. Robustness of a finite path
  12. Zones and Difference Bound Matrices
  13. Controllable predecessors
  14. Robustness of an infinite path
  15. Slicing regions

Key Result

proposition thmcounterproposition

Let $\pi$ be a well-formed region path from $(\ell,r)$ to $(\ell',r')$. Then, there exists $\delta>0$ so that $\mathsf{CPre}_\pi^\delta(r')\neq\emptyset$ if and only if $\pi$ is robust.

Figures (4)

  • Figure 1: A timed automaton, and some of its reachable regions.
  • Figure 2: The orbit graph of a region cycle in the automaton of Fig. \ref{['fig:taEx']}, and its folding.
  • Figure 3: A timed automaton with a robustly iterable cycle $\ell_0\ell_1\ell_2$ is on the left. The corresponding orbit graph is displayed in the center and its folded orbit graph is depicted on the right. The folded orbit graph is a cluster graph with two complete SCCs.
  • Figure 4: Cluster corner partitions and some slices of a region of dimension 2.

Theorems & Definitions (17)

  • remark thmcounterremark
  • remark thmcounterremark
  • definition thmcounterdefinition
  • remark thmcounterremark
  • definition thmcounterdefinition
  • definition thmcounterdefinition: bengtsson2003timed
  • definition thmcounterdefinition: Sankur13
  • proposition thmcounterproposition
  • definition thmcounterdefinition
  • lemma thmcountertheorem
  • ...and 7 more