{\L}ukasiewicz {\mu}-calculus

TL;DR

This paper introduces the { extL}ukasiewicz { extmu}-calculus, extending logic with fixed points and scalar multiplication, providing effective computation procedures, and exploring its application to probabilistic systems and property verification.

Contribution

It develops the { extL}ukasiewicz { extmu}-calculus with fixed points, presents algorithms for evaluating its terms, and applies it to probabilistic transition systems and property encoding.

Findings

{ extL}ukasiewicz { extmu}-calculus defines monotone piecewise linear functions.

Algorithms for computing { extL}ukasiewicz { extmu}-calculus terms are effective.

The logic can encode properties of probabilistic nondeterministic systems.

Abstract

The paper explores properties of the {\L}ukasiewicz {\mu}-calculus, or {\L}{\mu} for short, an extension of {\L}ukasiewicz 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 {\L}ukasiewicz 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 {\L}ukasiewicz modal {\mu}-calculus formulas. We also show that the algorithms for computing values of {\L}ukasiewicz {\mu}-calculus terms provide automatic (albeit impractical) methods for verifying {\L}ukasiewicz modal {\mu}-calculus properties of finite rational PNTS's.