Game semantics for probabilistic modal μ-calculi

Abstract

The probabilistic (or quantitative) modal μ-calculus is a fixed-point logic designed for expressing properties of probabilistic labeled transition systems (PLTS’s). 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. A first contribution of the thesis is to extend this coincidence result to arbitrary PLTS’s. A shortcoming of the probabilistic μ-calculus is the lack of expressiveness required to encode other important temporal logics for PLTS’s such as Probabilistic Computation Tree Logic (PCTL). To address this limitation, we extend the logic with a new pair of operators: independent product and coproduct, and we show that the resulting logic can encode the qualitative fragment of PCTL. Moreover, a further extension of the logic, with the operation of truncated sum and its dual, is expressive enough to encode full PCTL. A major contribution of the thesis is the definition of appropriate game semantics for these extended probabilistic μ-calculi. This relies on the definition of a new class of games, called tree games, which generalize standard 2-player stochastic games. In tree games, a play can be split into concurrent subplays which continue their evolution independently. Surprisingly, this simple device supports the encoding of the whole class of imperfect-information games known as Blackwell games. Moreover, interesting open problems in game theory, such as qualitative determinacy for 2-player stochastic parity games, can be reformulated as determinacy problems for suitable classes of tree games. Our main technical result about tree games is a proof of determinacy for 2-player stochastic metaparity games, which is the class of tree games that we use to give game semantics to the extended probabilistic μ-calculi. In order to cope with measure-theoretic technicalities, the proof is carried out in ZFC set theory extended with Martin’s Axiom at the first uncountable cardinal (MAℵ1). The final result of the thesis shows that the game semantics of the extended logics coincides with the denotational semantics, for arbitrary PLTS’s. However, in contrast to the earlier coincidence result, which is proved in ZFC, the proof of coincidence for the extended calculi is once again carried out in ZFC +MAℵ1 .