id: 06040185
dt: j
an: 06040185
au: Mio, Matteo
ti: On the equivalence of game and denotational semantics for the probabilistic
    $μ$-calculus.
so: Log. Methods Comput. Sci. 8, No. 2, Paper No. 7, 21 p., electronic only
    (2012).
py: 2012
pu: Logical Methods in Computer Science c/o Institute of Theoretical Computer
    Science, Technical University of Braunschweig, Braunschweig
la: EN
cc: 
ut: probabilistic temporal logic; game semantics; two-player stochastic games;
    modal $μ$-calculus
ci: 
li: doi:10.2168/LMCS-8(2:7)2012
ab: Summary: The probabilistic (or quantitative) modal $μ$-calculus is a
    fixed-point logic designed 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 PLTSs, 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 proof technique for proving result of
    parity games by induction on their complexity.
rv: