Specifying Properties for Modular π-Calculus

摘要：

We propose a modal logic for Modular π calculus 12: a logic to specify both temporal and spatial properties for processes in Modular π calculus. Characterization of process equivalence the logic induce is investigated,and it is shown that the distinguishing power of the logic falls between bisimilarity and structural congruence. Then a model checking algorithm for the logic over the finite-control subset of Modular π calculus is presented, and its correctness proved.

作者: Takashi KITAMURA Huimin LIN

作者单位: Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences

会议类型: 国际会议

会议名称: 第二届IFIP/IEEE软件工程理论基础国际研讨会(TASE 2008)(Second IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering)

会议地点: 南京

会议语种:英文

页码: 201-208

在线出版日期: 2008-06-17（万方平台首次上网日期，不代表论文的发表时间）