Łukasiewicz mu-Calculus

Matteo Mio
Alex Simpson
(University of Edinburgh)

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 David Baelde and Arnaud Carayol: Proceedings Workshop on Fixed Points in Computer Science (FICS 2013), Turino, Italy, September 1st, 2013, Electronic Proceedings in Theoretical Computer Science 126, pp. 87–104.
Published: 28th August 2013.

ArXived at: http://dx.doi.org/10.4204/EPTCS.126.7 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org