Faculty Colloq & CSE600: Generalized Synchronization Trees

Dates: 
Friday, December 2, 2016 - 14:30 to 16:00
Location: 
Room 120, New Computer Science

Generalized Synchronization Trees

Presented by:
Prof. Rance Cleaveland
Department of Computer Science
University of Maryland at College Park

Abstract: Process-algebraic theories of system modeling focus on composition operators as a basis for defining systems. Mathematically, these operators are interpreted as functions over a space of system behaviors that capture how systems execute. The basic theory for discrete systems was initially developed by Milner in the early 1980s using so-called synchronization trees as the basic semantic model for systems; a notion of equivalence, called bisimulation equivalence, was then introduced on top of these trees as a basis for reasoning about when different trees nevertheless are behaviorally indistinguishable. Subsequent work by many other researchers showed how a variety of useful composition operators, including various forms of parallel composition, choice, interrupt-handling, and the like, could be encoded cleanly in this framework, with equivalence relations based on bisimulation used to reason about actual systems.
This talk will explore how the notion of synchronization tree can be generalized to systems, such as cyber-physical systems, having continuous as well as discrete behavior. The notion of generalized synchronization tree will be introduced and shown to conservatively extend Milner’s notion of synchronization tree. We then explore notions of bisimulation this extended setting and show that notions that coincide in the discrete world can be distinguished in our more general setting. Finally, we show how notions of composition defined in the discrete setting can be carried over to the new framework, yielding a rich array of composition operators that may be used in defining hybrid systems.

Speaker Bio: Rance Cleaveland is Professor of Computer Science at the University of Maryland (UMD) at College Park. He is also a co-founder Reactive Systems, Inc., a company that makes model-based testing tools for embedded software, and a past Executive and Scientific Director of the Fraunhofer Center for Experimental Software Engineering in College Park. Prior to joining the UMD faculty in 2005, he held professorships at the State University of New York at Stony Brook and at North Carolina State University (NCSU). He is a past recipient of Young Investigator Awards from the US National Science Foundation and from the Office of Naval Research; the Alcoa Engineering Research Achievement prize at North Carolina State University; and teaching awards from NCSU and UMD. He has published over 140 papers in the areas of software verification and validation, formal methods, model checking, software specification formalisms, verification tools, software testing, and software architecture. Cleaveland received B.S. degrees in Mathematics and Computer Science from Duke University and M.S. and Ph.D. degrees in Computer Science from Cornell University.

Computed Event Type: 
Mis
Event Title: 
Faculty Colloq & CSE600: Generalized Synchronization Trees