{\L}ukasiewicz mu-Calculus
Matteo Mio (CWI), Alex Simpson (University of Edinburgh)
TL;DR
This paper introduces the { extL}ukasiewicz mu-calculus, a fuzzy logic variant that encodes probabilistic temporal logic PCTL and provides a model-checking algorithm for finite systems.
Contribution
It presents the formal properties of the { extL}ukasiewicz mu-calculus, demonstrating its encoding of PCTL and offering a new model-checking method for probabilistic systems.
Findings
The logic encodes PCTL.
A model-checking algorithm is developed.
Applicable to finite rational probabilistic systems.
Abstract
The paper explores properties of {\L}ukasiewicz mu-calculus, a version of the quantitative/probabilistic modal mu-calculus containing both weak and strong conjunctions and disjunctions from {\L}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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.