如需要完整文档点击下方 "点击下载文档" 按钮

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

如需要完整文档点击下方 "点击下载文档" 按钮

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

将 完整文档 下载到本地，方便收藏和查阅

文件号：062807

点击下载文档