Document Open Access Logo

Modal Decomposition on Nondeterministic Probabilistic Processes

Authors Valentina Castiglioni, Daniel Gebler, Simone Tini

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.36.pdf
  • Filesize: 0.51 MB
  • 15 pages

Document Identifiers

Author Details

Valentina Castiglioni
Daniel Gebler
Simone Tini

Cite AsGet BibTex

Valentina Castiglioni, Daniel Gebler, and Simone Tini. Modal Decomposition on Nondeterministic Probabilistic Processes. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 36:1-36:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CONCUR.2016.36

Abstract

We propose a SOS-based method for decomposing modal formulae for nondeterministic probabilistic processes. The purpose is to reduce the satisfaction problem of a formula for a process to verifying whether its subprocesses satisfy certain formulae obtained from its decomposition. By our decomposition, we obtain (pre)congruence formats for probabilistic bisimilarity, ready similarity and similarity.
Keywords
  • SOS
  • nondeterministic probabilistic process algebras
  • logical characterization
  • decomposition of modal formulae

Metrics

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

References

  1. S. Andova and T.A.C. Willemse. Branching bisimulation for probabilistic systems: characteristics and decidability. Theoret. Comput. Sci., 356(3):325-355, 2006. Google Scholar
  2. B. Bloom, W. J. Fokkink, and R. J. van Glabbeek. Precongruence formats for decorated trace semantics. ACM Trans. Comput. Log., 5(1):26-78, 2004. Google Scholar
  3. B. Bloom, S. Istrail, and A. R. Meyer. Bisimulation can't be traced. J. ACM, 42(1):232-268, 1995. Google Scholar
  4. V. Castiglioni, D. Gebler, and S. Tini. Logical characterization of bisimulation metrics. In Proc. QAPL 2016, Electronic Proceedings in Theoretical Computer Science, 2016. Google Scholar
  5. P. R. D'Argenio, D. Gebler, and M. D. Lee. Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules. In Proc. FoSSaCS 2014, volume 8412 of Lecture Notes in Computer Science, pages 289-303. Springer, 2014. Google Scholar
  6. P. R. D'Argenio and M. D. Lee. Probabilistic transition system specification: Congruence and full abstraction of bisimulation. In Proc. FoSSaCS 2012, volume 7213 of Lecture Notes in Computer Science, pages 452-466. Springer, 2012. Google Scholar
  7. Y. Deng and W. Du. Logical, metric, and algorithmic characterisations of probabilistic bisimulation. CoRR, abs/1103.4577, 2011. Google Scholar
  8. Y. Deng and R. J. van Glabbeek. Characterising probabilistic processes logically - (extended abstract). In Proc. LPAR-17, volume 6397 of Lecture Notes in Computer Science, pages 278-293. Springer, 2010. Google Scholar
  9. 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
  10. J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Metrics for labelled markov processes. Theoret. Comput. Sci., 318(3):323-354, 2004. Google Scholar
  11. J. Desharnais, R. Jagadeesan, V. Gupta, and P. Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In Proc. LICS 2002, pages 413-422. IEEE Computer Society, 2002. Google Scholar
  12. W. J. Fokkink and R. J. van Glabbeek. Divide and congruence II: from decomposition of modal formulas to preservation of delay and weak bisimilarity. CoRR, abs/1604.07530, 2016. Google Scholar
  13. W. J. Fokkink, R. J. van Glabbeek, and P. de Wind. Compositionality of Hennessy-Milner logic by structural operational semantics. Theoret. Comput. Sci., 354(3):421-440, 2006. Google Scholar
  14. W. J. Fokkink, R. J. van Glabbeek, and P. de Wind. Divide and congruence: From decomposition of modal formulas to preservation of branching and η-bisimilarity. Inf. Comput., 214:59-85, 2012. Google Scholar
  15. D. Gebler and W. J. Fokkink. Compositionality of probabilistic Hennessy-Milner logic through structural operational semantics. In Proc. CONCUR 2012, volume 7454 of Lecture Notes in Computer Science, pages 395-409. Springer, 2012. Google Scholar
  16. D. Gebler, K. G. Larsen, and S. Tini. Compositional metric reasoning with Probabilistic Process Calculi. In Proc. FoSSaCS'15, volume 9034 of Lecture Notes in Computer Science, pages 230-245. Springer, 2015. Google Scholar
  17. D. Gebler, K. G. Larsen, and S. Tini. Compositional metric reasoning with Probabilistic Process Calculi. Logical Methods in Computer Science, 2016. Google Scholar
  18. D. Gebler and S. Tini. SOS specifications of probabilistic systems by uniformly continuous operators. In Proc. CONCUR 2015, volume 42 of LIPIcs, pages 155-168. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  19. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32:137-161, 1985. Google Scholar
  20. R. Lanotte and S. Tini. Probabilistic bisimulation as a congruence. ACM Trans. Comput. Log., 10:1-48, 2009. Google Scholar
  21. K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Inf. Comput., 94(1):1-28, 1991. Google Scholar
  22. K. G. Larsen and L. Xinxin. Compositionality through an operational semantics of contexts. J. Log. Comput., 1(6):761-795, 1991. Google Scholar
  23. G. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Aarhus University, 1981. Google Scholar
  24. R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, 1995. Google Scholar
  25. F. van Breugel and J. Worrell. An algorithm for quantitative verification of probabilistic transition systems. In Proc. CONCUR 2001, volume 2154 of Lecture Notes in Computer Science, pages 336-350. Springer, 2001. 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