Efficient on-the-fly Algorithm for Checking Alternating Timed Simulation

Abstract In this paper we focus on property-preserving preorders between timed game automata and their application to control of partially observable systems. We define timed weak alternating simulation as a preorder between timed game automata, which preserves controllability. We define the rules of building a symbolic turn-based two-player game such that the existence of a winning strategy is equivalent to the simulation being satisfied. We also propose an on-the-fly algorithm for solving this game. This simulation checking method can be applied to the case of non-alternating or strong simulations as well. We illustrate our algorithm by a case study and report on results.

• Type: Conference
• Year: 2009
• Where: FORMATS
• Authors: Peter Bulychev, Thomas Chatain, Alexandre David, Kim Guldstrand Larsen
• Keywords: Formal Methods, FORMATS 2009, Timed Game Automata, Turn-based Two-player Game, Weak Alternating Simulation