摘要：并发加权μ-演算(concurrent weightedμ-calculus,CWC)是对Kim.G.Larsen所提出的并发加权逻辑的强有力的扩充,通过加入不动点算子,增强表达能力,实现对复杂模块化系统的有效建模。对CWC进行了研究,给出了CWC的语法并阐述了CWC的标记加权转移语义。μ-演算与自动机理论密不可分,引入了轮替树自动机用于处理CWC,阐述了轮替树自动机与CWC之间的联系,构建了一种特定的用于CWC的轮替树自动机模型。一致性内插定理是Craig内插定理的加强和扩展,为了探究CWC上的一致性内插定理,根据Andrew M.Pitts提出的方法,利用互模拟量词寻找一致性插值。给出了互模拟量词在标记加权转移系统上的语义,并研究了互模拟量词和CWC上一致性内插定理之间的关系。在此过程中利用ω展开(unravelling),由ω展开树的一系列特性,结合轮替树自动机,证明了一致性内插定理在CWC上成立。
分类：期刊> 自然科学与工程技术> 信息科技> 电子信息科学综合
收录：统计源期刊(中国科技论文优秀期刊) > 知网收录(中) > 维普收录(中) > 万方收录(中) > 国家图书馆馆藏 > 上海图书馆馆藏
关键词：互模拟量词 并发 加权 轮替树自动机 一致性内插
注：因版权方要求，不能公开全文，如需全文，请咨询杂志社
