2015/10/03 by Matteo Mio, Mio, Matteo, Alex Simpson +1 · 1 citation
Mathematics · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Probability and Statistical Research
paper · pdf · doi:10.48550/arxiv.1510.00797
openalex publication_date 2015/10/03 · openalex created_date 2019/07/30 · openalex updated_date 2026/07/28
The paper explores properties of the Łukasiewicz μ-calculus, or Łμ for short, an extension of Łukasiewicz logic with scalar multiplication and least and greatest fixed-point operators (for monotone formulas). We observe that Łμ terms, with n variables, define monotone piecewise linear functions from [0, 1]n to [0, 1]. Two effective procedures for calculating the output of Łμ terms on rational inputs are presented. We then consider the Łukasiewicz modal μ-calculus, which is obtained by adding box and diamond modalities to Łμ. Alternatively, it can be viewed as a generalization of Kozen's modal μ-calculus adapted to probabilistic nondeterministic transition systems (PNTS's). We show how properties expressible in the well-known logic PCTL can be encoded as Łukasiewicz modal μ-calculus formulas. We also show that the algorithms for computing values of Łukasiewicz μ-calculus terms provide automatic (albeit impractical) methods for verifying Łukasiewicz modal μ-calculus properties of finite rational PNTS's.