并发加权 μ-演算的一致性内插-《计算机技术与发展》

文章信息/Info

Author(s):: YU Han; ZHANG Jin-jin; School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China

Keywords:: μ-calculus; bisimulation quantifier; concurrent; weighted; alternating tree automata; ω unravelling; uniform interpolation

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

Abstract:: 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 nterpolation is found using the bisimulation quantifier according to the method proposed by Andrew M. Pitts. After introducing the semantic of bisimulation uantifier,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.