Łukasiewicz μ-calculus

DOI10.3233/FI-2017-1472zbMATH Open1380.68281arXiv1510.00797OpenAlexW2185433846MaRDI QIDQ4589613FDOQ4589613

Alex Simpson, Matteo Mio

Publication date: 10 November 2017

Published in: Fundamenta Informaticae (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1510.00797

zbMATH Keywords

model checkingprobabilistic \(\mu\)-calculusPCTLŁukasiewicz logic

Mathematics Subject Classification ID

Many-valued logic (03B50) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (16)

• Linear abelian modal logic
• Title not available (Why is that?)
• Sound approximate and asymptotic probabilistic bisimulations for PCTL
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Solving Łukasiewicz \(\mu\)-terms
• Title not available (Why is that?)
• Coinduction in Flow: The Later Modality in Fibrations
• Systems of fixpoint equations: abstraction, games, up-to techniques and local algorithms
• Title not available (Why is that?)
• Title not available (Why is that?)
• -Calculus with Explicit Points and Approximations
• Free modal Riesz spaces are Archimedean: a syntactic proof
• Title not available (Why is that?)
• Title not available (Why is that?)

This page was built for publication: Łukasiewicz μ-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4589613)