Abstract / Description of output
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.
Original language | English |
---|---|
Pages (from-to) | 87-104 |
Number of pages | 18 |
Journal | Electronic Proceedings in Theoretical Computer Science |
Volume | 126 |
DOIs | |
Publication status | Published - 2013 |