并发加权μ-演算的若干性质  

Some Properties of Concurrent Weighted μ-Calculus

作　　者：余寒 YU Han(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)

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

出　　处：《计算机科学与探索》2018年第10期1684-1690,共7页Journal of Frontiers of Computer Science and Technology

基　　金：国家自然科学基金No.61602249~~

摘　　要：最近,针对为组合性标记加权转移系统建模的需要,Larsen等人提出了并发加权逻辑。该逻辑是多模态的,包含了反映给定状态的资源总量和限制转换过程的模态词,以及能够应对组合性系统的二元模态词,可以有效地表达系统的质化、量化和模块化的性质。为了增强并发加权逻辑的表达能力,对带不动点算子的并发加权逻辑——并发加权μ-演算进行了研究,给出了并发加权μ-演算的语法和标记加权转移语义,在表达能力与复杂性之间建立了良好的平衡。研究了并发加权μ-演算与轮替树自动机之间的联系,构建了一种特定的用于并发加权μ-演算的轮替树自动机模型。该自动机模型在表达能力上与并发加权μ-演算互模拟等价。在此基础上,进一步证明了并发加权μ-演算的可判定性及小模型性。Recently,Larsen and others propose concurrent weighted logic(CWL)so that compositional labeled weighted transition system(LWS)can be modeled.CWL is a multimodal logic which contains modal operators indexed with rational numbers to reflect the resources of the given state and restrict the transition of LWSs as well as a binary modal operator that encodes properties concerning the composition of LWSs.Therefore,the qualitative,quantitative and modular properties of LWSs can be expressed efficiently.To increase the expressiveness of CWL,this paper develops the concurrent weightedμ-calculus(CWC),which extends CWL by including fixed point operators.The syntax and semantic on LWS of CWC are given.And the balance between expressive power and complexity is established.Besides,an internal connection between CWC and alternating tree automata is researched,advocating an automaton model specifically tailored for working with CWC.The automaton model proposed is really equivalent to CWC with respect to expressive power in bisimilar level.On this basis this paper shows the decidability and small model property of CWC.

关 键 词：并发加权逻辑 μ-演算 轮替树自动机 可判定性 小模型性 

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