Document Open Access Logo

Logical Characterization of Bisimulation for Transition Relations over Probability Distributions with Internal Actions

Authors Matias David Lee, Erik P. de Vink

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2016.29.pdf
  • Filesize: 0.55 MB
  • 14 pages

Document Identifiers

Author Details

Matias David Lee
Erik P. de Vink

Cite AsGet BibTex

Matias David Lee and Erik P. de Vink. Logical Characterization of Bisimulation for Transition Relations over Probability Distributions with Internal Actions. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 29:1-29:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.MFCS.2016.29

Abstract

In recent years the study of probabilistic transition systems has shifted to transition relations over distributions to allow for a smooth adaptation of the standard non-probabilistic apparatus. In this paper we study transition relations over probability distributions in a setting with internal actions. We provide new logics that characterize probabilistic strong, weak and branching bisimulation. Because these semantics may be considered too strong in the probabilistic context, Eisentraut et al. recently proposed weak distribution bisimulation. To show the flexibility of our approach based on the framework of van Glabbeek for the non-deterministic setting, we provide a novel logical characterization for the latter probabilistic equivalence as well.
Keywords
  • probabilistic transition systems
  • weak bisimulations
  • logical characterization
  • transition relation over distributions
  • modal logics

Metrics

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

References

  1. J.C.M. Baeten and R. J. van Glabbeek. Another look at abstraction in process algebra. In T. Ottmann, editor, Proc. ICALP'87, pages 84-94. LNCS 267, 1987. Google Scholar
  2. S. Crafa and F. Ranzato. Logical characterizations of behavioral relations on transition systems of probability distributions. TOCL, 16(1):2:1-24, 2014. Google Scholar
  3. P.R. D'Argenio and M.D. Lee. Probabilistic transition system specification: Congruence and full abstraction of bisimulation. In L. Birkedal, editor, Proc. FOSSACS 2012, 2012. Google Scholar
  4. P.R. D'Argenio, M.D. Lee, and D. Gebler. SOS rule formats for convex and abstract probabilistic bisimulations. In S. Crafa et al., editor, Proc. EXPRESS/SOS 2015, 2015. Google Scholar
  5. Y. Deng and M. Hennessy. On the semantics of Markov automata. Information and Computation, 222:139-168, 2013. Google Scholar
  6. Y. Deng, R. J. van Glabbeek, M Hennessy, and C. Morgan. Characterising testing preorders for finite probabilistic processes. Logical Methods in Computer Science, 4(4), 2008. Google Scholar
  7. Y. Deng and R.J. van Glabbeek. Characterising probabilistic processes logically. CoRR, abs/1007.5188, 2010. Google Scholar
  8. J. Desharnais, V. Gupta, R. Jagadeesan, and P Panangaden. Weak bisimulation is sound and complete for PCTL^*. Information and Computation, 208(2):203-219, 2010. Google Scholar
  9. C. Eisentraut, H. Hermanns, J. Krämer, A. Turrini, and L. Zhang. Deciding bisimilarities on distributions. In Joshi, K.R. et al., editor, Proc. QEST 2013, pages 72-88, 2013. Google Scholar
  10. M. Hennessy. Exploring probabilistic bisimulations, part I. Formal Aspects of Computing, 24(4-6):749-768, 2012. Google Scholar
  11. H. Hermanns, J. Krcál, and J. Kretínský. Probabilistic bisimulation: Naturally on distributions. In P. Baldan and D. Gorla, editors, Proc. CONCUR 2014, pages 249-265, 2014. Google Scholar
  12. H. Hermanns, A. Parma, R. Segala, B. Wachter, and L. Zhang. Probabilistic logical characterization. Information and Computation, 209(2):154-172, 2011. Google Scholar
  13. K.G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, 1991. Google Scholar
  14. N.A. Lynch, R. Segala, and F.W. Vaandrager. Observing branching structure through probabilistic contexts. SIAM Journal of Computing, 37(4):977-1013, 2007. Google Scholar
  15. M. Mio. Upper-expectation bisimilarity and Łukasiewicz μ-calculus. In A. Muscholl, editor, Proc. FoSSaCS, pages 335-350, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54830-7_22.
  16. M. Mio and A.K. Simpson. Łukasiewicz μ-calculus. CoRR, abs/1510.00797, 2015. Google Scholar
  17. A. Parma and R. Segala. Logical characterizations of bisimulations for discrete probabilistic systems. In H. Seidl, editor, Proc. FOSSACS 2007, pages 287-301. LNCS 4423, 2007. Google Scholar
  18. J. Sack and L. Zhang. A general framework for probabilistic characterizing formulae. In VMCAI 2012, Philadelphia, USA, January, 2012. Proceedings, pages 396-411, 2012. Google Scholar
  19. L. Song, L. Zhang, and J.C. Godskesen. Bisimulations meet PCTL equivalences for probabilistic automata. Logical Methods in Computer Science, 9(2), 2013. Google Scholar
  20. M.I.A. Stoelinga. Alea jacta est: verification of probabilistic, real-time and parametric systems. PhD thesis, Radboud Universiteit Nijmegen, 2002. Google Scholar
  21. R. J. van Glabbeek. The linear time-branching time spectrum II. In E. Best, editor, Proc. CONCUR '93, pages 66-81. LNCS 715, 1993. Google Scholar
  22. R. J. van Glabbeek and W. P. Weijland. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555-600, 1996. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact