On the equivalence of game and denotational semantics for the probabilistic μ -calculus

Matteo Mio 1, 2
1 COMETE - Concurrency, Mobility and Transactions
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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 proof technique for proving result of parity games by induction on their complexity.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (2), pp.1-21
Liste complète des métadonnées

https://hal.inria.fr/hal-00763454
Contributeur : Matteo Mio <>
Soumis le : lundi 10 décembre 2012 - 18:57:20
Dernière modification le : jeudi 10 mai 2018 - 02:06:08

Lien texte intégral

Identifiants

  • HAL Id : hal-00763454, version 1
  • ARXIV : 1205.0126

Collections

Citation

Matteo Mio. On the equivalence of game and denotational semantics for the probabilistic μ -calculus. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, 8 (2), pp.1-21. 〈hal-00763454〉

Partager

Métriques

Consultations de la notice

196