Łukasiewicz -calculus

DOI10.3233/FI-2017-1472MaRDI QIDQ4589613zbMATH OpenOpenAlexFDO

Authors Matteo Mio, Alex Simpson

Publication date 10 November 2017

Published in Fundamenta Informaticae (Search for Journal in Brave)

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)

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.

Recommendations

• scientific article; zbMATH DE number 7357543
• Solving Łukasiewicz \(\mu\)-terms
• Results on the propositional \(\mu\)-calculus
• scientific article; zbMATH DE number 1330140
• Probabilistic temporal logics via the modal mu-calculus

Cited in

(17)

• Linear abelian modal logic
• scientific article; zbMATH DE number 7566075 (Why is no real title available?)
• Sound approximate and asymptotic probabilistic bisimulations for PCTL
• Solving Łukasiewicz \(\mu\)-terms
• Behavioural equivalences for timed systems
• scientific article; zbMATH DE number 6841178 (Why is no real title available?)
• Coinduction in Flow: The Later Modality in Fibrations
• Proof theory of Riesz spaces and modal Riesz spaces
• Probabilistic logics based on Riesz spaces
• Separable GPL: decidable model checking with more non-determinism
• Systems of fixpoint equations: abstraction, games, up-to techniques and local algorithms
• scientific article; zbMATH DE number 7559481 (Why is no real title available?)
• scientific article; zbMATH DE number 7559483 (Why is no real title available?)
• -Calculus with Explicit Points and Approximations
• Free modal Riesz spaces are Archimedean: a syntactic proof
• scientific article; zbMATH DE number 1406235 (Why is no real title available?)
• scientific article; zbMATH DE number 7357543 (Why is no real title available?)

This page was built for publication: Łukasiewicz \(\mu\)-calculus

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