并发加权μ-演算的一致性内插

摘要：

并发加权μ -演算(concurrent weighted μ -calculus,CWC)是对Kim. G. Larsen所提出的并发加权逻辑的强有力的扩充,通过加入不动点算子,增强表达能力,实现对复杂模块化系统的有效建模.对CWC进行了研究,给出了CWC的语法并阐述了CWC的标记加权转移语义. μ-演算与自动机理论密不可分,引入了轮替树自动机用于处理CWC,阐述了轮替树自动机与CWC之间的联系,构建了一种特定的用于CWC的轮替树自动机模型.一致性内插定理是Craig内插定理的加强和扩展,为了探究CWC上的一致性内插定理,根据Andrew M. Pitts提出的方法,利用互模拟量词寻找一致性插值.给出了互模拟量词在标记加权转移系统上的语义,并研究了互模拟量词和CWC上一致性内插定理之间的关系.在此过程中利用ω展开(unravelling),由ω展开树的一系列特性,结合轮替树自动机,证明了一致性内插定理在CWC上成立.

关键词：μ-演算、互模拟量词、并发、加权、轮替树自动机、ω展开、一致性内插

所属期刊栏目：28

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金61602249

在线出版日期：2018-12-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：22-25,29