Skip to main content
SpringerLink
Log in

Divide and Congruence: From Decomposition of Modalities to Preservation of Branching Bisimulation

  • Conference paper
Formal Methods for Components and Objects (FMCO 2005)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 4111))

Included in the following conference series:

Abstract

We present a method for decomposing modal formulas for processes with the internal action τ. To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy formulas that are obtained by decomposing the original formula. The decomposition uses the structural operational semantics that underlies the process algebra. We use this decomposition method to derive congruence formats for branching and rooted branching bisimulation equivalence.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Information and Control 60(1/3), 109–137 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  2. Bloom, B.: Structural operational semantics for weak bisimulations. Theoretical Computer Science 146(1/2), 25–68 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  3. Bloom, B., Fokkink, W.J., van Glabbeek, R.J.: Precongruence formats for decorated trace semantics. ACM Transactions on Computational Logic 5(1), 26–78 (2004)

    Article  MathSciNet  Google Scholar 

  4. Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. Journal of the ACM 42(1), 232–268 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  5. Bol, R.N., Groote, J.F.: The meaning of negative premises in transition system specifications. Journal of the ACM 43(5), 863–914 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  6. De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. Journal of the ACM 42(2), 458–487 (1995)

    Article  MATH  Google Scholar 

  7. Fokkink, W.J.: Rooted branching bisimulation as a congruence. Journal of Computer and System Sciences 60(1), 13–37 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  8. Fokkink, W.J., van Glabbeek, R.J.: Ntyft/ntyxt rules reduce to ntree rules. Information and Computation 126(1), 1–10 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  9. Fokkink, W.J., van Glabbeek, R.J., de Wind, P.: Compositionality of Hennessy-Milner logic by structural operational semantics. Theoretical Computer Science 354(3), 421–440 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  10. Fokkink, W.J., van Glabbeek, R.J., de Wind, P.: Divide and congruence applied to η-bisimulation. In: Proc. SOS 2005. ENTCS. Elsevier, Amsterdam (to appear, 2005)

    Google Scholar 

  11. van Glabbeek, R.J.: The linear time-branching time spectrum II: The semantics of sequential systems with silent moves. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)

    Google Scholar 

  12. van Glabbeek, R.J.: The meaning of negative premises in transition system specifications II. Journal of Logic and Algebraic Programming 60/61, 229–258 (2004)

    Article  Google Scholar 

  13. van Glabbeek, R.J.: On cool congruence formats for weak bisimulations (extended abstract). In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 331–346. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  14. van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), 555–600 (1996)

    Article  MathSciNet  Google Scholar 

  15. Groote, J.F.: Transition system specifications with negative premises. Theoretical Computer Science 118(2), 263–299 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  16. Groote, J.F., Vaandrager, F.W.: Structured operational semantics and bisimulation as a congruence. Information and Computation 100(2), 202–260 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  17. Hennessy, M.C.B., Milner, R.: Algebraic laws for non-determinism and concurrency. Journal of the ACM 32(1), 137–161 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  18. Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Shannon, C., McCarthy, J. (eds.) Automata Studies, pp. 3–41. Princeton University Press, Princeton (1956)

    Google Scholar 

  19. Larsen, K.G., Liu, X.: Compositionality through an operational semantics of contexts. Journal of Logic and Computation 1(6), 761–795 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  20. Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60/61, 17–139 (2004); Originally appeared in 1981

    Article  MathSciNet  Google Scholar 

  21. de Simone, R.: Higher-level synchronising devices in Meije–SCCS. Theoretical Computer Science 37(3), 245–267 (1985)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Section Theoretical Computer Science, Vrije Universiteit Amsterdam, Amsterdam

    Wan Fokkink & Paulien de Wind

  2. Department of Software Engineering, CWI, Amsterdam

    Wan Fokkink

  3. National ICT Australia, Sydney

    Rob van Glabbeek

  4. School of Computer Science and Engineering, University of New South Wales, Sydney

    Rob van Glabbeek

Authors
  1. Wan Fokkink
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rob van Glabbeek
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Paulien de Wind
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Centre for Mathematics and Computer Science, CWI, Kruislaan 413, 1098, Amsterdam, SJ, The Netherlands

    Frank S. de Boer

  2. Leiden Institute of Advanced Computer Science, Leiden University, P.O. Box 9512, 2300, Leiden, RA, The Netherlands

    Marcello M. Bonsangue

  3. Centre Equitation, VERIMAG, 2 Avenue de Vignate, 38610, Grenoble-Gières, France

    Susanne Graf

  4. Institute of Computer Science and Applied Mathematics, Christian-Albrechts University, Kiel,Hermann-Rodewald-Straße 3, 24118, Kiel, Germany

    Willem-Paul de Roever

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fokkink, W., van Glabbeek, R., de Wind, P. (2006). Divide and Congruence: From Decomposition of Modalities to Preservation of Branching Bisimulation. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2005. Lecture Notes in Computer Science, vol 4111. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11804192_10

Download citation

  • DOI: https://doi.org/10.1007/11804192_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-36749-9

  • Online ISBN: 978-3-540-36750-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation