Controller Synthesis for Real-Time Systems

Title: Controller Synthesis for Real-Time Systems
Speaker: Professor Kim G. Larsen (Center for Embedded Software Systems Aalborg University DENMARK)
Time: 9:30am, Wednesday, August 15
Venue: Lecture room, Lab for Computer Science, Level 3 Building #5, Institute of Software, CAS

Abstract:UPPAAL Tiga (CAV07) is a recent branch of the real-time verification tool UPPAAL (www.uppaal.com) allowing control programs to be synthesized from timed game automata models with respect to control purposes
specified as CTL formulas. Thus both safety and recahbility games are supported. The talk will present our symbolic extension of linear time local model checking algorithm, providing an efficient on-the-fly algorithm for synthesizing winning strategies for  timed games (CONCUR05).UPPAAL Tiga allows for winning strategies to be
represented as BDD/CDDs usefull 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.