Combining Symbolic Representations for Solving Timed Games

We present a general approach to combine symbolic state space representations for the discrete and continuous parts in the synthesis of winning strategies for timed reachability games. The combination on abstraction refinement where discrete symbolic techniques are used to produce a sequence of abstract timed game automata. Afrefinement step, the resulting abstraction is used for computing an under- and an over-approximation of the timed winning states. The key idea is to identify large relevant and irrelevant parts of the precise weakest winning strategy already on coarse, and therefore simple, abstractions. If neither the existence nor nonexistence of a winning strategy can be established in the approximations, we use them to guide the refinement process. Based on a prototype that combines binary decision diagrams [7,9] and difference bound matrices [5], we experimentally evaluate the technique on standard benchmarks from timed controller synthesis. The results clearly demonstrate th...

• Type: Journal
• Year: 2010
• Where: FORMATS
• Authors: Rüdiger Ehlers, Robert Mattmüller, Hans-Jörg Peter
• Keywords: Abstract Timed Game, Formal Methods, FORMATS 2010, Timed Winning States, Winning Strategy