[05-21] Symbolic semantics for Open Systems and their Bisimulation algorithms

文章來源:  |  發布時間:2019-05-16  |  【打印】 【關閉


  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 



  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. 



  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. 

浙江6十1走势图表 麻将游戏单机版下载 快乐8玩法介绍 河南快赢481往期走势图 5分快3怎么看大小 福建十一选五走势图表 4场进球技巧 股票配资排名官网 bugeyu捕鱼大师官网 宝博棋牌注册 河北快3基本二码遗漏 上海11选5走势图五码分布 北京快3基本走势图一定牛 新的网络赚钱平台 捉鸡麻将贵阳 云南快乐十分网上 福彩排七开奖走势图