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

• 作者: 余寒 张晋津
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: μ-演算 互模拟量词 并发 加权 轮替树自动机 ω展开 一致性内插
• 年，卷（期）: 2018,（11）
• 所属期刊栏目: 智能、算法、系统工程
• 页码范围: 22-25,29
• 页数: 5页
• 分类号: TP301
• 字数: 4639字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2018.11.005

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张晋津	南京航空航天大学计算机科学与技术学院	5	0	0.0	0.0
2	余寒	南京航空航天大学计算机科学与技术学院	2	0	0.0	0.0