Title: Symbolic semantics for Open Systems and their Bisimulation algorithms. 

　　Speaker: Dr. Eric Madelaine (INRIA Sophia-Antipolis) 

　　Venue: Seminar Room (Room 334), Building No. 5, Institute of Software, CAS 

　　Time: 10:00, Tuesday May 21th, 2019 

　　Abstract: 

　　pNets (parameterized Networks of synchronized automata) have been defined as a semantic model to represent the behavior of systems of interacting processes with explicit data, flexible process synchronization, and hierarchical system construction. We model "open systems" in the sense of interaction with some environment encoded as process parameters with unspecified behavior, named "holes". The main motivation of this work is to provide a model that 

　　1) have good compositionality properties: logical properties and equivalences should be preserved by holes instanciation; 

　　2) can be represented by (symbolic) finite automata, allowing the implementation of model-checking and equivalence-checking algorithms.    

　　We present the basic definitions and results of the pNet formalism and the "open automaton" semantics. We define our notion of (strong) FH-bisimulation, and its properties; then show how we can define algorithms for: 

　　- checking that a given relation is a FH-bisimulation 

　　- given the initial states of 2 open automata, generate the minimal hypothesis that would make them bisimilar (in an on-the-fly manner).  

　　Both algorithms rely on SMT techniques to handle the data part of the reasoning. 

　　Bio: 

　　Dr. Eric Madelaine has an engineer diploma from Ecole Polytechnique de Paris, a PhD in computer science in 1983 from university of Paris 7, and an HdR from university of Nice Sophia-Antipolis in 2011. He is a researcher at INRIA since 1983, and he is currently member the Kairos research-team at INRIA Sophia-Antipolis. His research domains range from programming language semantics and process algebras, formal methods and model-checking, to specification and verification techniques for distributed applications. He has been member of 20+ program committees, and he is chair of the steering committee of the FACS symposium. He has been participating in many French and European projects, and he was PI in various bilateral projects, including Chile, Argentina, and China.  

　　Recent research topics: 

　　-        Behavioral semantics of concurrent, distributed, communicating, synchronous or asynchronous, software systems. 

　　-        Formal methods for specification, requirements, models, analysis of such systems. 

　　-        Tool assisted methods for the verification of concurrent and communicating systems, including model-checking, equivalence checking, and satisfiability based approaches. 

　　-        Compositional / symbolic approaches for verification of large distributed software systems. 

　　-        Algorithms, tools, and software environments for automatic verification.