The paper explores properties of Lukasiewicz mu-calculus, a version of the quantitative/probabilistic modal mu-calculus containing both weak and strong conjunctions and disjunctions from Lukasiewicz (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.
|Number of pages||18|
|Journal||Electronic Proceedings in Theoretical Computer Science|
|Publication status||Published - 2013|