Bounding Clock Copies in One-Clock Alternating Timed Tree Automata

  • Timed automata provide a framework for verifying real-time systems: by abstracting continuous time into a finite system, the emptiness problem becomes decidable. Alternating timed automata (ATA) extend the expressivity of timed automata, but are generally undecidable due to an unbounded number of clock copies they need to maintain. While one-clock ATA restore decidability by bounding the number of simultaneous clock copies, they remain restricted to timed words as input. The goal of this thesis is to extend the bounding mechanism to the tree setting, enabling reasoning about game strategies instead of single system paths. This allows us to identify a decidable fragment of one-clock alternatingtimed tree automata, and to develop a model-checking algorithm for the formal verification of strategies over timed trees.