Determinizing timed automata

27^th March 2012, 16:00 G12
Dr. Nathalie Bertrand
INRIA Rennes Bretagne-Atlantique
France

Abstract

Timed automata are a popular model for real-time systems, that extend finite automata with clocks that can be tested and reset. Unfortunately, unlike finite automata, timed automata cannot be determinized in general. In this talk we will survey two approaches to overcome this difficulty. First of all, we present a generic determinization procedure that is applicable to all know determinizable subclasses. Second, we report on an approximate determinization algorithm based on the resolution of a simple safety game.