【Symbolic Semantics for Open Systems and Their Bisimulation Algorithms】
报告题目：Symbolic Semantics for Open Systems and Their Bisimulation Algorithms
报告人： Eric Madelaine 研究员 INRIA-Sophia Antipolis, France
主持人： 张敏 副教授
报告时间：2019年5月15日 周三14:00-15:00
报告地点：中北校区数学馆201
报告摘要：
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, that1) 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.
报告人简介：
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.