Expressiveness of Probabilistic Modal Logics, Revisited

Authors Nathanaël Fijalkow, Bartek Klin, Prakash Panangaden

Thumbnail PDF


  • Filesize: 489 kB
  • 12 pages

Document Identifiers

Author Details

Nathanaël Fijalkow
Bartek Klin
Prakash Panangaden

Cite AsGet BibTex

Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden. Expressiveness of Probabilistic Modal Logics, Revisited. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 105:1-105:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Labelled Markov processes are probabilistic versions of labelled transition systems. In general, the state space of a labelled Markov process may be a continuum. Logical characterizations of probabilistic bisimulation and simulation were given by Desharnais et al. These results hold for systems defined on analytic state spaces and assume that there are countably many labels in the case of bisimulation and finitely many labels in the case of simulation. In this paper, we first revisit these results by giving simpler and more streamlined proofs. In particular, our proof for simulation has the same structure as the one for bisimulation, relying on a new result of a topological nature. This departs from the known proof for this result, which uses domain theory techniques and falls out of a theory of approximation of Labelled Markov processes. Both our proofs assume the presence of countably many labels. We investigate the necessity of this assumption, and show that the logical characterization of bisimulation may fail when there are uncountably many labels. However, with a stronger assumption on the transition functions (continuity instead of just measurability), we can regain the logical characterization result, for arbitrarily many labels. These new results arose from a new game-theoretic way of understanding probabilistic simulation and bisimulation.
  • probabilistic modal logic
  • probabilistic bisimulation
  • probabilistic simulation


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. W. Arveson. An Invitation to C^*-Algebra. Springer-Verlag, 1976. Google Scholar
  2. M. Bernardo and M. Miculan. Disjunctive probabilistic modal logic is enough for bisimilarity on reactive probabilistic systems. In ICTCS, volume 1720, pages 203-220, 2016. Google Scholar
  3. P. Billingsley. Probability and Measure. Wiley-Interscience, 1995. Google Scholar
  4. R. Blute, J. Desharnais, A. Edalat, and P. Panangaden. Bisimulation for labelled Markov processes. In LICS, 1997. Google Scholar
  5. J. Desharnais. Labelled Markov Processes. PhD thesis, McGill University, 1999. Google Scholar
  6. J. Desharnais, A. Edalat, and P. Panangaden. A logical characterization of bisimulation for labelled Markov processes. In LICS, pages 478-489, 1998. Google Scholar
  7. J. Desharnais, A. Edalat, and P. Panangaden. Bisimulation for labeled Markov processes. Information and Computation, 179(2):163-193, 2002. Google Scholar
  8. J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Approximating labeled Markov processes. Information and Computation, 184(1):160-200, 2003. Google Scholar
  9. J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. A metric for labelled Markov processes. Theoretical Computer Science, 318(3):323-354, June 2004. Google Scholar
  10. M. Hennessy and R. Milner. On observing nondeterminism and concurrency. In ICALP, volume 85, pages 299-309, 1980. Google Scholar
  11. A. S. Kechris. Classical Descriptive Set Theory, volume 156 of Graduate Texts in Mathematics. Springer-Verlag, 1995. Google Scholar
  12. K. G. Larsen and A. Skou. Bisimulation through probablistic testing. Information and Computation, 94:1-28, 1991. Google Scholar
  13. P. Panangaden. Labelled Markov Processes. Imperial College Press, 2009. Google Scholar
  14. J. van Benthem. Modal correspondence theory. PhD thesis, University of Amsterdam, 1976. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail