Abstract: 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.

Key words: concurrent weighted logic, [μ]-calculus, alternating tree automata, decidability, small model property

摘要： 最近，针对为组合性标记加权转移系统建模的需要，Larsen等人提出了并发加权逻辑。该逻辑是多模态的，包含了反映给定状态的资源总量和限制转换过程的模态词，以及能够应对组合性系统的二元模态词，可以有效地表达系统的质化、量化和模块化的性质。为了增强并发加权逻辑的表达能力，对带不动点算子的并发加权逻辑——并发加权[μ]-演算进行了研究，给出了并发加权[μ]-演算的语法和标记加权转移语义，在表达能力与复杂性之间建立了良好的平衡。研究了并发加权[μ]-演算与轮替树自动机之间的联系，构建了一种特定的用于并发加权[μ]-演算的轮替树自动机模型。该自动机模型在表达能力上与并发加权[μ]-演算互模拟等价。在此基础上，进一步证明了并发加权[μ]-演算的可判定性及小模型性。

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