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

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