Date: Thursday, September 14
Time: 10:00-11:00
Place: A3017 (CDT Demo Room)

A Complete Axiomatisation for Timed Automata


Professor Huimin Lin
Chinese Academy of  Sciences, Beijing


Timed automata have emerged as a popular model for real-time
systems. Many tools for analyzing and reasoning about real-time
systems are based on this model. Timed automata extend the traditional
notion of automata by associating each automaton with a finite set of
(real-valued) clock variables which can be tested and reset to
zero. In this talk I will introduce a language for describing
timed-automata, and present an complete inference system for deducing
bisimulation equivalence for them. The main novelty of this inference
system lies in separating manipulation of time from reasoning about
system behaviour.