×

zbMATH — the first resource for mathematics

Coupled similarity: the first 32 years. (English) Zbl 07203616
Summary: 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.
Reviewer: Reviewer (Berlin)
MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
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) · Zbl 0855.68030
[2] Agha, G.; Thati, P.; Owe, O.; Krogdahl, S.; Lyche, T., An algebraic theory of actors and its application to a simple object-based language, From Object-Orientation to Formal Methods. Essays in Memory of Ole-Johan Dahl, LNCS, 26-57 (2004), Berlin: Springer, Berlin · Zbl 1278.68064
[3] Amadio, RM; Castellani, I.; Sangiorgi, D., On bisimulations for the asynchronous \(\pi \)-calculus, Theor. Comput. Sci., 195, 2, 291-324 (1998) · Zbl 0915.68009
[4] Baeten, JCM, A brief history of process algebra, Theor. Comput. Sci., 335, 2-3, 131-146 (2005) · Zbl 1080.68072
[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) · Zbl 0769.68089
[6] Brookes, SD; Hoare, CAR; Roscoe, AW, A theory of communicating sequential processes, J. ACM, 31, 3, 560-599 (1984) · Zbl 0628.68025
[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). doi: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) · Zbl 0516.68024
[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) · Zbl 1169.68539
[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) · Zbl 1028.68541
[15] Dsouza, A., Bloom, B.: On the expressive power of CCS. In: Proceedings of FSTTCS, LNCS, pp. 309-323. Springer (1995) · Zbl 1354.68194
[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) · Zbl 1065.68071
[19] Fournet, C.; Gonthier, G., A hierarchy of equivalences for asynchronous calculi, J. Log. Algebr. Program., 63, 1, 131-173 (2005) · Zbl 1066.68088
[20] Fu, Y.; Lu, H., On the expressiveness of interaction, Theor. Comput. Sci., 411, 11-13, 1387-1451 (2010) · Zbl 1191.68436
[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)
[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) · Zbl 1361.68028
[24] Gorla, D., Towards a unified approach to encodability and separation results for process calculi, Inf. Comput., 208, 9, 1031-1053 (2010) · Zbl 1209.68336
[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). 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). 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, RJ; Goltz, U., Refinement of actions and equivalence notions for concurrent systems, Acta Inf., 37, 4-5, 229-327 (2001) · Zbl 0969.68081
[29] Glabbeek, RJ; Weijland, WP, Branching time and abstraction in bisimulation semantics, J. ACM, 43, 3, 555-600 (1996) · Zbl 0882.68085
[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)
[33] Merro, M.; Sangiorgi, D., On asynchrony in name-passing calculi, Math. Struct. Comput. Sci., 14, 5, 715-767 (2004) · Zbl 1093.68026
[34] Milner, R.: Process constructors and interpretations. IFIP Congress (Invited Paper), pp. 507-514 (1986)
[35] Milner, R., Communication and Concurrency (1989), Upper Saddle River: Prentice-Hall Inc., Upper Saddle River
[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, BC, Decoding choice encodings, Inf. Comput., 163, 1, 1-59 (2000) · Zbl 1003.68080
[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 · Zbl 0941.68573
[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) · Zbl 1361.68085
[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) · Zbl 1381.68215
[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 · Zbl 0999.68528
[48] Sangiorgi, D., Introduction to Bisimulation and Coinduction (2012), New York: Cambridge University Press, New York · Zbl 1252.68008
[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 · Zbl 0770.68092
[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) · Zbl 1003.68090
[55] Voorhoeve, M.; Mauw, S., Impossible futures and determinism, Inf. Process. Lett., 80, 1, 51-58 (2001) · Zbl 1003.68090
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.