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


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.