摘要 : The paper explores properties of the Lukasiewicz mu-calculus, or L mu for short, an extension of Lukasiewicz logic with scalar multiplication and least and greatest fixed-point operators (for monotone formulas). We observe that L ... 展开 The paper explores properties of the Lukasiewicz mu-calculus, or L mu for short, an extension of Lukasiewicz logic with scalar multiplication and least and greatest fixed-point operators (for monotone formulas). We observe that L mu terms, with n variables, define monotone piecewise linear functions from [0, 1](n) to [0, 1]. Two effective procedures for calculating the output of L mu terms on rational inputs are presented. We then consider the Lukasiewicz modal mu-calculus, which is obtained by adding box and diamond modalities to L mu. Alternatively, it can be viewed as a generalization of Kozen's modal mu-calculus adapted to probabilistic nondeterministic transition systems (PNTS's). We show how properties expressible in the well-known logic PCTL can be encoded as Lukasiewicz modal mu-calculus formulas. We also show that the algorithms for computing values of Lukasiewicz mu-calculus terms provide automatic (albeit impractical) methods for verifying Lukasiewicz modal mu-calculus properties of finite rational PNTS's. 收起