Affiliations: [a] Laboratoire de l’Informatique du Parallèlisme, CNRS and École Normale Supérieure de Lyon, France. matteo.mio@ens-lyon.fr | [b] Faculty of Mathematics and Physics, University of Ljubljana, Slovenia. Alex.Simpson@fmf.uni-lj.si
Correspondence:
[C]
Address for correspondence: Laboratoire de l’Informatique du Parallélisme, CNRS and École Normale Supérieure de Lyon, 46 Allée d’Italie, Lyon 69364, France.
Note: [*] The first author carried out part of this work during the tenure of an ERCIM “Alain Bensoussan” Fellowship, supported by the Marie Curie Co-funding of Regional, National and International Programmes (COFUND) of the European Commission. He also acknowledges the support of the ERC advanced grant ECSYM and of the grant “Projet Émergent PMSO” of the École Normale Supérieure de Lyon.
Note: [†] Work carried out at the Universities of Edinburgh and Ljubljana. This material is based upon work supported by the Air Force Office of Scientific Research, Air Force Material Command, USAF under Award No. FA9550-14-1-0096.
Abstract: 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 piece-wise 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.
Keywords: Łukasiewicz logic, Probabilistic μ-Calculus, Model Checking, PCTL
