Document Open Access Logo

Divide and Congruence III: Stability & Divergence

Authors Wan Fokkink, Rob van Glabbeek, Bas Luttik

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.15.pdf
  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Author Details

Wan Fokkink
Rob van Glabbeek
Bas Luttik

Cite As Get BibTex

Wan Fokkink, Rob van Glabbeek, and Bas Luttik. Divide and Congruence III: Stability & Divergence. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CONCUR.2017.15

Abstract

In two earlier papers we derived congruence formats for weak semantics on the basis of a decomposition method for modal formulas. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. Here this work is extended with important stability and divergence requirements. Stability refers to the absence of a tau-transition. We show, using the decomposition method, how congruence formats can be relaxed for weak semantics that are stability-respecting. Divergence, which refers to the presence of an infinite sequence of tau-transitions, escapes the inductive decomposition method. We circumvent this problem by proving that a congruence format for a stability-respecting weak semantics is also a congruence format for its divergence-preserving counterpart.

Subject Classification

Keywords
  • Structural Operational Semantics
  • Compositionality
  • Congruence
  • Modal Logic
  • Modal Decomposition
  • Weak Semantics
  • Divergence

Metrics

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

References

  1. J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. Syntax and defining equations for an interrupt mechanism in process algebra. Fundamenta Informaticae, 9(2):127-167, 1986. Google Scholar
  2. T. Basten. Branching bisimulation is an equivalence indeed! Information Processing Letters, 58(3):141-147, 1996. URL: http://dx.doi.org/10.1016/0020-0190(96)00034-8.
  3. B. Bloom, W.J. Fokkink, and R.J. van Glabbeek. Precongruence formats for decorated trace semantics. Transactions on Computational Logic, 5(1):26-78, 2004. URL: http://dx.doi.org/10.1145/963927.963929.
  4. B. Bloom, S. Istrail, and A.R. Meyer. Bisimulation can't be traced. Journal of the ACM, 42(1):232-268, 1995. URL: http://dx.doi.org/10.1145/200836.200876.
  5. R. Bol and J.F. Groote. The meaning of negative premises in transition system specifications. Journal of the ACM, 43(5):863-914, 1996. URL: http://dx.doi.org/10.1145/234752.234756.
  6. W.J. Fokkink. Rooted branching bisimulation as a congruence. Journal of Computer and System Sciences, 60(1):13-37, 2000. URL: http://dx.doi.org/10.1006/jcss.1999.1663.
  7. W.J. Fokkink and R.J. van Glabbeek. Divide and congruence II: Delay and weak bisimilarity. In Proc. LICS 2016, pages 778-787. ACM/IEEE, 2016. URL: http://dx.doi.org/10.1145/2933575.2933590.
  8. W.J. Fokkink, R.J. van Glabbeek, and B. Luttik. Divide and congruence III: From decomposition of modal formulas to preservation of stability and divergence. Full version. URL: http://theory.stanford.edu/~rvg/abstracts.html#125.
  9. W.J. Fokkink, R.J. van Glabbeek, and P. de Wind. Divide and congruence: From decomposition of modalities to preservation of branching bisimulation. In Proc. FMCO 2005, volume 4111 of LNCS, pages 195-218, 2006. URL: http://dx.doi.org/10.1007/11804192_10.
  10. 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. Information and Computation, 214:59-85, 2012. URL: http://dx.doi.org/10.1016/j.ic.2011.10.011.
  11. R.J. van Glabbeek. The linear time-branching time spectrum II: The semantics of sequential systems with silent moves. In Proc. CONCUR 1993, volume 715 of LNCS, pages 66-81. Springer, 1993. URL: http://dx.doi.org/10.1007/3-540-57208-2_6.
  12. R.J. van Glabbeek. The meaning of negative premises in transition system specifications II. Journal of Logic and Algebraic Programming, 60/61:229-258, 2004. URL: http://dx.doi.org/10.1016/j.jlap.2004.03.007.
  13. R.J. van Glabbeek, B. Luttik, and N. Trc̆ka. Branching bisimilarity with explicit divergence. Fundamenta Informaticae, 93(4):371-392, 2009. URL: http://dx.doi.org/10.3233/FI-2009-109.
  14. R.J. van Glabbeek, B. Luttik, and N. Trc̆ka. Computation tree logic with deadlock detection. Logical Methods in Computer Science, 5(4), 2009. Google Scholar
  15. R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43(3):555-600, 1996. URL: http://dx.doi.org/10.1145/233551.233556.
  16. J.F. Groote. Transition system specifications with negative premises. Theoretical Computer Science, 118(2):263-299, 1993. URL: http://dx.doi.org/10.1016/0304-3975(93)90111-6.
  17. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, 1985. URL: http://dx.doi.org/10.1145/2455.2460.
  18. R. Milner. Communication and Concurrency. Prentice-Hall, 1989. Google Scholar
  19. I. Ulidowski. Equivalences on observable processes. In Proc. LICS 1992, pages 148-159. IEEE, 1992. URL: http://dx.doi.org/10.1109/LICS.1992.185529.
  20. I. Ulidowski and I. Phillips. Ordered SOS rules and process languages for branching and eager bisimulations. Information and Computation, 178(1):180-213, 2002. URL: http://dx.doi.org/10.1006/inco.2002.3161.
  21. I. Ulidowski and S. Yuen. Process languages for rooted eager bisimulation. In Proc. CONCUR 2000, volume 1877 of LNCS, pages 275-289. Springer, 2000. URL: http://dx.doi.org/10.1007/3-540-44618-4_21.
  22. F.W. Vaandrager. Algebraic Techniques for Concurrency and their Application. PhD thesis, University of Amsterdam, 1990. Google Scholar
  23. D. Walker. Bisimulation and divergence. Information and Computation, 85(2):202-241, 1990. URL: http://dx.doi.org/10.1016/0890-5401(90)90048-M.
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