Łukasiewicz mu-Calculus

Abstract

The paper explores properties of Łukasiewicz mu-calculus, a version of the quantitative/probabilistic modal mu-calculus containing both weak and strong conjunctions and disjunctions from Łukasiewicz (fuzzy) logic. We show that this logic encodes the well-known probabilistic temporal logic PCTL. And we give a model-checking algorithm for computing the rational denotational value of a formula at any state in a finite rational probabilistic nondeterministic transition system.

In Proceedings FICS 2013, arXiv:1308.5896

References in corpus (2)

• Probabilistic modal μ-calculus with independent product
• On the equivalence of game and denotational semantics for the probabilistic mu-calculus

Cited by in corpus (3)

• A Real-Valued Modal Logic
• Probabilistic logics based on Riesz spaces
• Fixpoint Games on Continuous Lattices