Title: Controller automata, a Model for Real-Time Systems with Mutex Componet
Abstract: Timed automata are commonly recognized as a formal behavioral model for real-time systems. For compositional system design, parallel composition of timed automata as proposed by Larsen et al.is useful.
Although parallel composition provides a general method for system construction, in the low level behavior, components often behave sequentially by passing control via communication. This paper proposes a behavioral model, named controller automata, to combine timed automata by focusing on the control passing between components. In a controller automaton, to each state a timed automaton is assigned. A timed automaton at a state may be preempted by the control passing to another state by a global labeled transition. A controller automaton properly extends the expressive power because of the stack. We investigate the expressiveness and decidability results of the controller automata.
主讲人介绍：李国强博士于2008年获得日本北陆先端科学技术大学/Japan Advanced Institute of Science and Technology (JAIST)博士学位、2005年获得上海交通大学计算机系硕士学位。2008-09年期间任名古屋大学/ Nagoya University信息科学研究科博士后研究员,现为上海交通大学软件学院讲师。2012年获国家自然科学基金青年基金项目、并曾参与多项国家自然科学基金项目。研究方向为形式化验证、程序语言理论、软件工程理论。

时间：2012年2月28号（周二）13:30
地点：数学馆东202