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

Uniform Interpolation of Concurrent Weighted μ-calculus

作　　者：余寒 张晋津[1] YU Han;ZHANG Jin-jin(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京210016

出　　处：《计算机技术与发展》2018年第11期22-25,29,共5页Computer Technology and Development

基　　金：国家自然科学基金(61602249)

摘　　要：并发加权μ-演算(concurrent weightedμ-calculus,CWC)是对Kim. G. Larsen所提出的并发加权逻辑的强有力的扩充,通过加入不动点算子,增强表达能力,实现对复杂模块化系统的有效建模。对CWC进行了研究,给出了CWC的语法并阐述了CWC的标记加权转移语义。μ-演算与自动机理论密不可分,引入了轮替树自动机用于处理CWC,阐述了轮替树自动机与CWC之间的联系,构建了一种特定的用于CWC的轮替树自动机模型。一致性内插定理是Craig内插定理的加强和扩展,为了探究CWC上的一致性内插定理,根据Andrew M. Pitts提出的方法,利用互模拟量词寻找一致性插值。给出了互模拟量词在标记加权转移系统上的语义,并研究了互模拟量词和CWC上一致性内插定理之间的关系。在此过程中利用ω展开(unravelling),由ω展开树的一系列特性,结合轮替树自动机,证明了一致性内插定理在CWC上成立。Concurrent weightedμ-calculus(CWC)extends the concurrent weighted logic(CWL)proposed by Kim.G.Larsen by including fixed point operators so as to increase its expressiveness.And CWC reflects the properties of complex modular system more effectively.The syntax and semantic on labeled weighted transition system of CWC is described.Automata theory is intimately related toμ-calculus,therefore the alternating tree automata is introduced to handle CWC.A coherent exposition of the connection of alternating tree automata and CWC is given,advocating an automaton model specifically working with CWC.Uniform interpolation is a very strong version of Craig interpolation.To research the uniform interpolation theorem on CWC,the uniform interpolation is found using the bisimulation quantifier according to the method proposed by Andrew M.Pitts.After introducing the semantic of bisimulation quantifier,the relation between bisimulation quantifier and uniform interpolation theorem on CWC is given.In the process,ωunravelling is introduced.By the properties ofωunravelling tree,with the alternating tree automata,the uniform interpolation theorem on CWC is proved to be true.

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

分 类 号：TP301[自动化与计算机技术—计算机系统结构]