UPPAAL Tiga -- Controller Synthesis for Real-Time Systems

Kim G. Larsen
Aalborg University, Denmark
Friday, 8 December, 2006 (All day)

UPPAAL Tiga is a recent branch of the real-time verification tool UPPAAL allowing control programs to be synthesized from timed game automata models with respect to control purposes specified as CTL formulas. Thus both safety and reachability games are supported. The talk will present the efficient on-the-fly algorithm used for synthesizing winning strategies for timed games, emphasizing recent methods used for achieving signicant improvement of performance compared with the first implementation (CONCUR05). UPPAAL Tiga allows for winning strategies to be represented as BDD/CDDs useful for compact embedded control programs. In the talk we also show how UPPAAL Tiga itself may be used for checking refinements between timed games (useful in settings of partial observability) and how the on-the-fly algorithm UPPAAL-Tiga may be used (and extended) to generate testing strategies for real-time systems.