[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content

Advertisement

Springer Nature Link
Log in

Coupled similarity: the first 32 years

  • Original Article
  • Published:
Acta Informatica Aims and scope Submit manuscript

Abstract

Coupled similarity is an equivalence on (labeled) transition systems; its distinguishing power lies between (weak) bisimilarity and (may) testing equivalence. Its main feature, compared to weak bisimilarity, is an additional \(\tau \)-law that abstracts from the atomicity of internal choices among several possible branches, thus allowing for gradual commitments. The need for this \(\tau \)-law in applications was motivated by van Glabbeek and Vaandrager in 1988. Parrow and Sjödin coined the term coupled simulation in 1992 as a coinductive proof technique for the comparison of distributed (not “just” concurrent) systems, heavily exploiting gradual commitments. Over the years, coupled similarity also gained significance for the definition and analysis of the correctness of encodings, of action refinement and contraction, and of branching-time semantics for various process calculi. In this paper, we compare variants and formalizations of coupled similarity and highlight its relevance.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

Notes

  1. Parrow and Sjödin [39] and Sangiorgi [48] here just speak of “simulation,” not “weak simulation.” But, from their examples and lemmas, it seems reasonable to read a “weak” into their definitions. Nestmann and Pierce [38] explicitly requires weak simulations.

  2. Parrow and Sjödin [39] and Sangiorgi [48] claim a variant of this to hold without the assumption of shared stability. The Isabelle proof in Bisping [7] (following the construction from [48]) however needs this extra assumption and it is not obvious how to dispose of it.

  3. Also, later completeness proofs for the stronger weak congruences [1, 13] turned out neater.

  4. On \(\textsf {CCS} \) descendants, without the expressive power of \(+\), \(\equiv _{\mathrm{CS}}\) usually is a congruence. One important example is the Asynchronous Pi-Calculus [38, Prop. 2.4.4].

  5. An asynchronous simulation\({\mathscr {S}}\) for (P, Q) requires the usual (strong and weak) simulation game for \(\tau \)- and output transitions, but instead of doing the same for input transitions, the requirement becomes \((\; \overline{a} \langle z \rangle | P \;,\; \overline{a} \langle z \rangle | Q \;) \in {\mathscr {S}}\) for arbitrary messages \( \overline{a} \langle z \rangle \). Thus, inputs are not observed directly, but only indirectly via potential observable behavior after receptions.

References

  1. Aceto, L., van Glabbeek, R., Fokkink, W., Ingólfsdóttir, A.: Axiomatizing prefix iteration with silent steps. Inf. Comput. 127(1), 26–40 (1996)

    Article  MathSciNet  Google Scholar 

  2. Agha, G., Thati, P.: An algebraic theory of actors and its application to a simple object-based language. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. Essays in Memory of Ole-Johan Dahl, LNCS, vol. 2635, pp. 26–57. Springer, Berlin (2004)

    Chapter  Google Scholar 

  3. Amadio, R.M., Castellani, I., Sangiorgi, D.: On bisimulations for the asynchronous \(\pi \)-calculus. Theor. Comput. Sci. 195(2), 291–324 (1998)

    Article  MathSciNet  Google Scholar 

  4. Baeten, J.C.M.: A brief history of process algebra. Theor. Comput. Sci. 335(2–3), 131–146 (2005). https://doi.org/10.1016/j.tcs.2004.07.036

    Article  MathSciNet  MATH  Google Scholar 

  5. Bouajjani, A., Fernandez, J.C., Graf, S., Rodriguez, C., Sifakis, J.: Safety for branching time semantics. In: Albert, J.L. (Hrsg.), Monien, B. (Hrsg.), Rodríguez-Artalejo, M. (Hrsg.) (eds.) Proceedings of ICALP, LNCS, vol. 510, pp. 76–92. Springer (1991)

  6. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984)

    Article  MathSciNet  Google Scholar 

  7. Bisping, B.: Computing coupled similarity. Technische Universität Berlin, Diplomarbeit (2018). https://coupledsim.bbisping.de/bisping_computingCoupledSimilarity_thesis.pdf. Accessed 15 Nov 2019

  8. Bisping, B.: Isabelle/HOL proof and apache flink program for TACAS 2019 paper: computing coupled similarity. Figshare 3 (2019). https://doi.org/10.6084/m9.figshare.7831382.v1

  9. Bisping, B., Nestmann, U.: Computing coupled similarity. In: Proceedings of TACAS, LNCS, pp. 244–261. Springer (2019)

  10. Boudol, G.: Asynchrony and the \(\pi \)-calculus (Note)/INRIA Sophia-Antipolis version (1992). https://hal.inria.fr/inria-00076939/document. 1992 (1702). Rapport de Recherche

  11. Brookes, S.D.: On the relationship of CCS and CSP. In: Proceedings of ICALP, LNCS, pp. 83–96. Springer (1983)

  12. Derrick, J., Dongol, B., Schellhorn, G., Tofan, B., Travkin, O., Wehrheim, H.: Quiescent consistency: defining and verifying relaxed linearizability. In: FM 2014: Formal Methods-19th International Symposium, Singapore, May 12–16 2014, Proceedings. Lecture Notes in Computer Science, vol. 8442, pp. 200–214. Springer (2014). ISBN 978-3-319-06409-3

  13. Deng, Y.: A simple completeness proof for the axiomatisations of weak behavioural equivalences. Bull. EATCS 93, 207–219 (2007)

    MathSciNet  MATH  Google Scholar 

  14. Derrick, J., Wehrheim, H.: Using coupled simulations in non-atomic refinement. In: International Conference of B and Z Users, LNCS, vol. 2651, pp. 127–147. Springer (2003)

  15. Dsouza, A., Bloom, B.: On the expressive power of CCS. In: Proceedings of FSTTCS, LNCS, pp. 309–323. Springer (1995)

  16. Evrard, H., Lang, F.: Formal verification of distributed branching multiway synchronisation protocols. In: Proceedings of FMOODS/FORTE, pp. 146–160. Springer (2013)

  17. Fournet, C., Gonthier, G.: The reflexive chemical abstract machine and the join-calculus. In: Steele, Jr. G. (Hrsg.), ACM (Veranst.) Proceedings of POPL ’96 ACM, pp. 372–385. Springer (1996)

  18. Fournet, C., Gonthier, G.: The join calculus: a language for distributed mobile programming. In: Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, Sep 9–15 2000, Advanced Lectures (LNCS), vol. 2395, pp. 268–332. Springer (2002)

  19. Fournet, C., Gonthier, G.: A hierarchy of equivalences for asynchronous calculi. J. Log. Algebr. Program. 63(1), 131–173 (2005)

    Article  MathSciNet  Google Scholar 

  20. Fu, Y., Lu, H.: On the expressiveness of interaction. Theor. Comput. Sci. 411(11–13), 1387–1451 (2010). https://doi.org/10.1016/j.tcs.2009.11.011

    Article  MathSciNet  MATH  Google Scholar 

  21. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tool Technol. Transf. 15(2), 89–107 (2013)

    Article  Google Scholar 

  22. Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: Katoen, J.-P. (Hrsg.), Langerak, R. (Hrsg.), Rensink, A. (Hrsg.) ModelEd, TestEd, TrustEd—Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol. 10500, pp. 3–26. Springer (2017). ISBN 978-3-319-68269-3

  23. Gorla, D., Nestmann, U.: Full abstraction for expressiveness: history, myths and facts. Math. Struct. Comput. Sci. 26(4), 639–654 (2016). https://doi.org/10.1017/S0960129514000279

    Article  MathSciNet  MATH  Google Scholar 

  24. Gorla, D.: Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. 208(9), 1031–1053 (2010). https://doi.org/10.1016/j.ic.2010.05.002

    Article  MathSciNet  MATH  Google Scholar 

  25. Gorrieri, R., Rensink, A.: Action refinement. Version: 2001. In: Bergstra, J.A. (Hrsg.), Ponse, A. (Hrsg.), Smolka, S.A. (Hrsg.) Handbook of Process Algebra, pp. 1047–1147. North-Holland/Elsevier (2001). https://doi.org/10.1016/b978-044482830-9/50034-5. ISBN 978-0-444-82830-9

  26. Glabbeek, R.J.: A branching time model of CSP. Version: 2017. In: Gibson-Robinson, T. (Hrsg.), Hopcroft, P. (Hrsg.), Lazić, R. (Hrsg.) Concurrency, Security, and Puzzles: Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, pp. 272–293. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-51046-0_14. ISBN 978-3-319-51046-0

  27. Glabbeek, R.J.: The linear time-branching time spectrum II. In: International Conference on Concurrency Theory, pp. 66–81. Springer (1993)

  28. Glabbeek, R.J., Goltz, U.: Refinement of actions and equivalence notions for concurrent systems. Acta Inf. 37(4/5), 229–327 (2001). https://doi.org/10.1007/s002360000041

    Article  MathSciNet  MATH  Google Scholar 

  29. Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996). https://doi.org/10.1145/233551.233556

    Article  MathSciNet  MATH  Google Scholar 

  30. Hatzel, M., Wagner, C., Peters, K., Nestmann, U.: Encoding CSP into CCS. In: Proceedings of the Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, and 12th Workshop on Structural Operational Semantics, EXPRESS/SOS, pp. 61–75 (2015)

  31. Honda, K., Tokoro, M.: An object calculus for asynchronous communication. In: Tokoro, M. (Hrsg.), Nierstrasz, O. (Hrsg.), Wegner, P. (Hrsg.) Object-Based Concurrent Computing 1991, LNCS, vol. 612, pp. 133–147. Springer (1992)

  32. Knabe, F.: A distributed protocol for channel-based communication with choice. Comput. Artif. Intell. 12(5), 475–490 (1993)

    Google Scholar 

  33. Merro, M., Sangiorgi, D.: On asynchrony in name-passing calculi. Math. Struct. Comput. Sci. 14(5), 715–767 (2004). https://doi.org/10.1017/S0960129504004323

    Article  MathSciNet  MATH  Google Scholar 

  34. Milner, R.: Process constructors and interpretations. IFIP Congress (Invited Paper), pp. 507–514 (1986)

  35. Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)

    MATH  Google Scholar 

  36. Milner, R.: Skew bisimilarity, June (1995). Personal Communication

  37. Mitchell, K.: Implementations of process synchronisation and their Analysis. LFCS, University of Edinburgh, Dissertation, July (1986)

  38. Nestmann, U., Pierce, B.C.: Decoding choice encodings. Inf. Comput. 163(1), 1–59 (2000). https://doi.org/10.1006/inco.2000.2868

    Article  MathSciNet  MATH  Google Scholar 

  39. Parrow, J., Sjödin, P.: The complete axiomatization of cs-congruence. In: Enjalbert, P. (Hrsg.), Mayr, E.W. (Hrsg.), Wagner, K.W. (Hrsg.) STACS 94: 11th Annual Symposium on Theoretical Aspects of Computer Science Caen, France, Feb 24–26, 1994 Proceedings, pp. 555–568. Springer, Berlin (1994). ISBN 978-3-540-48332–8

  40. Parrow, J., Sjödin, P.: Multiway synchronization verified with coupled simulation. In: Cleaveland, W.R. (Hrsg.) CONCUR ’92: Third International Conference on Concurrency Theory Stony Brook, NY, USA, Aug 24–27, 1992 Proceedings, pp. 518-533. Springer, Berlin (1992). ISBN 978-3-540-47293-3

  41. Parrow, J.: General conditions for full abstraction. Math. Struct. Comput. Sci. 26(4), 655–657 (2016). https://doi.org/10.1017/S0960129514000280

    Article  MathSciNet  MATH  Google Scholar 

  42. Peters, K.: Translational expressiveness. TU Berlin, Dissertation (2012). http://opus.kobv.de/tuberlin/volltexte/2012/3749/. Accessed 15 Nov 2019

  43. Peters, K., Glabbeek, R.J.: Analysing and comparing encodability criteria. In: Proceedings of the Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, and 12th Workshop on Structural Operational Semantics, EXPRESS/SOS, pp. 46–60 (2015)

  44. Peters, K., van Glabbeek, R.: Analysing and comparing encodability criteria for process calculi. In: Archive of Formal Proofs. http://isa-afp.org/entries/Encodability_Process_Calculi.shtml. Formal Proof Development of the Theories Described in the Workshop Paper. Analysing and Comparing Encodability Criteria (2015). Accessed 15 Nov 2019

  45. Peters, K., Nestmann, U., Goltz, U.: On distributability in process calculi. In: Proceedings of ESOP, LNCS, vol. 7792, pp. 310–329. Springer (2013)

  46. Pierce, B.C., Turner, D.N.: Pict: a programming language based on the Pi-calculus. In: Plotkin, G. (Hrsg.), Stirling, C. (Hrsg.), Tofte, M. (Hrsg.) Proof, Language and Interaction: Essays in Honour of Robin Milner, pp. 455–494. MIT Press (2000)

  47. Rensink, A.: Action contraction. In: Proceedings of the 11th International Conference on Concurrency Theory (CONCUR ’00), pp. 290–304. Springer, Berlin (2000). ISBN 3-540-67897-2

  48. Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, New York (2012). https://doi.org/10.1017/CBO9780511777110

    Book  MATH  Google Scholar 

  49. van Glabbeek, R., Vaandrager, F.: Modular specifications in process algebra. In: Wirsing, M. (Hrsg.), Bergstra, J.A. (Hrsg.) Algebraic Methods: Theory, Tools and Applications. Algebraic Methods 1987, pp. 465–506. Springer, Berlin (1989). ISBN 978-3-540-46758-8

  50. van Glabbeek, R.: Musings on encodings and expressiveness. In: Proceedings of EXPRESS/SOS, vol. 89, (EPTCS), pp. 81–98 (2012)

  51. van Glabbeek, R., Vaandrager, F.: Modular specifications in process algebra—with curious queues/Centrum Wiskunde & Informatica (1988) (CS-R8821). CWI Report

  52. van Glabbeek, R.: Comparative concurrency semantics and refinement of actions. Centrum Wiskunde & Informatica, Dissertation (1990)

  53. van Glabbeek, R.: Comparative concurrency semantics and refinement of actions. http://theory.stanford.edu/~rvg/thesis.html. Online summary of the Ph.D. Thesis. Accessed 15 Nov 2019

  54. Voorhoeve, M., Mauw, S.: Impossible futures and determinism/Technische Universiteit Eindhoven, vol. 0014. Computing Science Reports (2000)

  55. Voorhoeve, M., Mauw, S.: Impossible futures and determinism. Inf. Process. Lett. 80(1), 51–58 (2001)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Modelle und Theorie Verteilter Systeme, Technische Universität Berlin, Berlin, Germany

    Benjamin Bisping, Uwe Nestmann & Kirstin Peters

Authors
  1. Benjamin Bisping
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Uwe Nestmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kirstin Peters
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kirstin Peters.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Bisping, B., Nestmann, U. & Peters, K. Coupled similarity: the first 32 years. Acta Informatica 57, 439–463 (2020). https://doi.org/10.1007/s00236-019-00356-4

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00236-019-00356-4

Search

Navigation