On the equivalence of game and denotational semantics for the probabilistic mu-calculus
Matteo Mio (LIX, Ecole Polytechnique)

TL;DR
This paper proves that the denotational and game semantics for the probabilistic mu-calculus are equivalent on all models, including infinite ones, strengthening the theoretical understanding of this logic.
Contribution
It establishes the equivalence of denotational and game semantics for the probabilistic mu-calculus on arbitrary models, extending previous results limited to finite systems.
Findings
Proves equivalence on infinite models
Uses unraveling method for proof
Strengthens theoretical foundation of probabilistic mu-calculus
Abstract
The probabilistic (or quantitative) modal mu-calculus is a fixed-point logic de- signed for expressing properties of probabilistic labeled transition systems (PLTS). Two semantics have been studied for this logic, both assigning to every process state a value in the interval [0,1] representing the probability that the property expressed by the formula holds at the state. One semantics is denotational and the other is a game semantics, specified in terms of two-player stochastic games. The two semantics have been proved to coincide on all finite PLTS's, but the equivalence of the two semantics on arbitrary models has been open in literature. In this paper we prove that the equivalence indeed holds for arbitrary infinite models, and thus our result strengthens the fruitful connection between denotational and game semantics. Our proof adapts the unraveling or unfolding method, a general…
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.
Taxonomy
TopicsSemantic Web and Ontologies · Logic, Reasoning, and Knowledge · Multi-Agent Systems and Negotiation
