Document Open Access Logo

SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators

Authors Daniel Gebler, Simone Tini

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.155.pdf
  • Filesize: 0.51 MB
  • 14 pages

Document Identifiers

Author Details

Daniel Gebler
Simone Tini

Cite As Get BibTex

Daniel Gebler and Simone Tini. SOS Specifications of Probabilistic Systems by Uniformly Continuous Operators. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 155-168, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CONCUR.2015.155

Abstract

Compositional reasoning over probabilistic systems wrt. behavioral metric semantics requires the language operators to be uniformly continuous. We study which SOS specifications define uniformly continuous operators wrt. bisimulation metric semantics. We propose an expressive specification format that allows us to specify operators of any given modulus of continuity. Moreover, we provide a method that allows to derive from any given specification the modulus of continuity of its operators.

Subject Classification

Keywords
  • SOS
  • probabilistic process algebra
  • bisimulation metric semantics
  • compositional metric reasoning
  • uniform continuity

Metrics

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

References

  1. Luca Aceto, Wan Fokkink, and Chris Verhoef. Structural operational semantics. In Handbook of Process Algebra, pages 197-292. Elsevier, 2001. Google Scholar
  2. Suzana Andova and Tim AC Willemse. Branching bisimulation for probabilistic systems: characteristics and decidability. TCS, 356(3):325-355, 2006. Google Scholar
  3. Falk Bartels. GSOS for probabilistic transition systems. In Proc. CMCS'02, volume 65 of ENTCS, pages 29-53. Elsevier, 2002. Google Scholar
  4. Falk Bartels. On Generalised Coinduction and Probabilistic Specification Formats. PhD thesis, VU University Amsterdam, 2004. Google Scholar
  5. Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. J. ACM, 42:232-268, 1995. Google Scholar
  6. Pedro R. D'Argenio, Daniel Gebler, and Matias David Lee. Axiomatizing Bisimulation Equivalences and Metrics from Probabilistic SOS Rules. In Proc. FoSSaCS'14, volume 8412 of LNCS, pages 289-303. Springer, 2014. Google Scholar
  7. Pedro R. D'Argenio and Matias David Lee. Probabilistic Transition System Specification: Congruence and Full Abstraction of Bisimulation. In Proc. FoSSaCS'12, volume 7213 of LNCS, pages 452-466. Springer, 2012. Google Scholar
  8. Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang. Metrics for Action-labelled Quantitative Transition Systems. In Proc. QAPL'05, volume 153 of EPTCS, pages 79-96, 2005. Google Scholar
  9. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for Labelled Markov Processes. TCS, 318(3):323-354, 2004. Google Scholar
  10. Josée Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden. The Metric Analogue of Weak Bisimulation for Probabilistic Processes. In Proc. LICS'02, pages 413-422. IEEE, 2002. Google Scholar
  11. Wan Fokkink, Rob J. van Glabbeek, and Paulien de Wind. Divide and congruence: From decomposition of modal formulas to preservation of branching and η-bisimilarity. I&C, 214:59-85, 2012. Google Scholar
  12. Daniel Gebler, Kim G. Larsen, and Simone Tini. Compositional metric reasoning with Probabilistic Process Calculi. In Proc. FoSSaCS'15, volume 9034 of LNCS, pages 230-245. Springer, 2015. Google Scholar
  13. Daniel Gebler and Simone Tini. Fixed-point Characterization of Compositionality Properties of Probabilistic Processes Combinators. In Proc. EXPRESS/SOS'14, volume 160 of EPTCS, pages 63-78. OPA, 2014. Google Scholar
  14. T.A. Henzinger. Quantitative reactive modeling and verification. Computer Science - R&D, 28(4):331-344, 2013. Google Scholar
  15. Bengt Jonsson and Wang Larsen, Kim G.and Yi. Probabilistic Extensions of Process Algebras. In Handbook of Process Algebra, pages 685-710. Elsevier, 2001. Google Scholar
  16. Ruggero Lanotte and Simone Tini. Probabilistic bisimulation as a congruence. ACM TOCL, 10:1-48, 2009. Google Scholar
  17. Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. I&C, 94:1-28, 1991. Google Scholar
  18. Matias David Lee, Daniel Gebler, and Pedro R. D'Argenio. Tree Rules in Probabilistic Transition System Specifications with Negative and Quantitative Premises. In Proc. EXPRESS/SOS'12, volume 89 of EPTCS, pages 115-130. OPA, 2012. Google Scholar
  19. Mohammad Reza Mousavi, Michel A. Reniers, and Jan Friso Groote. SOS formats and meta-theory: 20 years after. TCS, 373(3):238-272, 2007. Google Scholar
  20. Roberto Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, 1995. Google Scholar
  21. Simone Tini. Non-expansive ε-bisimulations for probabilistic processes. TCS, 411:2202-2222, 2010. Google Scholar
  22. Franck van Breugel and James Worrell. Towards quantitative verification of probabilistic transition systems. In Proc. ICALP'01, volume 2076 of LNCS, pages 421-432. Springer, 2001. Google Scholar
  23. Wang Yi and Kim Guldstrand Larsen. Testing probabilistic and nondeterministic processes. In PSTV, volume 12, pages 47-61, 1992. 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 About DROPS Imprint Privacy Contact