Title: Specification Theories of Modal Transition Systems

Speaker: Mikael H. Moeller (Ph.d. Student, Aalborg University, Denmark)

Time: 2:30 pm, December 8th (Thursday), 2011.

Venue: Lecture room, the 3rd Floor, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences.

Abstract:

Modal transition systems (MTS) is a well-studied specification formalism

of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcome many of the limitations and we investigate the computational complexity of modal refinement checking.

Bibliography.

Mikael H. Moeller is a 2nd-year Ph.d. student from Aalborg University, Denmark. His main areas of interest include formal verification and system specification in component-based manner, mainly using different variants of Modal Transition Systems and Timed-Arc Petri Nets.