{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T10:08:33Z","timestamp":1781258913198,"version":"3.54.1"},"publisher-location":"Cham","reference-count":436,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031156281","type":"print"},{"value":"9783031156298","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-15629-8_13","type":"book-chapter","created":{"date-parts":[[2022,9,24]],"date-time":"2022-09-24T16:26:53Z","timestamp":1664036813000},"page":"213-265","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Equivalence Checking 40 Years After: A\u00a0Review of\u00a0Bisimulation Tools"],"prefix":"10.1007","author":[{"given":"Hubert","family":"Garavel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Lang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,9,7]]},"reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-540-30138-7_24","volume-title":"Computer Safety, Reliability, and Security","author":"A Aldini","year":"2004","unstructured":"Aldini, A., Bernardo, M.: An integrated view of security analysis and performance evaluation: trading QoS with covert channel bandwidth. In: Heisel, M., Liggesmeyer, P., Wittmann, S. (eds.) SAFECOMP 2004. LNCS, vol. 3219, pp. 283\u2013296. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30138-7_24"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Aldini, A., Bernardo, M.: TwoTowers 4.0: towards the integration of security analysis and performance evaluation. In: 1st International Conference on Quantitative Evaluation of Systems (QEST 2004), Enschede, The Netherlands, pp. 336\u2013337. IEEE Computer Society, September 2004","DOI":"10.1109\/QEST.2004.1348055"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L., Halbwachs, N., Wong-Toi, H.: An implementation of three algorithms for timing verification based on automata emptiness. In: Proceedings of the Real-Time Systems Symposium, Phoenix, Arizona, USA, December 1992, pp. 157\u2013166. IEEE Computer Society (1992)","DOI":"10.1109\/REAL.1992.242667"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/BFb0084802","volume-title":"CONCUR \u201992","author":"R Alur","year":"1992","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Dill, D., Wong-Toi, H.: Minimization of timed transition systems. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 340\u2013354. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0084802"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/BFb0032042","volume-title":"Automata, Languages and Programming","author":"R Alur","year":"1990","unstructured":"Alur, R., Dill, D.: Automata for modeling real-time systems. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322\u2013335. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0032042"},{"issue":"2","key":"13_CR6","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"13_CR7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)90266-6","volume":"126","author":"HR Andersen","year":"1994","unstructured":"Andersen, H.R.: Model checking and Boolean graphs. Theor. Comput. Sci. 126(1), 3\u201330 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Andersen, H.R.: Partial model checking. In: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science LICS (San Diego, California, USA), pp. 398\u2013407. IEEE Computer Society Press, June 1995","DOI":"10.1109\/LICS.1995.523274"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-319-25150-9_33","volume-title":"Theoretical Aspects of Computing - ICTAC 2015","author":"JR Andersen","year":"2015","unstructured":"Andersen, J.R., et al.: CAAL: Concurrency Workbench, Aalborg edition. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 573\u2013582. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25150-9_33"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1007\/978-3-642-31424-7_52","volume-title":"Computer Aided Verification","author":"P Armstrong","year":"2012","unstructured":"Armstrong, P., et al.: Recent developments in FDR. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 699\u2013704. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_52"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-56610-4_60","volume-title":"TAPSOFT\u201993: Theory and Practice of Software Development","author":"A Arnold","year":"1993","unstructured":"Arnold, A.: Verification and comparison of transition systems. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993. LNCS, vol. 668, pp. 121\u2013135. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56610-4_60"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Arnold, A., B\u00e9gay, D., Crubill\u00e9, P.: Construction and Analysis of Transition Systems with MEC. AMAST Series in Computing, vol. 3. World Scientific (1994)","DOI":"10.1142\/2505"},{"issue":"2\u20133","key":"13_CR13","doi-asserted-by":"publisher","first-page":"109","DOI":"10.3233\/FI-1999-402302","volume":"40","author":"A Arnold","year":"1999","unstructured":"Arnold, A., Point, G., Griffault, A., Rauzy, A.: The AltaRica formalism for describing concurrent systems. Fundam. Informaticae 40(2\u20133), 109\u2013124 (1999)","journal-title":"Fundam. Informaticae"},{"key":"13_CR14","unstructured":"Arts, T., van Langevelde, I.: Verifying a Smart Design of TCAP: A Synergetic Experience. Research Report SEN-R9910, CWI (1999)"},{"key":"13_CR15","unstructured":"Arts, T., van Langevelde, I.: How $$\\mu $$CRL supported a smart redesign of a real-life protocol. In: Gnesi, S., Latella, D. (eds.) Proceedings of the 4th International ERCIM Workshop on Formal Methods for Industrial Critical Systems (Trento, Italy), pp. 31\u201353. ERCIM, CNR, July 1999"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Arts, T., van Langevelde, I.: Correct performance of transaction capabilities. In: Valmari, A., Yakovlev, A. (eds.) Proceedings of the 2nd International Conference on Application of Concurrency to System Design (ICACSD 2001), Newcastle upon Tyne, UK, pp. 35\u201342. IEEE Computer Society, June 2001","DOI":"10.1109\/CSD.2001.981762"},{"key":"13_CR17","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0304-3975(84)90067-7","volume":"30","author":"D Austry","year":"1984","unstructured":"Austry, D., Boudol, G.: Alg\u00e8bre de Processus et Synchronisation. Theor. Comput. Sci. 30, 91\u2013131 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR18","unstructured":"Azema, P., Drira, K., Vernadat, F.: A bus instrumentation protocol specified in LOTOS. In: Quemada, J., Manas, J., V\u00e1zquez, E. (eds.) Proceedings of the 3rd International Conference on Formal Description Techniques FORTE 1990 (Madrid, Spain). North-Holland, November 1990"},{"key":"13_CR19","doi-asserted-by":"publisher","unstructured":"Az\u00e9ma, P., Vernadat, F., Lloret, J.-C.: Requirement analysis for communication protocols. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 286\u2013293. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_24","DOI":"10.1007\/3-540-52148-8_24"},{"key":"13_CR20","doi-asserted-by":"crossref","unstructured":"Baeten, J.C.M., Sangiorgi, D.: Concurrency theory: a historical perspective on coinduction and process calculi. In: Siekmann, J.H. (ed.) Computational Logic, Handbook of the History of Logic, vol. 9, pp. 399\u2013442. Elsevier (2014)","DOI":"10.1016\/B978-0-444-51624-4.50009-5"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-61474-5_57","volume-title":"Computer Aided Verification","author":"C Baier","year":"1996","unstructured":"Baier, C.: Polynomial time algorithms for testing probabilistic bisimulation and simulation. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 50\u201361. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_57"},{"key":"13_CR22","unstructured":"Baray, F., Wodey, P.: Verification in the codesign process by means of LOTOS based model-checking. In: Gnesi, S., Schieferdecker, I., Rennoch, A. (eds.) Proceedings of the 5th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2000), Berlin, Germany, pp. 87\u2013108. GMD Report 91, Berlin, April 2000"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/3-540-68061-6_32","volume-title":"Computer Performance Evaluation","author":"F Bause","year":"1998","unstructured":"Bause, F., Buchholz, P., Kemper, P.: A toolbox for functional and quantitative analysis of DEDS. In: Puigjaner, R., Savino, N.N., Serra, B. (eds.) TOOLS 1998. LNCS, vol. 1469, pp. 356\u2013359. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-68061-6_32"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J Bengtsson","year":"1996","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL\u2014a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232\u2013243. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020949"},{"key":"13_CR25","unstructured":"Benslimane, A., Abouaissa, A.: XTP specification and validation with LOTOS. In: Proceedings of the Western MultiConference WMC 1998, Communication Networks and Distributed Systems Modeling and Simulation CNDS 1998 (San Diego, California, USA). Society for Computer Simulation International, January 1998"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1007\/978-3-540-31980-1_42","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Bergamini","year":"2005","unstructured":"Bergamini, D., Descoubes, N., Joubert, C., Mateescu, R.: BISIMULATOR: a modular tool for on-the-fly equivalence checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 581\u2013585. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_42"},{"issue":"1\u20133","key":"13_CR27","first-page":"109","volume":"60","author":"JA Bergstra","year":"1984","unstructured":"Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Comput. 60(1\u20133), 109\u2013137 (1984)","journal-title":"Inf. Comput."},{"key":"13_CR28","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(85)90088-X","volume":"37","author":"JA Bergstra","year":"1985","unstructured":"Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theor. Comput. Sci. 37, 77\u2013121 (1985)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20133","key":"13_CR29","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1016\/S0304-3975(03)00277-9","volume":"309","author":"JA Bergstra","year":"2003","unstructured":"Bergstra, J.A., Ponse, A., van der Zwaag, M.: Branching time and orthogonal bisimulation equivalence. Theor. Comput. Sci. 309(1\u20133), 313\u2013355 (2003)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"13_CR30","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/S0164-1212(97)00057-5","volume":"39","author":"C Bernardeschi","year":"1997","unstructured":"Bernardeschi, C., Fantechi, A., Gnesi, S.: An industrial application for the JACK environment. J. Syst. Softw. 39(3), 249\u2013264 (1997)","journal-title":"J. Syst. Softw."},{"issue":"2","key":"13_CR31","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1023\/A:1008645826258","volume":"12","author":"C Bernardeschi","year":"1998","unstructured":"Bernardeschi, C., Fantechi, A., Gnesi, S., Larosa, S., Mongardi, G., Romano, D.: A formal verification environment for railway signaling system design. Formal Methods Syst. Des. 12(2), 139\u2013161 (1998)","journal-title":"Formal Methods Syst. Des."},{"key":"13_CR32","unstructured":"Bernardo, M., Bravetti, M.: Functional and performance modeling and analysis of token ring using EMPA. In: Degano, P., Vaccaro, U., Pirillo, G. (eds.) Proceedings of the 6th Italian Conference on Theoretical Computer Science (1998)"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/3-540-63165-8_192","volume-title":"Automata, Languages and Programming","author":"M Bernardo","year":"1997","unstructured":"Bernardo, M.: An algebra-based method to associate rewards with EMPA terms. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 358\u2013368. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63165-8_192"},{"key":"13_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/3-540-46429-8_34","volume-title":"Computer Performance Evaluation.Modelling Techniques and Tools","author":"M Bernardo","year":"2000","unstructured":"Bernardo, M.: Implementing symbolic models for value passing in TwoTowers. In: Haverkort, B.R., Bohnenkamp, H.C., Smith, C.U. (eds.) TOOLS 2000. LNCS, vol. 1786, pp. 370\u2013373. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46429-8_34"},{"key":"13_CR35","doi-asserted-by":"crossref","unstructured":"Bernardo, M., Cleaveland, R., Sims, S., Stewart, W.: TwoTowers: a tool integrating functional and performance analysis of concurrent systems. In: Budkowski, S., Cavalli, A.R., Najm, E. (eds.) Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE XI\/PSTV XVIII 1998, IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XI) and Protocol Specification, Testing and Verification (PSTV XVIII), Paris, France. IFIP Conference Proceedings, vol. 135, pp. 457\u2013467. Kluwer, November 1998","DOI":"10.1007\/978-0-387-35394-4_28"},{"key":"13_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-60222-4_95","volume-title":"Parallel Computing Technologies","author":"A Bianchi","year":"1995","unstructured":"Bianchi, A., Coluccini, S., Degano, P., Priami, C.: An efficient verifier of truly concurrent properties. In: Malyshkin, V. (ed.) PaCT 1995. LNCS, vol. 964, pp. 36\u201350. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60222-4_95"},{"key":"13_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-319-63121-9_9","volume-title":"Models, Algorithms, Logics and Tools","author":"S Biewer","year":"2017","unstructured":"Biewer, S., Freiberger, F., Held, P.L., Hermanns, H.: Teaching academic concurrency to amazing students. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 170\u2013195. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63121-9_9"},{"key":"13_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-44585-4_23","volume-title":"Computer Aided Verification","author":"S Blom","year":"2001","unstructured":"Blom, S., Fokkink, W., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J.: $$\\mu $$CRL: a toolset for analysing algebraic specifications. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 250\u2013254. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_23"},{"key":"13_CR39","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1016\/S1571-0661(04)80827-2","volume":"80","author":"S Blom","year":"2003","unstructured":"Blom, S., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J.: New developments around the mCRL tool set. Electron. Notes Theor. Comput. Sci. 80, 284\u2013288 (2003)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"4","key":"13_CR40","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1016\/S1571-0661(05)80390-1","volume":"68","author":"S Blom","year":"2002","unstructured":"Blom, S., Orzan, S.: A distributed algorithm for strong bisimulation reduction of state spaces. Electron. Notes Theor. Comput. Sci. 68(4), 523\u2013538 (2002)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1","key":"13_CR41","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S1571-0661(05)80099-4","volume":"89","author":"S Blom","year":"2003","unstructured":"Blom, S., Orzan, S.: Distributed branching bisimulation reduction of state spaces. Electron. Notes Theor. Comput. Sci. 89(1), 99\u2013113 (2003)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"13_CR42","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/S1571-0661(04)80812-0","volume":"80","author":"S Blom","year":"2003","unstructured":"Blom, S., Orzan, S.: Distributed state space minimization. Electron. Notes Theor. Comput. Sci. 80, 109\u2013123 (2003)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1","key":"13_CR43","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/s10009-004-0159-4","volume":"7","author":"S Blom","year":"2005","unstructured":"Blom, S., Orzan, S.: A distributed algorithm for strong bisimulation reduction of state spaces. Softw. Tools Technol. Transfer 7(1), 74\u201386 (2005)","journal-title":"Softw. Tools Technol. Transfer"},{"issue":"3","key":"13_CR44","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/s10009-004-0185-2","volume":"7","author":"S Blom","year":"2005","unstructured":"Blom, S., Orzan, S.: Distributed state space minimization. Softw. Tools Technol. Transfer 7(3), 280\u2013291 (2005)","journal-title":"Softw. Tools Technol. Transfer"},{"key":"13_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1007\/3-540-45657-0_50","volume-title":"Computer Aided Verification","author":"S Blom","year":"2002","unstructured":"Blom, S., van de Pol, J.: State space reduction by proving confluence. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 596\u2013609. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_50"},{"key":"13_CR46","doi-asserted-by":"crossref","unstructured":"Blom, S., van de Pol, J.: Distributed branching bisimulation minimization by inductive signatures. In: Brim, L., van de Pol, J. (eds.) Proceedings 8th International Workshop on Parallel and Distributed Methods in Verification (PDMC 2009), Eindhoven, The Netherlands. EPTCS, vol. 14, pp. 32\u201346, November 2009","DOI":"10.4204\/EPTCS.14.3"},{"key":"13_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-14295-6_31","volume-title":"Computer Aided Verification","author":"S Blom","year":"2010","unstructured":"Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354\u2013359. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_31"},{"key":"13_CR48","doi-asserted-by":"crossref","unstructured":"Blute, R., Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. In: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, pp. 149\u2013158. IEEE Computer Society, June 1997","DOI":"10.7146\/brics.v4i4.18783"},{"key":"13_CR49","unstructured":"Bolognesi, T., Caneve, M.: SQUIGGLES: a tool for the analysis of LOTOS specifications. In: Turner, K.J. (ed.) Proceedings of the 1st International Conference on Formal Description Techniques (FORTE 1988), Stirling, Scotland, pp. 201\u2013216. North-Holland, September 1988"},{"key":"13_CR50","unstructured":"Bolognesi, T., Caneve, M.: Equivalence verification: theory, algorithms, and a tool. In: van Eijk, P., Vissers, C.A., Diaz, M. (eds.) The Formal Description Technique LOTOS, pp. 303\u2013326. North-Holland (1989)"},{"key":"13_CR51","doi-asserted-by":"crossref","unstructured":"Borgstr\u00f6m, J., Gutkovas, R., Rodhe, I., Victor, B.: A parametric tool for applied process calculi. In: Carmona, J., Lazarescu, M.T., Pietkiewicz-Koutny, M. (eds.) 13th International Conference on Application of Concurrency to System Design, ACSD 2013, Barcelona, Spain, pp. 180\u2013185. IEEE Computer Society, July 2013","DOI":"10.1109\/ACSD.2013.22"},{"key":"13_CR52","doi-asserted-by":"crossref","unstructured":"Borgstr\u00f6m, J., Gutkovas, R., Rodhe, I., Victor, B.: The psi-calculi workbench: a generic tool for applied process calculi. ACM Trans. Embed. Comput. Syst. 14(1), 9:1\u20139:25 (2015)","DOI":"10.1145\/2682570"},{"key":"13_CR53","unstructured":"B\u00f8rjesson, A., Larsen, K.G., Skou, A.: Generality in design and compositional verification using TAV. In: Diaz, M., Groz, R. (eds.) Proceedings of the IFIP TC6\/WG6.1 5th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE 1992), Perros-Guirec, France, 13\u201316 October 1992. IFIP Transactions, vol. C-10, pp. 449\u2013464. North-Holland, September 1992"},{"issue":"3","key":"13_CR54","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/BF01384499","volume":"6","author":"A B\u00f8rjesson","year":"1995","unstructured":"B\u00f8rjesson, A., Larsen, K.G., Skou, A.: Generality in design and compositional verification using TAV. Formal Methods Syst. Des. 6(3), 239\u2013258 (1995)","journal-title":"Formal Methods Syst. Des."},{"key":"13_CR55","unstructured":"Bos, V.: ChiSigma Manual (2002). ResearchGate"},{"key":"13_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-54233-7_126","volume-title":"Automata, Languages and Programming","author":"A Bouajjani","year":"1991","unstructured":"Bouajjani, A., Fernandez, J.C., Graf, S., Rodriguez, C., Sifakis, J.: Safety for branching time semantics. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) ICALP 1991. LNCS, vol. 510, pp. 76\u201392. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-54233-7_126"},{"key":"13_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/BFb0023733","volume-title":"Computer-Aided Verification","author":"A Bouajjani","year":"1991","unstructured":"Bouajjani, A., Fernandez, J.-C., Halbwachs, N.: Minimal model generation. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 197\u2013203. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0023733"},{"key":"13_CR58","unstructured":"Bouali, A.: Weak and Branching Bisimulation in FcTool. Research Report 1575, INRIA (1992)"},{"key":"13_CR59","unstructured":"Bouali, A.: XEVE: An ESTEREL Verification Environment (Version v1_3). Technical Report 214, INRIA (1997)"},{"key":"13_CR60","unstructured":"Bouali, A., Gnesi, S., Larosa, S.: The Integration Project for the JACK Environment. Research Report CS-R9443, CWI (1994)"},{"key":"13_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-61474-5_98","volume-title":"Computer Aided Verification","author":"A Bouali","year":"1996","unstructured":"Bouali, A., Ressouche, A., Roy, V., de Simone, R.: The FC2TOOLS set. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 441\u2013445. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_98"},{"key":"13_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1007\/BFb0014350","volume-title":"Algebraic Methodology and Software Technology","author":"A Bouali","year":"1996","unstructured":"Bouali, A., Ressouche, A., Roy, V., de Simone, R.: The FC2TOOLS set. In: Wirsing, M., Nivat, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 595\u2013598. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0014350"},{"key":"13_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/3-540-61042-1_57","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Bouali","year":"1996","unstructured":"Bouali, A., Ressouche, A., Roy, V., de Simone, R.: The FC2TOOLS set (tool demonstration). In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, p. 396. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61042-1_57"},{"key":"13_CR64","unstructured":"Bouali, A., Ressouche, A., Roy, V., de Simone, R.: The FCTOOLS User Manual (Version 1.0). Technical Report RT-0191, INRIA, June 1996"},{"key":"13_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-56496-9_9","volume-title":"Computer Aided Verification","author":"A Bouali","year":"1993","unstructured":"Bouali, A., de Simone, R.: Symbolic bisimulation minimisation. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 96\u2013108. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56496-9_9"},{"key":"13_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-52148-8_1","volume-title":"Automatic Verification Methods for Finite State Systems","author":"G Boudol","year":"1990","unstructured":"Boudol, G., Roy, V., de Simone, R., Vergamini, D.: Process calculi, from theory to practice: verification tools. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 1\u201310. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_1"},{"key":"13_CR67","unstructured":"Boudol, G., de Simone, R., Vergamini, D.: Experiment with AUTO and AUTOGRAPH on a simple case of sliding window protocol. Research Report 870, INRIA (1988)"},{"issue":"3","key":"13_CR68","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/s00165-016-0366-2","volume":"28","author":"A Boulgakov","year":"2016","unstructured":"Boulgakov, A., Gibson-Robinson, T., Roscoe, A.W.: Computing maximal weak and other bisimulations. Formal Aspects Comput. 28(3), 381\u2013407 (2016)","journal-title":"Formal Aspects Comput."},{"key":"13_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Computer Aided Verification","author":"M Bozga","year":"1998","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: KRONOS: a model-checking tool for real-time systems. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 546\u2013550. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028779"},{"key":"13_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/BFb0055357","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"M Bozga","year":"1998","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: KRONOS: a model-checking tool for real-time systems. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 298\u2013302. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055357"},{"issue":"1\u20132","key":"13_CR71","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/s100090050012","volume":"1","author":"M Bozga","year":"1997","unstructured":"Bozga, M., Fernandez, J.C., Kerbrat, A., Mounier, L.: Protocol verification with the ALDEBARAN toolset. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 166\u2013184 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"13_CR72","unstructured":"Briais, S.: ABC User\u2019s Guide (2005). http:\/\/sbriais.free.fr\/tools\/abc\/abc_ug.ps"},{"key":"13_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/3-540-44667-2_5","volume-title":"Lectures on Formal Methods and PerformanceAnalysis","author":"E Brinksma","year":"2001","unstructured":"Brinksma, E., Hermanns, H.: Process algebra and Markov chains. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000. LNCS, vol. 2090, pp. 183\u2013231. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44667-2_5"},{"issue":"3","key":"13_CR74","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"SD Brookes","year":"1984","unstructured":"Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560\u2013599 (1984)","journal-title":"J. ACM"},{"key":"13_CR75","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35(8) (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"13_CR76","doi-asserted-by":"crossref","unstructured":"Buchholz, P.: Equivalence relations for stochastic automata networks. In: Stewart, W.J. (ed.) Computation with Markov Chains: Proceedings of the 2nd International Workshop on the Numerical Solution of Markov Chains, pp. 197\u2013216. Kluwer (1995)","DOI":"10.1007\/978-1-4615-2241-6_13"},{"key":"13_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/3-540-48683-6_41","volume-title":"Computer Aided Verification","author":"P Buchholz","year":"1999","unstructured":"Buchholz, P., Kemper, P.: A toolbox for the analysis of discrete event dynamic systems. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 483\u2013486. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_41"},{"key":"13_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-49059-0_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Buchholz","year":"1999","unstructured":"Buchholz, P., Kemper, P.: Modular state level analysis of distributed systems techniques and tool support. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 420\u2013434. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_29"},{"issue":"4","key":"13_CR79","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1134\/S0361768811040013","volume":"37","author":"PE Bulychev","year":"2011","unstructured":"Bulychev, P.E.: Game-theoretic simulation checking tool. Program. Comput. Softw. 37(4), 200\u2013209 (2011)","journal-title":"Program. Comput. Softw."},{"key":"13_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-030-17465-1_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Bunte","year":"2019","unstructured":"Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21\u201339. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_2"},{"key":"13_CR81","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-48387-X_20","volume-title":"Parallel Computing Technologies","author":"AV Bystrov","year":"1999","unstructured":"Bystrov, A.V., Virbitskaite, I.B.: Implementing model checking and equivalence checking for time petri nets by the RT-MEC tool. In: Malyshkin, V. (ed.) PaCT 1999. LNCS, vol. 1662, pp. 194\u2013199. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48387-X_20"},{"key":"13_CR82","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-89287-8_4","volume":"1","author":"F Calzolai","year":"2008","unstructured":"Calzolai, F., De Nicola, R., Loreti, M., Tiezzi, F.: TAPAs: a tool for the analysis of process algebras. Trans. Petri Nets Other Model. Concurr. 1, 54\u201370 (2008)","journal-title":"Trans. Petri Nets Other Model. Concurr."},{"key":"13_CR83","doi-asserted-by":"crossref","unstructured":"Camurati, P., Corno, F., Prinetto, P.: An efficient tool for system-level verification of behaviors and temporal properties. In: Proceedings of the European Design Automation Conference (EURO-DAC 1993), Hamburg, Germany, pp. 124\u2013129. IEEE Computer Society, September 1993","DOI":"10.1109\/EURDAC.1993.410626"},{"key":"13_CR84","series-title":"Lecture Notes in Control and Information Sciences","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/BFb0042304","volume-title":"Discrete Event Systems: Models and Applications","author":"V Carchiolo","year":"1987","unstructured":"Carchiolo, V., Faro, A.: A tool for the automated verification of ECCS specifications of OSI protocols. In: Varaiya, P., Kurzhanski, A.B. (eds.) Discrete Event Systems: Models and Applications. LNCIS, pp. 57\u201368. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/BFb0042304"},{"key":"13_CR85","doi-asserted-by":"crossref","unstructured":"Cerans, K., Godskesen, J.C., Larsen, K.G.: Timed Modal Specification - Theory and Tools. Research Report RS-97-11, BRICS (1997)","DOI":"10.7146\/brics.v4i11.18802"},{"key":"13_CR86","doi-asserted-by":"crossref","unstructured":"Chehaibar, G., Garavel, H., Mounier, L., Tawbi, N., Zulian, F.: Specification and verification of the PowerScale bus arbitration protocol: an industrial experiment with LOTOS. In: Gotzhein, R., Bredereke, J. (eds.) Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification (FORTE\/PSTV 1996), Kaiserslautern, Germany, pp. 435\u2013450. Chapman & Hall, October 1996. Full version available as INRIA Research Report RR-2958","DOI":"10.1007\/978-0-387-35079-0_28"},{"key":"13_CR87","doi-asserted-by":"crossref","unstructured":"Chen, L., Ebrahimi, M., Tahoori, M.B.: Quantitative evaluation of register vulnerabilities in RTL control paths. In: Natale, G.D. (ed.) Proceedings of the 19th IEEE European Test Symposium (ETS 2014), Paderborn, Germany, pp. 1\u20132. IEEE, May 2014","DOI":"10.1109\/ETS.2014.6847837"},{"key":"13_CR88","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-540-74407-8_9","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"T Chen","year":"2007","unstructured":"Chen, T., Ploeger, B., van de Pol, J., Willemse, T.A.C.: Equivalence checking for infinite systems using parameterized Boolean equation systems. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 120\u2013135. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74407-8_9"},{"key":"13_CR89","doi-asserted-by":"crossref","unstructured":"Cheng, Y.P., Cheng, Y.R., Wang, H.Y.: ARCATS: a scalable compositional analysis tool suite. In: Haddad, H. (ed.) Proceedings of the 2006 ACM Symposium on Applied Computing (SAC 2006), Dijon, France, pp. 1852\u20131853. ACM, April 2006","DOI":"10.1145\/1141277.1141713"},{"key":"13_CR90","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11812128_21","volume-title":"Implementation and Application of Automata","author":"Y-P Cheng","year":"2006","unstructured":"Cheng, Y.-P., Wang, H.-Y., Cheng, Y.-R.: On-the-fly branching bisimulation minimization for compositional analysis. In: Ibarra, O.H., Yen, H.-C. (eds.) CIAA 2006. LNCS, vol. 4094, pp. 219\u2013229. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11812128_21"},{"key":"13_CR91","doi-asserted-by":"crossref","unstructured":"Cheung, S.C., Kramer, J.: Enhancing compositional reachability analysis with context constraints. In: Proceedings of the 1st ACM SIGSOFT International Symposium on the Foundations of Software Engineering (Los Angeles, CA, USA), pp. 115\u2013125. ACM Press, December 1993","DOI":"10.1145\/167049.167071"},{"key":"13_CR92","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/3-540-63531-9_17","volume-title":"Software Engineering \u2014 ESEC\/FSE\u201997","author":"SC Cheung","year":"1997","unstructured":"Cheung, S.C., Giannakopoulou, D., Kramer, J.: Verification of liveness properties using compositional reachability analysis. In: Jazayeri, M., Schauer, H. (eds.) ESEC\/SIGSOFT FSE 1997. LNCS, vol. 1301, pp. 227\u2013243. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63531-9_17"},{"key":"13_CR93","unstructured":"Clarke, D.: VERSA: Verification, Execution and Rewrite System for ASCR. Technical Report MS-CIS-95-34, University of Pennsylvania (1995)"},{"key":"13_CR94","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/3-540-61474-5_89","volume-title":"Computer Aided Verification","author":"D Clarke","year":"1996","unstructured":"Clarke, D., Ben-Abdallah, H., Lee, I., Xie, H.-L., Sokolsky, O.: XVERSA: an integrated graphical and textual toolset for the specification and analysis of resource-bound real-time systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 402\u2013405. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_89"},{"key":"13_CR95","unstructured":"Clarke, D., Lee, I.: VERSA: a tool for analyzing resource-bound real-time systems. J. Comput. Softw. Eng. 3(2) (1995)"},{"key":"13_CR96","unstructured":"Clarke, D., Lee, I., Xie, H.L.: VERSA: A Tool for the Specification and Analysis of Resource-Bound Real-Time Systems. Technical Report MS-CIS-93-77, University of Pennsylvania (1993)"},{"issue":"11","key":"13_CR97","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1592761.1592781","volume":"52","author":"EM Clarke","year":"2009","unstructured":"Clarke, E.M., Emerson, E.A., Sifakis, J.: Model checking: algorithmic verification and debugging. Commun. ACM 52(11), 74\u201384 (2009)","journal-title":"Commun. ACM"},{"key":"13_CR98","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/BFb0023750","volume-title":"Computer-Aided Verification","author":"R Cleaveland","year":"1991","unstructured":"Cleaveland, R.: On automatically explaining bisimulation inequivalence. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 364\u2013372. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0023750"},{"key":"13_CR99","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/3-540-56883-2_8","volume-title":"Functional Programming, Concurrency, Simulation and Automated Reasoning","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R.: Analyzing concurrent systems using the Concurrency Workbench. In: Lauer, P.E. (ed.) Functional Programming, Concurrency, Simulation and Automated Reasoning. LNCS, vol. 693, pp. 129\u2013144. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56883-2_8"},{"key":"13_CR100","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Gada, J.N., Lewis, P.M., Smolka, S.A., Sokolsky, O., Zhang, S.: The Concurrency Factory - practical tools for specification, simulation, verification, and implementation of concurrent systems. In: Blelloch, G.E., Chandy, K.M., Jagannathan, S. (eds.) Proceedings of the DIMACS Workshop on Specification of Parallel Algorithms, Princeton, New Jersey, USA. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 18, pp. 75\u201389. DIMACS\/AMS, May 1994","DOI":"10.1090\/dimacs\/018\/06"},{"key":"13_CR101","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/3-540-52148-8_2","volume-title":"Automatic Verification Methods for Finite State Systems","author":"R Cleaveland","year":"1990","unstructured":"Cleaveland, R., Hennessy, M.: Testing equivalence as a bisimulation equivalence. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 11\u201323. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_2"},{"key":"13_CR102","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/3-540-61474-5_88","volume-title":"Computer Aided Verification","author":"R Cleaveland","year":"1996","unstructured":"Cleaveland, R., Lewis, P.M., Smolka, S.A., Sokolsky, O.: The Concurrency Factory: a development environment for concurrent systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 398\u2013401. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_88"},{"key":"13_CR103","unstructured":"Cleaveland, R., Li, T., Sims, S.: The Concurrency Workbench of the New Century (Version 1.2) - User\u2019s Manual, July 2000. State University of New York at Stony Brook"},{"key":"13_CR104","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: A semantics based verification tool for finite state systems. In: Brinksma, E., Scollo, G., Vissers, C.A. (eds.) Proceedings of the 9th International Symposium on Protocol Specification, Testing and Verification (PSTV 1989), Enschede, The Netherlands, pp. 287\u2013302. North-Holland (1989)"},{"key":"13_CR105","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-52148-8_3","volume-title":"Automatic Verification Methods for Finite State Systems","author":"R Cleaveland","year":"1990","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: The Concurrency Workbench. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 24\u201337. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_3"},{"issue":"1","key":"13_CR106","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: The Concurrency Workbench: a semantics-based tool for the verification of concurrent systems. ACM Trans. Program. Lang. Syst. 15(1), 36\u201372 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR107","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Sims, S.: The Concurrency Workbench of North Carolina User\u2019s manual (version 1.0) (1996)","DOI":"10.1007\/3-540-61474-5_87"},{"key":"13_CR108","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/3-540-61474-5_87","volume-title":"Computer Aided Verification","author":"R Cleaveland","year":"1996","unstructured":"Cleaveland, R., Sims, S.: The NCSU Concurrency Workbench. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 394\u2013397. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_87"},{"key":"13_CR109","unstructured":"Cleaveland, R., Sims, S.: Generic tools for verifying concurrent systems. In: Proceedings of the 1998 ARO\/ONR\/NSF\/DARPA Monterey Workshop on Engineering Automation for Computer Based Systems, pp. 38\u201346 (1999)"},{"issue":"1","key":"13_CR110","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0167-6423(01)00033-8","volume":"42","author":"R Cleaveland","year":"2002","unstructured":"Cleaveland, R., Sims, S.: Generic tools for verifying concurrent systems. Sci. Comput. Program. 42(1), 39\u201347 (2002)","journal-title":"Sci. Comput. Program."},{"key":"13_CR111","doi-asserted-by":"crossref","unstructured":"Cornejo, M.A., Garavel, H., Mateescu, R., de Palma, N.: Specification and verification of a dynamic reconfiguration protocol for agent-based applications. In: Laurentowski, A., Kosinski, J., Mossurska, Z., Ruchala, R. (eds.) Proceedings of the 3rd IFIP WG 6.1 International Working Conference on Distributed Applications and Interoperable Systems (DAIS 2001), Krakow, Poland, pp. 229\u2013242. Kluwer Academic Publishers, September 2001. Full version available as INRIA Research Report RR-4222","DOI":"10.1007\/0-306-47005-5_20"},{"key":"13_CR112","unstructured":"Coste, N.: Vers la pr\u00e9diction de performance de mod\u00e8les compositionnels dans les architectures GALS. Ph.D. thesis, Universit\u00e9 de Grenoble, June 2010"},{"key":"13_CR113","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-16561-0_18","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"N Coste","year":"2010","unstructured":"Coste, N., Garavel, H., Hermanns, H., Lang, F., Mateescu, R., Serwe, W.: Ten years of performance evaluation for concurrent systems using CADP. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 128\u2013142. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16561-0_18"},{"key":"13_CR114","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-02658-4_18","volume-title":"Computer Aided Verification","author":"N Coste","year":"2009","unstructured":"Coste, N., Hermanns, H., Lantreibecq, E., Serwe, W.: Towards performance prediction of compositional models in industrial GALS designs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 204\u2013218. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_18"},{"key":"13_CR115","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-36742-7_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Cranen","year":"2013","unstructured":"Cranen, S., et al.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 199\u2013213. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_15"},{"key":"13_CR116","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-540-85361-9_25","volume-title":"CONCUR 2008 - Concurrency Theory","author":"P Crouzen","year":"2008","unstructured":"Crouzen, P., Hermanns, H., Zhang, L.: On the minimisation of acyclic models. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 295\u2013309. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85361-9_25"},{"key":"13_CR117","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-19811-3_9","volume-title":"Fundamental Approaches to Software Engineering","author":"P Crouzen","year":"2011","unstructured":"Crouzen, P., Lang, F.: Smart reduction. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 111\u2013126. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19811-3_9"},{"issue":"2","key":"13_CR118","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/0304-3975(94)00169-J","volume":"138","author":"JW Davies","year":"1995","unstructured":"Davies, J.W., Schneider, S.A.: A brief history of timed CSP. Theor. Comput. Sci. 138(2), 243\u2013271 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR119","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/BFb0020947","volume-title":"Hybrid Systems III","author":"C Daws","year":"1996","unstructured":"Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool Kronos. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 208\u2013219. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0020947"},{"key":"13_CR120","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"R De Nicola","year":"1984","unstructured":"De Nicola, R., Hennessy, M.C.B.: Testing equivalences for processes. Theor. Comput. Sci. 34, 83\u2013133 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR121","doi-asserted-by":"crossref","unstructured":"De Nicola, R., Inverardi, P., Nesi, M.: Equational reasoning about LOTOS specifications: a rewriting approach. In: Proceedings of the 6th International Workshop on Software Specification and Design, pp. 148\u2013155 (1991)","DOI":"10.1109\/IWSSD.1991.213066"},{"key":"13_CR122","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/3-540-53479-2_17","volume-title":"Semantics of Systems of Concurrent Processes","author":"R De Nicola","year":"1990","unstructured":"De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407\u2013419. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-53479-2_17"},{"key":"13_CR123","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-60385-9_15","volume-title":"Correct Hardware Design and Verification Methods","author":"R De Nicola","year":"1995","unstructured":"De Nicola, R., Fantechi, A., Gnesi, S., Larosa, S., Ristori, G.: Verifying hardware components with JACK. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 246\u2013260. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60385-9_15"},{"key":"13_CR124","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-52148-8_5","volume-title":"Automatic Verification Methods for Finite State Systems","author":"R De Nicola","year":"1990","unstructured":"De Nicola, R., Inverardi, P., Nesi, M.: Using the axiomatic presentation of behavioural equivalences for manipulating CCS specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 54\u201367. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_5"},{"key":"13_CR125","doi-asserted-by":"crossref","unstructured":"De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation (extended abstract). In: Proceedings of the 4th Annual Symposium on Logic in Computer Science (LICS 1989), Pacific Grove, California, USA, pp. 118\u2013129. IEEE Computer Society (1990)","DOI":"10.1109\/LICS.1990.113739"},{"issue":"2","key":"13_CR126","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R De Nicola","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458\u2013487 (1995)","journal-title":"J. ACM"},{"key":"13_CR127","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-642-35873-9_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C Dehnert","year":"2013","unstructured":"Dehnert, C., Katoen, J.-P., Parker, D.: SMT-based bisimulation minimisation of Markov models. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 28\u201347. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_5"},{"key":"13_CR128","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-540-71209-1_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Derisavi","year":"2007","unstructured":"Derisavi, S.: A symbolic algorithm for optimal Markov chain lumping. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 139\u2013154. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_13"},{"key":"13_CR129","doi-asserted-by":"crossref","unstructured":"Derisavi, S.: Signature-based symbolic algorithm for optimal Markov chain lumping. In: Proceedings of the 4th International Conference on the Quantitative Evaluation of Systems (QEST 2007), Edinburgh, Scotland, UK, pp. 141\u2013150. IEEE Computer Society, September 2007","DOI":"10.1109\/QEST.2007.27"},{"key":"13_CR130","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-662-49674-9_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T van Dijk","year":"2016","unstructured":"van Dijk, T., van de Pol, J.: Multi-core symbolic bisimulation minimisation. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 332\u2013348. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_19"},{"issue":"6","key":"13_CR131","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/s10009-016-0433-2","volume":"19","author":"T van Dijk","year":"2017","unstructured":"van Dijk, T., van de Pol, J.: SYLVAN: multi-core framework for decision diagrams. Int. J. Softw. Tools Technol. Transf. 19(6), 675\u2013696 (2017)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"13_CR132","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-319-63516-3_13","volume-title":"Handbook of Parallel Constraint Reasoning","author":"T van Dijk","year":"2018","unstructured":"van Dijk, T., van de Pol, J.: Multi-core decision diagrams. In: Hamadi, Y., Sais, L. (eds.) Handbook of Parallel Constraint Reasoning, pp. 509\u2013545. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-63516-3_13"},{"issue":"2","key":"13_CR133","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/s10009-017-0468-z","volume":"20","author":"T van Dijk","year":"2018","unstructured":"van Dijk, T., van de Pol, J.: Multi-core symbolic bisimulation minimisation. Int. J. Softw. Tools Technol. Transf. 20(2), 157\u2013177 (2018)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"13_CR134","unstructured":"Doumenc, G., Madelaine, E.: Une traduction de PLOTOS en MEIJE. Research Report RR-0938, INRIA (1988)"},{"key":"13_CR135","unstructured":"Doumenc, G., Madelaine, E., De Simone, R.: Proving Process Calculi Translations in ECRINS: The pureLOTOS -$$>$$ MEIJE Example. Research Report RR-1192, INRIA (1990)"},{"key":"13_CR136","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1016\/S1571-0661(04)80547-4","volume":"67","author":"A Dovier","year":"2002","unstructured":"Dovier, A., Gentilini, R., Piazza, C., Policriti, A.: Rank-based symbolic bisimulation (and model checking). Electron. Notes Theor. Comput. Sci. 67, 166\u2013183 (2002)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"13_CR137","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/3-540-44585-4_8","volume-title":"Computer Aided Verification","author":"A Dovier","year":"2001","unstructured":"Dovier, A., Piazza, C., Policriti, A.: A fast bisimulation algorithm. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 79\u201390. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_8"},{"issue":"1\u20133","key":"13_CR138","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/S0304-3975(03)00361-X","volume":"311","author":"A Dovier","year":"2004","unstructured":"Dovier, A., Piazza, C., Policriti, A.: An efficient algorithm for computing bisimulation equivalence. Theor. Comput. Sci. 311(1\u20133), 221\u2013256 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR139","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-15375-4_3","volume-title":"CONCUR 2010 - Concurrency Theory","author":"C Eisentraut","year":"2010","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: Concurrency and composition in a stochastic world. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 21\u201339. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_3"},{"key":"13_CR140","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-55179-4_20","volume-title":"Computer Aided Verification","author":"R Enders","year":"1992","unstructured":"Enders, R., Filkorn, T., Taubner, D.: Generating BDDs for symbolic model checking in CCS. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 203\u2013213. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55179-4_20"},{"key":"13_CR141","unstructured":"Erdogmus, H.: Verifying semantic relations in SPIN. In: Proceedings of the 1st SPIN Workshop (Montr\u00e9al, Qu\u00e9bec) (1995)"},{"key":"13_CR142","unstructured":"Erdogmus, H., de B. Johnston, R., Cleary, C.: Formal verification based on relation checking in SPIN: a case study. In: Proceedings of the 1st Workshop on Formal Methods in Software Practice (San Diego, California, USA) (1995)"},{"key":"13_CR143","unstructured":"Ernberg, P., Fredlund, L., Jonsson, B.: Specification and Validation of a Simple Overtaking Protocol using LOTOS. T 90006, Swedish Institute of Computer Science, Kista, Sweden, October 1990"},{"key":"13_CR144","unstructured":"Ernberg, P., Fredlund, L.A.: Identifying Some Bottlenecks of the Concurrency Workbench. Research Report T90\/9002, SICS (1990)"},{"key":"13_CR145","unstructured":"Ernberg, P., Hovander, T., Monfort, F.: Specification and implementation of an ISDN telephone system using LOTOS. In: Diaz, M., Groz, R. (eds.) Proceedings of the IFIP TC6\/WG6.1 5th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE 1992), Perros-Guirec, France. IFIP Transactions, vol. C-10, pp. 171\u2013186. North-Holland, October 1992"},{"key":"13_CR146","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-76562-9_13","volume-title":"Proceedings Verl\u00e4\u00dfliche Informationssysteme","author":"K Estenfeld","year":"1991","unstructured":"Estenfeld, K., Schneider, H.A., Taubner, D., Tid\u00e9n, E.: Computer aided verification of parallel processes. In: Pfitzmann, A., Raubold, E. (eds.) VIS 1991, vol. 271, pp. 208\u2013226. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/978-3-642-76562-9_13"},{"key":"13_CR147","unstructured":"Fernandez, J.C.: ALDEBARAN: Un syst\u00e8me de v\u00e9rification par r\u00e9duction de processus communicants. Ph.D. thesis, Universit\u00e9 Joseph Fourier (Grenoble), May 1988"},{"key":"13_CR148","unstructured":"Fernandez, J.C.: ALDEBARAN: A Tool for Verification of Communicating Processes. Rapport SPECTRE C14, Laboratoire de G\u00e9nie Informatique - Institut IMAG, Grenoble, September 1989"},{"key":"13_CR149","unstructured":"Fernandez, J.C.: ALDEBARAN: User\u2019s Manual. Laboratoire de G\u00e9nie Informatique \u2013 Institut IMAG, Grenoble, January 1989"},{"issue":"2\u20133","key":"13_CR150","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/0167-6423(90)90071-K","volume":"13","author":"JC Fernandez","year":"1990","unstructured":"Fernandez, J.C.: An implementation of an efficient algorithm for bisimulation equivalence. Sci. Comput. Program. 13(2\u20133), 219\u2013236 (1990)","journal-title":"Sci. Comput. Program."},{"key":"13_CR151","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/3-540-61474-5_97","volume-title":"Computer Aided Verification","author":"J-C Fernandez","year":"1996","unstructured":"Fernandez, J.-C., Garavel, H., Kerbrat, A., Mounier, L., Mateescu, R., Sighireanu, M.: CADP (C\u00c6SAR\/ALDEBARAN Development Package): a protocol validation and verification toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 437\u2013440. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_97"},{"key":"13_CR152","doi-asserted-by":"crossref","unstructured":"Fernandez, J.C., Garavel, H., Mounier, L., Rasse, A., Rodr\u00edguez, C., Sifakis, J.: A toolbox for the verification of LOTOS programs. In: Clarke, L.A. (ed.) Proceedings of the 14th International Conference on Software Engineering (ICSE 2014), Melbourne, Australia, pp. 246\u2013259. ACM, May 1992","DOI":"10.1145\/143062.143124"},{"key":"13_CR153","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-56922-7_8","volume-title":"Computer Aided Verification","author":"JC Fernandez","year":"1993","unstructured":"Fernandez, J.C., Kerbrat, A., Mounier, L.: Symbolic equivalence checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 85\u201396. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56922-7_8"},{"key":"13_CR154","unstructured":"Fernandez, J.C., Mounier, L.: Verifying bisimulations \u201cOn the Fly\u201d. In: Quemada, J., Manas, J., V\u00e1zquez, E. (eds.) Proceedings of the 3rd International Conference on Formal Description Techniques (FORTE 1990), Madrid, Spain. North-Holland, November 1990"},{"key":"13_CR155","doi-asserted-by":"crossref","unstructured":"Fernandez, J.C., Mounier, L.: A tool set for deciding behavioral equivalences. In: Proceedings of CONCUR 1991, Amsterdam, The Netherlands, August 1991","DOI":"10.1007\/3-540-54430-5_78"},{"key":"13_CR156","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/3-540-55179-4_18","volume-title":"Computer Aided Verification","author":"J-C Fernandez","year":"1992","unstructured":"Fernandez, J.-C., Mounier, L.: \u201cOn the fly\u2019\u2019 verification of behavioural equivalences and preorders. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 181\u2013191. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55179-4_18"},{"key":"13_CR157","unstructured":"Ferrari, G., Modoni, G., Quaglia, P.: Towards a semantic-based verification environment for the $$\\pi $$-calculus. In: De Santis, A. (ed.) Proceedings of the 5th Italian Conference on Theoretical Computer Science (1995)"},{"key":"13_CR158","unstructured":"F\u00e9vrier, A., Najm, E., Prost, N., Robles, F.: Verifying an ATM switch with Formal Methods (1994). http:\/\/cadp.inria.fr\/ftp\/publications\/others\/Fevrier-Najm-Prost-Robles-94.pdf"},{"key":"13_CR159","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/3-540-49519-3_9","volume-title":"Formal Methods in Computer-Aided Design","author":"K Fisler","year":"1998","unstructured":"Fisler, K., Vardi, M.Y.: Bisimulation minimization in an automata-theoretic verification framework. In: Gopalakrishnan, G., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 115\u2013132. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49519-3_9"},{"key":"13_CR160","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/3-540-48153-2_29","volume-title":"Correct Hardware Design and Verification Methods","author":"K Fisler","year":"1999","unstructured":"Fisler, K., Vardi, M.Y.: Bisimulation and model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 338\u2013342. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_29"},{"issue":"1","key":"13_CR161","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1023\/A:1016091902809","volume":"21","author":"K Fisler","year":"2002","unstructured":"Fisler, K., Vardi, M.Y.: Bisimulation minimization and symbolic model checking. Formal Methods Syst. Des. 21(1), 39\u201378 (2002)","journal-title":"Formal Methods Syst. Des."},{"issue":"9","key":"13_CR162","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1109\/32.629493","volume":"23","author":"R Focardi","year":"1997","unstructured":"Focardi, R., Gorrieri, R.: The compositional security checker: a tool for the verification of information flow security properties. IEEE Trans. Softw. Eng. 23(9), 550\u2013571 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"13_CR163","unstructured":"Franceschinis, G., Ribaudo, M.: Symmetric and behavioural aggregation in a simple protocol example. In: Proceedings of the 6th International Workshop on Process Algebra and Performance Modelling (PAPM 1998), Nice, France (1998)"},{"key":"13_CR164","doi-asserted-by":"crossref","unstructured":"Francesco, N.D., Lettieri, G., Santone, A., Vaglini, G.: GreASE: a tool for efficient \u201cNonequivalence\u201d checking. ACM Trans. Softw. Eng. Methodol. 23(3), 24:1\u201324:26 (2014)","DOI":"10.1145\/2560563"},{"key":"13_CR165","unstructured":"Fredlund, L., Orava, F.: An experiment in formalizing and analysing railyard configurations. In: Brezo\u010dnik, Z., Kapus, T. (eds.) Proceedings of COST 247 International Workshop on Applied Formal Methods in System Design (Maribor, Slovenia), pp. 51\u201360. University of Maribor, Slovenia, June 1996"},{"key":"13_CR166","unstructured":"Fredlund, L.A.: The Timing and Probability Workbench: A tool for Analysing Timed Processes (1994). CiteSeer"},{"key":"13_CR167","doi-asserted-by":"crossref","unstructured":"Fredlund, L.A., Orava, F.: Modelling dynamic communication structures in LOTOS. In: Parker, K.R., Rose, G.A. (eds.) Proceedings of the IFIP TC6\/WG6.1 4th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE 1991), Sydney, Australia. IFIP Transactions, vol. C-2, pp. 185\u2013200. North-Holland, November 1991","DOI":"10.1016\/B978-0-444-89402-1.50023-0"},{"key":"13_CR168","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-319-39570-8_10","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"D de Frutos Escrig","year":"2016","unstructured":"de Frutos Escrig, D., Keiren, J.J.A., Willemse, T.A.C.: Branching bisimulation games. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 142\u2013157. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-39570-8_10"},{"key":"13_CR169","series-title":"Advances in Computing Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-7091-6355-9_7","volume-title":"Tool Support for System Specification, Development and Verification","author":"K Fuhrmann","year":"1998","unstructured":"Fuhrmann, K., Hiemer, J.: Formal verification of statemate-statecharts. In: Berghammer, R., Lakhnech, Y. (eds.) Tool Support for System Specification, Development and Verification. ACS, pp. 92\u2013107. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/978-3-7091-6355-9_7"},{"key":"13_CR170","unstructured":"Garavel, H.: Compilation et v\u00e9rification de programmes LOTOS. Ph.D. thesis, Universit\u00e9 Joseph Fourier (Grenoble), November 1989"},{"key":"13_CR171","unstructured":"Garavel, H.: An overview of the Eucalyptus toolbox. In: Brezo\u010dnik, Z., Kapus, T. (eds.) Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design (Maribor, Slovenia), pp. 76\u201388. University of Maribor, Slovenia, June 1996"},{"key":"13_CR172","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/BFb0054165","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Garavel","year":"1998","unstructured":"Garavel, H.: OPEN\/C\u00c6SAR: an open software architecture for verification, simulation, and testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 68\u201384. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054165"},{"key":"13_CR173","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/3-540-45614-7_23","volume-title":"FME 2002:Formal Methods\u2014Getting IT Right","author":"H Garavel","year":"2002","unstructured":"Garavel, H., Hermanns, H.: On combining functional verification and performance evaluation using CADP. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 410\u2013429. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45614-7_23 Full version available as INRIA Research Report 4492"},{"key":"13_CR174","unstructured":"Garavel, H., Jorgensen, M., Mateescu, R., Pecheur, C., Sighireanu, M., Vivien, B.: CADP\u201997 - status, applications and perspectives. In: Lovrek, I. (ed.) Proceedings of the 2nd COST 247 International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia), June 1997"},{"key":"13_CR175","doi-asserted-by":"crossref","unstructured":"Garavel, H., Lang, F.: SVL: a scripting language for compositional verification. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2001), Cheju Island, Korea, pp. 377\u2013392. Kluwer Academic Publishers, August 2001. Full version available as INRIA Research Report RR-4223","DOI":"10.1007\/0-306-47003-9_24"},{"key":"13_CR176","unstructured":"Garavel, H., Lang, F., Mateescu, R.: An Overview of CADP 2001. European Association for Software Science and Technology (EASST) Newsletter 4, 13\u201324 (Aug 2002), also available as INRIA Technical Report RT-0254, December 2001"},{"issue":"4","key":"13_CR177","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s00236-015-0226-1","volume":"52","author":"H Garavel","year":"2015","unstructured":"Garavel, H., Lang, F., Mateescu, R.: Compositional verification of asynchronous concurrent systems using CADP. Acta Informatica 52(4), 337\u2013392 (2015)","journal-title":"Acta Informatica"},{"key":"13_CR178","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-540-73368-3_18","volume-title":"Computer Aided Verification","author":"H Garavel","year":"2007","unstructured":"Garavel, H., Mateescu, R., Lang, F., Serwe, W.: CADP\u00a02006: a toolbox for the construction and analysis of distributed processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158\u2013163. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_18"},{"key":"13_CR179","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-642-19835-9_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Garavel","year":"2011","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: a toolbox for the construction and analysis of distributed processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372\u2013387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_33"},{"issue":"2","key":"13_CR180","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transfer (STTT) 15(2), 89\u2013107 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transfer (STTT)"},{"key":"13_CR181","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-030-00244-2_13","volume-title":"Formal Methods for Industrial Critical Systems","author":"H Garavel","year":"2018","unstructured":"Garavel, H., Lang, F., Mounier, L.: Compositional verification in action. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 189\u2013210. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00244-2_13"},{"key":"13_CR182","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-68270-9_1","volume-title":"ModelEd, TestEd, TrustEd","author":"H Garavel","year":"2017","unstructured":"Garavel, H., Lang, F., Serwe, W.: From LOTOS to LNT. In: Katoen, J.-P., Langerak, R., Rensink, A. (eds.) ModelEd, TestEd, TrustEd. LNCS, vol. 10500, pp. 3\u201326. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68270-9_1"},{"key":"13_CR183","doi-asserted-by":"crossref","unstructured":"Garavel, H., Mounier, L.: Specification and verification of various distributed leader election algorithms for unidirectional ring networks. Sci. Comput. Program. 29(1\u20132), 171\u2013197 (1997). Special issue on Industrially Relevant Applications of Formal Analysis Techniques. Full version available as INRIA Research Report RR-2986","DOI":"10.1016\/S0167-6423(96)00034-2"},{"key":"13_CR184","unstructured":"Garavel, H., Sifakis, J.: Compilation and verification of LOTOS specifications. In: Logrippo, L., Probert, R.L., Ural, H. (eds.) Proceedings of the 10th IFIP International Symposium on Protocol Specification, Testing and Verification (PSTV 1990), Ottawa, Canada, pp. 379\u2013394. North-Holland, June 1990"},{"key":"13_CR185","unstructured":"Germeau, F., Leduc, G.: Model-based design and verification of security protocols using LOTOS. In: Orman, H., Meadows, C. (eds.) Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols (Rutgers University, New Jersey, USA), September 1997"},{"issue":"2","key":"13_CR186","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1006\/inco.1998.2778","volume":"150","author":"R Gerth","year":"1999","unstructured":"Gerth, R., Kuiper, R., Peled, D.A., Penczek, W.: A partial order approach to branching time logic model checking. Inf. Comput. 150(2), 132\u2013152 (1999)","journal-title":"Inf. Comput."},{"key":"13_CR187","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/3-540-58021-2_20","volume-title":"Computer Performance Evaluation Modelling Techniques and Tools","author":"S Gilmore","year":"1994","unstructured":"Gilmore, S., Hillston, J.: The PEPA workbench: a tool to support a process algebra-based approach to performance modelling. In: Haring, G., Kotsis, G. (eds.) TOOLS 1994. LNCS, vol. 794, pp. 353\u2013368. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58021-2_20"},{"key":"13_CR188","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-540-24663-3_15","volume-title":"Performance Tools and Applications to Networked Systems","author":"S Gilmore","year":"2004","unstructured":"Gilmore, S., Hillston, J., Kloul, L.: PEPA nets. In: Calzarossa, M.C., Gelenbe, E. (eds.) MASCOTS 2003. LNCS, vol. 2965, pp. 311\u2013335. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24663-3_15"},{"issue":"2","key":"13_CR189","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/S0166-5316(03)00069-5","volume":"54","author":"S Gilmore","year":"2003","unstructured":"Gilmore, S., Hillston, J., Kloul, L., Ribaudo, M.: PEPA nets: a structured performance modelling formalism. Perform. Eval. 54(2), 79\u2013104 (2003)","journal-title":"Perform. Eval."},{"key":"13_CR190","unstructured":"van Glabbeek, R.J.: The linear time - branching time spectrum I. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 3\u201399. North-Holland\/Elsevier (2001)"},{"key":"13_CR191","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching-time and abstraction in bisimulation semantics (extended abstract). CS R8911, Centrum voor Wiskunde en Informatica, Amsterdam (1989). Also in Proceedings of IFIP 11th World Computer Congress, San Francisco (1989)"},{"issue":"3","key":"13_CR192","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"RJ van Glabbeek","year":"1996","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555\u2013600 (1996)","journal-title":"J. ACM"},{"key":"13_CR193","doi-asserted-by":"crossref","unstructured":"Gnesi, S., Madelaine, E., Ristori, G.: An exercise in protocol verification, pp. 255\u2013279. Kluwer (1995)","DOI":"10.1007\/978-1-4615-2203-4_13"},{"key":"13_CR194","unstructured":"Godskesen, J.C., Larsen, K.G., Zeeberg, M.: TAV (tools for automatic verification). In: Sifakis, J. (ed.) Proceedings of the 1st International Workshop on Automatic Verification Methods for Finite State Systems (CAV 1989), Grenoble, France, June 1989. Article present only in the participants proceedings, not in the LNCS 407 post-proceedings volume"},{"key":"13_CR195","unstructured":"Godskesen, J.C., Larsen, K.G.: User\u2019s Manual for Epsilon (Draft), available from CiteSeer"},{"key":"13_CR196","doi-asserted-by":"crossref","unstructured":"Godskesen, J.C., Larsen, K.G., Skou, A.: Automatic verification of real-time systems using Epsilon. In: Vuong, S.T., Chanson, S.T. (eds.) Protocol Specification, Testing and Verification XIV, Proceedings of the 14th IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Vancouver, BC, Canada. IFIP Conference Proceedings, vol. 1, pp. 323\u2013330. Chapman & Hall (1994)","DOI":"10.1007\/978-0-387-34867-4_21"},{"key":"13_CR197","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/BFb0023732","volume-title":"Computer-Aided Verification","author":"S Graf","year":"1991","unstructured":"Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 186\u2013196. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/BFb0023732"},{"issue":"5","key":"13_CR198","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BF01211911","volume":"8","author":"S Graf","year":"1996","unstructured":"Graf, S., Steffen, B., L\u00fcttgen, G.: Compositional minimization of finite state systems using interface specifications. Formal Aspects Comput. 8(5), 607\u2013616 (1996)","journal-title":"Formal Aspects Comput."},{"key":"13_CR199","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-540-27813-9_43","volume-title":"Computer Aided Verification","author":"A Griffault","year":"2004","unstructured":"Griffault, A., Vincent, A.: The Mec 5 model-checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 488\u2013491. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_43"},{"key":"13_CR200","unstructured":"Groote, J.: The Syntax and Semantics of Timed $$\\mu $$CRL. Technical Report SEN-R9709, CWI, Amsterdam, The Netherlands, June 1997"},{"key":"13_CR201","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Jansen, D.N., Keiren, J.J.A., Wijs, A.: An $$O(m \\log n)$$ algorithm for computing stuttering equivalence and branching bisimulation. ACM Trans. Comput. Log. 18(2), 13:1\u201313:34 (2017)","DOI":"10.1145\/3060140"},{"key":"13_CR202","unstructured":"Groote, J.F., Martens, J., de Vink, E.P.: Bisimulation by partitioning is $$\\varOmega ((m+n) \\log n)$$. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory (CONCUR 2021), Virtual Conference. LIPIcs, vol. 203, pp. 31:1\u201331:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, August 2021"},{"key":"13_CR203","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/j.entcs.2005.12.101","volume":"162","author":"JF Groote","year":"2006","unstructured":"Groote, J.F., Mathijssen, A., van Weerdenburg, M., Usenko, Y.S.: From $$\\mu $$CRL to mCRL2: motivation and outline. Electron. Notes Theor. Comput. Sci. 162, 191\u2013196 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"13_CR204","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1007\/BFb0014338","volume-title":"Algebraic Methodology and Software Technology","author":"JF Groote","year":"1996","unstructured":"Groote, J.F., van de Pol, J.: A bounded retransmission protocol for large data packets. In: Wirsing, M., Nivat, M. (eds.) AMAST 1996. LNCS, vol. 1101, pp. 536\u2013550. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0014338"},{"issue":"1\u20132","key":"13_CR205","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0304-3975(96)80702-X","volume":"170","author":"JF Groote","year":"1996","unstructured":"Groote, J.F., Sellink, M.P.A.: Confluence for process verification. Theor. Comput. Sci. 170(1\u20132), 47\u201381 (1996)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR206","unstructured":"Groote, J., Vaandrager, F.: An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence. CS-R 9001, Centrum voor Wiskunde en Informatica, Amsterdam, January 1990"},{"key":"13_CR207","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1007\/BFb0032063","volume-title":"Automata, Languages and Programming","author":"JF Groote","year":"1990","unstructured":"Groote, J.F., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Paterson, M.S. (ed.) ICALP 1990. LNCS, vol. 443, pp. 626\u2013638. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0032063"},{"issue":"2","key":"13_CR208","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1016\/0890-5401(92)90013-6","volume":"100","author":"JF Groote","year":"1992","unstructured":"Groote, J.F., Vaandrager, F.W.: Structured operational semantics and bisimulation as a congruence. Inf. Comput. 100(2), 202\u2013260 (1992)","journal-title":"Inf. Comput."},{"issue":"9","key":"13_CR209","doi-asserted-by":"publisher","first-page":"131","DOI":"10.3390\/a11090131","volume":"11","author":"JF Groote","year":"2018","unstructured":"Groote, J.F., Verduzco, J.R., de Vink, E.P.: An efficient algorithm to determine probabilistic bisimulation. Algorithms 11(9), 131 (2018)","journal-title":"Algorithms"},{"key":"13_CR210","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/978-3-662-49674-9_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JF Groote","year":"2016","unstructured":"Groote, J.F., Wijs, A.: An $$O(m\\log n)$$ algorithm for stuttering equivalence and branching bisimulation. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 607\u2013624. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_40"},{"key":"13_CR211","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Wijs, A.: An $$O(m \\log n)$$ algorithm for stuttering equivalence and branching bisimulation. CoRR abs\/1601.01478 (2016)","DOI":"10.1007\/978-3-662-49674-9_40"},{"key":"13_CR212","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-1-4757-2231-4_10","volume-title":"Synchronous Programming of Reactive Systems","author":"N Halbwachs","year":"1993","unstructured":"Halbwachs, N.: Using Auto for Esterel program verification. In: Halbwachs, N. (ed.) Synchronous Programming of Reactive Systems, vol. 215, pp. 149\u2013155. Springer, Boston (1993). https:\/\/doi.org\/10.1007\/978-1-4757-2231-4_10"},{"key":"13_CR213","unstructured":"Hansson, H.A.: Time and probability in formal design of distributed systems. Ph.d. thesis, University Uppsala, Sweden (1991)"},{"key":"13_CR214","unstructured":"Hansson, H.A.: Time and Probability in Formal Design of Distributed Systems. Elsevier (1994)"},{"key":"13_CR215","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-319-30000-9_9","volume-title":"Language and Automata Theory and Applications","author":"V Hashemi","year":"2016","unstructured":"Hashemi, V., Hermanns, H., Song, L., Subramani, K., Turrini, A., Wojciechowski, P.: Compositional bisimulation minimization for interval Markov decision processes. In: Dediu, A.-H., Janou\u0161ek, J., Mart\u00edn-Vide, C., Truthe, B. (eds.) LATA 2016. LNCS, vol. 9618, pp. 114\u2013126. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30000-9_9"},{"key":"13_CR216","unstructured":"Hashemi, V., Hermanns, H., Turrini, A.: On the efficiency of deciding probabilistic automata weak bisimulation. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 66 (2013)"},{"key":"13_CR217","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-319-69483-2_2","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications","author":"V Hashemi","year":"2017","unstructured":"Hashemi, V., Turrini, A., Hahn, E.M., Hermanns, H., Elbassioni, K.: Polynomial-time alternating probabilistic bisimulation for interval MDPs. In: Larsen, K.G., Sokolsky, O., Wang, J. (eds.) SETTA 2017. LNCS, vol. 10606, pp. 25\u201341. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-69483-2_2"},{"key":"13_CR218","unstructured":"He, J., Turner, K.J.: Modelling and Verifying Synchronous Circuits in DILL. Technical Report CSM-152, Department of Computing Science and Mathematics, University of Stirling (1999)"},{"key":"13_CR219","unstructured":"He, J., Turner, K.J.: Protocol-inspired hardware testing. In: Csopaki, G., Dibuz, S., Tarnay, K. (eds.) Proceedings of the IFIP 12th International Workshop on Testing of Communicating Systems (IWTCS 1999), Budapest, Hungary, pp. 131\u2013147. Kluwer Academic, September 1999"},{"key":"13_CR220","unstructured":"He, J., Turner, K.J.: Specification and verification of synchronous hardware using LOTOS. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Proceedings of the IFIP Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing, and Verification (FORTE\/PSTV 1999), Beijing, China, pp. 295\u2013312. Kluwer Academic Publishers, October 1999"},{"key":"13_CR221","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"818","DOI":"10.1007\/BFb0030643","volume-title":"TAPSOFT \u201997: Theory and Practice of Software Development","author":"M Heisel","year":"1997","unstructured":"Heisel, M., L\u00e9vy, N.: Using LOTOS patterns to characterize architectural styles. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997. LNCS, vol. 1214, pp. 818\u2013832. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0030643"},{"key":"13_CR222","unstructured":"Hellgren, V.: Performance Evaluation of Four Verification Tools: ALDEBARAN, BIDMIN, Concurrency Workbench and HOGGAR. Technical report, University of Helsinki, Department of Computer Science, p. 4, August 1995"},{"key":"13_CR223","unstructured":"Hellgren, V.: User\u2019s Manual: BIDMIN Version 1.2. Technical report, University of Helsinki, Department of Computer Science, p. 10, August 1995"},{"issue":"2","key":"13_CR224","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1016\/0304-3975(94)00172-F","volume":"138","author":"M Hennessy","year":"1995","unstructured":"Hennessy, M., Lin, H.: Symbolic bisimulations. Theor. Comput. Sci. 138(2), 353\u2013389 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR225","doi-asserted-by":"crossref","unstructured":"Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: 36th Annual Symposium on Foundations of Computer Science, Milwaukee, Wisconsin, USA, 23\u201325 October 1995, pp. 453\u2013462. IEEE Computer Society (1995)","DOI":"10.1109\/SFCS.1995.492576"},{"key":"13_CR226","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-60084-1_85","volume-title":"Automata, Languages and Programming","author":"TA Henzinger","year":"1995","unstructured":"Henzinger, T.A.: Hybrid automata with finite bisimulations. In: F\u00fcl\u00f6p, Z., G\u00e9cseg, F. (eds.) ICALP 1995. LNCS, vol. 944, pp. 324\u2013335. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60084-1_85"},{"key":"13_CR227","unstructured":"Herbert, M.: Evaluation de performances et sp\u00e9cification formelle sur un r\u00e9seau de stations haut d\u00e9bit. Master\u2019s thesis, Institut National des T\u00e9l\u00e9communications, Laboratoire pour les hautes performances en calcul (Lyon, France), December 1997"},{"key":"13_CR228","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45804-2","volume-title":"Interactive Markov Chains: The Quest for Quantified Quality","author":"H Hermanns","year":"2002","unstructured":"Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45804-2"},{"key":"13_CR229","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/3-540-68061-6_5","volume-title":"Computer Performance Evaluation","author":"H Hermanns","year":"1998","unstructured":"Hermanns, H., Herzog, U., Klehmet, U., Mertsiotakis, V., Siegle, M.: Compositional performance modelling with the TIPPtool. In: Puigjaner, R., Savino, N.N., Serra, B. (eds.) TOOLS 1998. LNCS, vol. 1469, pp. 51\u201362. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-68061-6_5"},{"issue":"1\u20134","key":"13_CR230","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0166-5316(99)00056-5","volume":"39","author":"H Hermanns","year":"2000","unstructured":"Hermanns, H., Herzog, U., Klehmet, U., Mertsiotakis, V., Siegle, M.: Compositional performance modelling with the TIPPtool. Perform. Eval. 39(1\u20134), 5\u201335 (2000)","journal-title":"Perform. Eval."},{"key":"13_CR231","doi-asserted-by":"crossref","unstructured":"Hermanns, H., Herzog, U., Mertsiotakis, V.: Stochastic process algebras as a tool for performance and dependability modelling. In: Proceedings of the 1995 International Computer Performance and Dependability Symposium, pp. 102\u2013111. IEEE (1995)","DOI":"10.1109\/IPDS.1995.395813"},{"issue":"9\u201310","key":"13_CR232","first-page":"901","volume":"30","author":"H Hermanns","year":"1998","unstructured":"Hermanns, H., Herzog, U., Mertsiotakis, V.: Stochastic process algebras - between LOTOS and Markov chains. Comput. Netw. 30(9\u201310), 901\u2013924 (1998)","journal-title":"Comput. Netw."},{"key":"13_CR233","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/3-540-36577-X_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Hermanns","year":"2003","unstructured":"Hermanns, H., Joubert, C.: A set of performance and dependability analysis components for CADP. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 425\u2013430. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_30"},{"key":"13_CR234","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/S0167-6423(99)00019-2","volume":"36","author":"H Hermanns","year":"2000","unstructured":"Hermanns, H., Katoen, J.P.: Automated compositional Markov chain generation for a plain-old telephone system. Sci. Comput. Program. 36, 97\u2013127 (2000)","journal-title":"Sci. Comput. Program."},{"key":"13_CR235","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-642-17071-3_16","volume-title":"Formal Methods for Components and Objects","author":"H Hermanns","year":"2010","unstructured":"Hermanns, H., Katoen, J.-P.: The how and why of interactive Markov chains. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 311\u2013337. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17071-3_16"},{"key":"13_CR236","unstructured":"Hermanns, H., Mertsiotakis, V., Rettelbach, M.: Performance analysis of distributed systems using TIPP\u2014a case study. In: Proceedings of the 10th U.K. Performance Engineering Workshop for Computer and Telecommunication Systems, Edinburgh, Scotland, United Kingdom. Edinburgh University Press, September 1994"},{"key":"13_CR237","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/3-540-48683-6_42","volume-title":"Computer Aided Verification","author":"H Hermanns","year":"1999","unstructured":"Hermanns, H., Mertsiotakis, V., Siegle, M.: TIPPtool: compositional specification and analysis of Markovian performance models. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 487\u2013490. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48683-6_42"},{"key":"13_CR238","unstructured":"Hermanns, H., Rettelbach, M.: Syntax, semantics, equivalences, and axioms for MTIPP. In: Herzog, U., Rettelbach, M. (eds.) Proceedings of the 2nd Workshop on Process Algebras and Performance Modelling (PAPM 1994), Erlangen, Germany. Lecture Notes in Computer Science, vol. 1601, pp. 71\u201388. University of Erlangen-N\u00fcrnberg, Germany, July 1994"},{"issue":"7","key":"13_CR239","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1093\/comjnl\/38.7.530","volume":"38","author":"H Hermanns","year":"1995","unstructured":"Hermanns, H., Rettelbach, M., Weiss, T.: Formal characterisation of immediate actions in SPA with nondeterministic branching. Comput. J. 38(7), 530\u2013541 (1995)","journal-title":"Comput. J."},{"key":"13_CR240","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/3-540-48778-6_15","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"H Hermanns","year":"1999","unstructured":"Hermanns, H., Siegle, M.: Bisimulation algorithms for stochastic process algebras and their BDD-based implementation. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol. 1601, pp. 244\u2013264. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48778-6_15"},{"key":"13_CR241","unstructured":"Hermanns, H., Siegle, M.: Symbolic minimisation of stochastic process algebra models. In: Spies, K., Sch\u00e4tz, B. (eds.) Formale Beschreibungstechniken f\u00fcr verteilte Systeme, 9. GI\/ITG-Fachgespr\u00e4ch, M\u00fcnchen, Juni 1999, pp. 73\u201382. Herbert Utz Verlag (1999)"},{"key":"13_CR242","unstructured":"Hermanns, H., Turrini, A.: Deciding probabilistic automata weak bisimulation in polynomial time. In: D\u2019Souza, D., Kavitha, T., Radhakrishnan, J. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, Hyderabad, India, 15\u201317 December 2012. LIPIcs, vol. 18, pp. 435\u2013447. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012)"},{"key":"13_CR243","doi-asserted-by":"crossref","unstructured":"Hernalsteen, C.: A timed automaton model for ET-LOTOS verification. In: Togashi, A., Mizuno, T., Shiratori, N., Higashino, T. (eds.) Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE X\/PSTV XVII 1997, IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE X) and Protocol Specification, Testing and Verification (PSTV XVII), Osaka, Japan, 18\u201321 November 1997. IFIP Conference Proceedings, vol. 107, pp. 193\u2013204. Chapman & Hall (1997)","DOI":"10.1007\/978-0-387-35271-8_12"},{"key":"13_CR244","unstructured":"Herzog, U., Mertsiotakis, V.: Stochastic process algebras applied to failure modelling. In: Herzog, U., Rettelbach, M. (eds.) Proceedings of the 2nd Workshop on Process Algebras and Performance Modelling, Regensberg, Germany. Arbeitsberichte des IMMD, Universit\u00e4t Erlangen-N\u00fcrnberg, Germany, July 1994"},{"key":"13_CR245","unstructured":"Hillerstr\u00f6m, M.: Verification of CCS-processes. Master\u2019s thesis, Computer Science Department, Aalborg University (1987)"},{"key":"13_CR246","unstructured":"Hillston, J.: A compositional approach to performance modelling. Ph.D. thesis, University of Edinburgh, December 1994"},{"key":"13_CR247","doi-asserted-by":"crossref","unstructured":"Hillston, J., Hermanns, Herzog, U., Mertsiotakis, V., Rettelbach, M.: Stochastic Process Algebras: Integrating Qualitative and Quantitative Modelling. Technical report, IMMD VII, University of Erlangen-N\u00fcrnberg, Germany (1994)","DOI":"10.1007\/978-0-387-34878-0_36"},{"key":"13_CR248","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-030-25540-4_27","volume-title":"Computer Aided Verification","author":"C-D Hong","year":"2019","unstructured":"Hong, C.-D., Lin, A.W., Majumdar, R., R\u00fcmmer, P.: Probabilistic bisimulation for parameterized systems. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 455\u2013474. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_27"},{"key":"13_CR249","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-49382-2_26","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"M Huhn","year":"1998","unstructured":"Huhn, M., Niebert, P., Wehrheim, H.: Partial order reductions for bisimulation checking. In: Arvind, V., Ramanujam, R. (eds.) FSTTCS 1998. LNCS, vol. 1530, pp. 271\u2013282. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/978-3-540-49382-2_26"},{"key":"13_CR250","unstructured":"Huth, M., Kwiatkowska, M.: On Probabilistic Model Checking (1996). CiteSeer"},{"key":"13_CR251","doi-asserted-by":"crossref","unstructured":"Huybers, R.: A parallel relation-based algorithm for symbolic bisimulation minimization. Ph.D. thesis, Leiden University (2018)","DOI":"10.1007\/978-3-030-11245-5_25"},{"key":"13_CR252","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1007\/978-3-030-11245-5_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Huybers","year":"2019","unstructured":"Huybers, R., Laarman, A.: A parallel relation-based algorithm for symbolic bisimulation minimization. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 535\u2013554. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_25"},{"key":"13_CR253","doi-asserted-by":"crossref","unstructured":"Ing\u00f3lfsd\u00f3ttir, A., Lin, H.: A symbolic approach to value-passing processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 427\u2013478. North-Holland\/Elsevier (2001)","DOI":"10.1016\/B978-044482830-9\/50025-4"},{"key":"13_CR254","unstructured":"Inverardi, P., Priami, C., Yankelevich, D.: Verification of concurrent systems in SML. In: Proceedings of ACM SIGPLAN Workshop on ML and its Applications, pp. 169\u2013174 (1992)"},{"key":"13_CR255","first-page":"158","volume":"45","author":"P Inverardi","year":"1991","unstructured":"Inverardi, P., Priami, C.: Evaluation of tools for the analysis of communicating systems. Bull. Eur. Assoc. Theor. Comput. Sci. (EATCS) 45, 158\u2013185 (1991)","journal-title":"Bull. Eur. Assoc. Theor. Comput. Sci. (EATCS)"},{"issue":"1","key":"13_CR256","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/BF00121261","volume":"8","author":"P Inverardi","year":"1996","unstructured":"Inverardi, P., Priami, C.: Automatic verification of distributed systems: the process algebra approach. Formal Methods Syst. Des. 8(1), 7\u201338 (1996)","journal-title":"Formal Methods Syst. Des."},{"issue":"6","key":"13_CR257","doi-asserted-by":"publisher","first-page":"676","DOI":"10.1007\/BF03259392","volume":"6","author":"P Inverardi","year":"1994","unstructured":"Inverardi, P., Priami, C., Yankelevich, D.: Automatizing parametric reasoning on distributed concurrent systems. Formal Aspects Comput. 6(6), 676\u2013695 (1994). https:\/\/doi.org\/10.1007\/BF03259392","journal-title":"Formal Aspects Comput."},{"key":"13_CR258","unstructured":"ISO\/IEC: ESTELLE - A Formal Description Technique Based on an Extended State Transition Model. International Standard 9074, International Organization for Standardization - Information Processing Systems - Open Systems Interconnection, Geneva, September 1988"},{"key":"13_CR259","unstructured":"ISO\/IEC: LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization - Information Processing Systems - Open Systems Interconnection, Geneva, September 1989"},{"key":"13_CR260","unstructured":"de Jacquier, A., Massart, T., Hernalsteen, C.: V\u00e9rification et correction d\u2019un protocole de contr\u00f4le a\u00e9rien. Technical report 363, Universit\u00e9 Libre de Bruxelles, May 1997"},{"key":"13_CR261","unstructured":"Jansen, D.N., Groote, J.F., Keiren, J.J.A., Wijs, A.: A simpler $$O(m \\log n)$$ algorithm for branching bisimilarity on labelled transition systems. CoRR abs\/1909.10824 (2019)"},{"key":"13_CR262","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-45237-7_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"DN Jansen","year":"2020","unstructured":"Jansen, D.N., Groote, J.F., Keiren, J.J.A., Wijs, A.: An $$O(m \\log n)$$ algorithm for branching bisimilarity on labelled transition systems. In: Biere, A., Parker, D. (eds.) TACAS 2020. LNCS, vol. 12079, pp. 3\u201320. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_1"},{"key":"13_CR263","unstructured":"Jansen, D.N., Groote, J.F., Timmers, F., Yang, P.: A near-linear-time algorithm for weak bisimilarity on Markov chains. In: Konnov, I., Kov\u00e1cs, L. (eds.) 31st International Conference on Concurrency Theory, CONCUR 2020, Vienna, Austria, 1\u20134 September 2020 (Virtual Conference). LIPIcs, vol. 171, pp. 8:1\u20138:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"13_CR264","unstructured":"Jard, C., J\u00e9ron, T., Fernandez, J.C., Mounier, L.: On-the-Fly Verification of Finite Transition Systems. Research Report 1861, INRIA (1993)"},{"key":"13_CR265","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-55179-4_15","volume-title":"Computer Aided Verification","author":"CT Jensen","year":"1992","unstructured":"Jensen, C.T.: The Concurrency Workbench with priorities. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 147\u2013157. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55179-4_15"},{"issue":"3","key":"13_CR266","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.jlap.2012.01.001","volume":"81","author":"M Johansson","year":"2012","unstructured":"Johansson, M., Victor, B., Parrow, J.: Computing strong and weak bisimulations for psi-calculi. J. Log. Algebraic Methods Program. 81(3), 162\u2013180 (2012)","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"1","key":"13_CR267","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"PC Kanellakis","year":"1990","unstructured":"Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43\u201368 (1990)","journal-title":"Inf. Comput."},{"key":"13_CR268","doi-asserted-by":"crossref","unstructured":"Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. In: Probert, R.L., Lynch, N.A., Santoro, N. (eds.) Proceedings of the 2nd Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada, pp. 228\u2013240. ACM, August 1983","DOI":"10.1145\/800221.806724"},{"key":"13_CR269","unstructured":"Kang, I., Lee, I., Kim, Y.S.: A state minimization technique for timed automata. In: Proceedings of International Workshop on Verification of Infinite State Systems INFINITY 1996 (1996)"},{"key":"13_CR270","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61"},{"key":"13_CR271","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-71209-1_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J-P Katoen","year":"2007","unstructured":"Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87\u2013101. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_9"},{"issue":"2","key":"13_CR272","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"J Katoen","year":"2011","unstructured":"Katoen, J., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90\u2013104 (2011)","journal-title":"Perform. Eval."},{"key":"13_CR273","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-19237-1_12","volume-title":"Hardware and Software: Verification and Testing","author":"JJA Keiren","year":"2011","unstructured":"Keiren, J.J.A., Willemse, T.A.C.: Bisimulation minimisations for Boolean equation systems. In: Namjoshi, K., Zeller, A., Ziv, A. (eds.) HVC 2009. LNCS, vol. 6405, pp. 102\u2013116. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19237-1_12"},{"issue":"7","key":"13_CR274","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"RM Keller","year":"1976","unstructured":"Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371\u2013384 (1976)","journal-title":"Commun. ACM"},{"key":"13_CR275","series-title":"Undergraduate Texts in Mathematic","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Finite Markov Chains","author":"JG Kemeny","year":"1976","unstructured":"Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Undergraduate Texts in Mathematic, Springer, Heidelberg (1976)"},{"key":"13_CR276","unstructured":"Kerbrat, A.: M\u00e9thodes symboliques pour la v\u00e9rification de processus communicants: Etude et mise en \u0153uvre. Ph.D. thesis, Universit\u00e9 Joseph Fourier (Grenoble), November 1994"},{"key":"13_CR277","unstructured":"Kerbrat, A.: Reachable state space analysis of LOTOS programs. In: Hogrefe, D., Leue, S. (eds.) Proceedings of the 7th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols FORTE 1994 (Bern, Switzerland), October 1994"},{"key":"13_CR278","doi-asserted-by":"publisher","unstructured":"Kerbrat, A., Ben Atallah, S.: Formal specification of a framework for groupware development. In: FORTE 1995. IAICT, pp. 303\u2013310. Springer, Boston (1996). https:\/\/doi.org\/10.1007\/978-0-387-34945-9_22","DOI":"10.1007\/978-0-387-34945-9_22"},{"key":"13_CR279","doi-asserted-by":"crossref","unstructured":"Kerbrat, A., Rodriguez, C., Lejeune, Y.: Interconnecting the ObjectGEODE and C\u00c6SAR\/ALDEBARAN toolsets. In: Cavalli, A., Sarma, A. (eds.) Proceedings of the 8th SDL Forum (Evry, France), September 1997","DOI":"10.1016\/B978-044482816-3\/50032-0"},{"key":"13_CR280","unstructured":"Kervinen, A., Valmari, A., J\u00e4rnstr\u00f6m, R.: Debugging a real-life protocol with CFFD-based verification tools. In: Gnesi, S., Ultes-Nitsche, U. (eds.) Proceedings of the 6th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2001), Paris, France, pp. 13\u201327. Universit\u00e9 Paris 7 - LIAFA and INRIA Rh\u00f4ne-Alpes, July 2001"},{"key":"13_CR281","unstructured":"Klehmet, U., Mertsiotakis, V.: TIPPtool: Timed Processes and Performability Evaluation (User\u2019s Guide-Version 2.3) (1998). CiteSeer"},{"key":"13_CR282","unstructured":"K\u00f6nig, B., Mika-Michalski, C., Schr\u00f6der, L.: User Manual T-Beg: A Tool for Behavioural Equivalence Games (2002). http:\/\/www.ti.inf.uni-due.de\/fileadmin\/public\/tools\/tbeg\/manual.pdf"},{"key":"13_CR283","unstructured":"Korver, H.P.: The Current State of Bisimulation Tools. P 9101, Centrum voor Wiskunde en Informatica, Amsterdam, January 1991"},{"key":"13_CR284","doi-asserted-by":"crossref","unstructured":"Korver, H.: Detecting feature interactions with C\u00e6sar\/Aldebaran. Sci. Comput. Program. 29(1\u20132), 259\u2013278 (1997). Special issue on Industrially Relevant Applications of Formal Analysis Techniques","DOI":"10.1016\/S0167-6423(96)00037-8"},{"issue":"2","key":"13_CR285","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1023\/A:1008226622237","volume":"8","author":"BJ Kr\u00e4mer","year":"1998","unstructured":"Kr\u00e4mer, B.J., V\u00f6lker, N., Lichtenecker, R., K\u00f6tter, H.: Deriving CORBA applications from formal specifications. J. Syst. Integr. 8(2), 143\u2013158 (1998)","journal-title":"J. Syst. Integr."},{"key":"13_CR286","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/BFb0035392","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J-P Krimm","year":"1997","unstructured":"Krimm, J.-P., Mounier, L.: Compositional state space generation from LOTOS programs. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 239\u2013258. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0035392 Extended version with proofs available as Research Report VERIMAG RR97-01"},{"key":"13_CR287","first-page":"83","volume":"16","author":"S Kripke","year":"1963","unstructured":"Kripke, S.: Semantical considerations on modal logic. Acta Philosophica Fennica 16, 83\u201394 (1963)","journal-title":"Acta Philosophica Fennica"},{"issue":"3","key":"13_CR288","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0141-9331(94)90109-0","volume":"18","author":"P Krishnan","year":"1994","unstructured":"Krishnan, P.: A case study in specifying and testing architectural features. Microprocess. Microsyst. 18(3), 123\u2013130 (1994)","journal-title":"Microprocess. Microsyst."},{"key":"13_CR289","doi-asserted-by":"crossref","unstructured":"Kristensen, C., Andersen, J., Skou, A.: Specification and automated verification of real-time behaviour: a case study. In: Proceedings of the 3rd IFAC\/IFIP Workshop on Algorithms and Architectures for Real-Time Control (AARTC 1995), Ostend, Belgium (1995)","DOI":"10.1016\/S1474-6670(17)47282-X"},{"key":"13_CR290","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/S1367-5788(97)00005-9","volume":"20","author":"C Kristensen","year":"1996","unstructured":"Kristensen, C., Andersen, J., Skou, A.: Specification and automated verification of real-time behaviour: a case study. Annu. Rev. Control. 20, 55\u201370 (1996)","journal-title":"Annu. Rev. Control."},{"key":"13_CR291","unstructured":"Kulakowski, K.: Concurrent bisimulation algorithm. CoRR abs\/1311.7635 (2013)"},{"key":"13_CR292","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/11817963_23","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 234\u2013248. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_23"},{"key":"13_CR293","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"13_CR294","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/3-540-46002-0_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Lang","year":"2002","unstructured":"Lang, F.: Compositional verification using SVL scripts. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 465\u2013469. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_33"},{"key":"13_CR295","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/11589976_6","volume-title":"Integrated Formal Methods","author":"F Lang","year":"2005","unstructured":"Lang, F.: Exp.Open 2.0: a flexible tool integrating partial order, compositional, and on-the-fly verification methods. In: Romijn, J., Smith, G., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 70\u201388. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11589976_6 Full version available as INRIA Research Report RR-5673"},{"key":"13_CR296","doi-asserted-by":"publisher","unstructured":"Lang, F.: Refined interfaces for compositional verification. In: Najm, E., Pradat-Peyre, J.-F., Vigui\u00e9 Donzeau-Gouge, V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 159\u2013174. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11888116_13 Full version available as INRIA Research Report RR-5996","DOI":"10.1007\/11888116_13"},{"key":"13_CR297","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-05089-3_11","volume-title":"FM 2009: Formal Methods","author":"F Lang","year":"2009","unstructured":"Lang, F., Mateescu, R.: Partial order reductions using compositional confluence detection. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 157\u2013172. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-05089-3_11"},{"issue":"4","key":"13_CR298","first-page":"1","volume":"9","author":"F Lang","year":"2013","unstructured":"Lang, F., Mateescu, R.: Partial model checking using networks of labelled transition systems and Boolean equation systems. Logical Methods Comput. Sci. 9(4), 1\u201332 (2013)","journal-title":"Logical Methods Comput. Sci."},{"key":"13_CR299","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-030-30942-8_13","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"F Lang","year":"2019","unstructured":"Lang, F., Mateescu, R., Mazzanti, F.: Compositional verification of concurrent systems by combining bisimulations. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 196\u2013213. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_13"},{"key":"13_CR300","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-030-45237-7_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Lang","year":"2020","unstructured":"Lang, F., Mateescu, R., Mazzanti, F.: Sharp congruences adequate with temporal logics combining weak and strong modalities. In: Biere, A., Parker, D. (eds.) TACAS 2020. LNCS, vol. 12079, pp. 57\u201376. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_4"},{"key":"13_CR301","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-60249-6_41","volume-title":"Fundamentals of Computation Theory","author":"KG Larsen","year":"1995","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Model-checking for real-time systems. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 62\u201388. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60249-6_41"},{"key":"13_CR302","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. In: Conference Record of the 16th Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, 11\u201313 January 1989, pp. 344\u2013352. ACM Press (1989)","DOI":"10.1145\/75277.75307"},{"issue":"1","key":"13_CR303","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"KG Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1\u201328 (1991)","journal-title":"Inf. Comput."},{"key":"13_CR304","unstructured":"Leduc, G., Bonaventure, O., Koerner, E., L\u00e9onard, L., Pecheur, C., Zanetti, D.: Specification and verification of a TTP protocol for the conditional access to services. In: Proceedings of the 12th Jacques Cartier Workshop on \u201cFormal Methods and their Applications: Telecommunications, VLSI and Real-Time Computerized Control System\u201d, Montr\u00e9al, Canada, October 1996"},{"key":"13_CR305","doi-asserted-by":"crossref","unstructured":"Leduc, G.: Verification of two versions of the challenge handshake authentication protocol (CHAP). Ann. Telecommun. 55(1\u20132), 18\u201330 (2000)","DOI":"10.1007\/BF02997769"},{"key":"13_CR306","doi-asserted-by":"crossref","unstructured":"Lee, D., Yannakakis, M.: Online minimization of transition systems (extended abstract). In: Kosaraju, S.R., Fellows, M., Wigderson, A., Ellis, J.A. (eds.) Proceedings of the 24th Annual ACM Symposium on Theory of Computing, Victoria, British Columbia, Canada, 4\u20136 May 1992, pp. 264\u2013274. ACM (1992)","DOI":"10.1145\/129712.129738"},{"issue":"3","key":"13_CR307","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/S0169-7552(96)00078-5","volume":"29","author":"L L\u00e9onard","year":"1997","unstructured":"L\u00e9onard, L., Leduc, G.: An introduction to ET-LOTOS for the description of time-sensitive systems. Comput. Netw. ISDN Syst. 29(3), 271\u2013292 (1997)","journal-title":"Comput. Netw. ISDN Syst."},{"issue":"3","key":"13_CR308","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/s001650050015","volume":"10","author":"L L\u00e9onard","year":"1998","unstructured":"L\u00e9onard, L., Leduc, G.: A formal definition of time in LOTOS. Formal Aspects Comput. 10(3), 248\u2013266 (1998). https:\/\/doi.org\/10.1007\/s001650050015","journal-title":"Formal Aspects Comput."},{"key":"13_CR309","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/3-540-49059-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Z Li","year":"1999","unstructured":"Li, Z., Chen, H.: Computing strong\/weak bisimulation equivalences and observation congruence for value-passing processes. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 300\u2013314. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_21"},{"issue":"4","key":"13_CR310","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/BF02916743","volume":"42","author":"Z Li","year":"1999","unstructured":"Li, Z., Chen, H., Wang, B.: Symbolic transition graph and its early bisimulation checking algorithms for the $$\\pi $$-calculus. Sci. China Ser. E: Technol. Sci. 42(4), 342\u2013353 (1999)","journal-title":"Sci. China Ser. E: Technol. Sci."},{"key":"13_CR311","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1057","DOI":"10.1007\/3-540-64359-1_771","volume-title":"Parallel and Distributed Processing","author":"R Lichtenecker","year":"1998","unstructured":"Lichtenecker, R., Gotthardt, K., Zalewski, J.: Automated verifications of communication protocols using CCS and BDDs. In: Rolim, J. (ed.) IPPS 1998. LNCS, vol. 1388, pp. 1057\u20131066. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-64359-1_771"},{"key":"13_CR312","unstructured":"Lin, H.: A verification tool for value-passing processes. In: Danthine, A.A.S., Leduc, G., Wolper, P. (eds.) Proceedings of the IFIP TC6\/WG6.1 13th International Symposium on Protocol Specification, Testing and Verification (PSTV 1993), Li\u00e8ge, Belgium. IFIP Transactions, vol. C-16, pp. 79\u201392. North-Holland, May 1993"},{"key":"13_CR313","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-61604-7_47","volume-title":"CONCUR \u201996: Concurrency Theory","author":"H Lin","year":"1996","unstructured":"Lin, H.: Symbolic transition graph with assignment. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 50\u201365. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61604-7_47"},{"issue":"1","key":"13_CR314","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF02951922","volume":"15","author":"H Lin","year":"2000","unstructured":"Lin, H.: Computing bisimulations for finite-control pi-calculus. J. Comput. Sci. Technol. 15(1), 1\u20139 (2000)","journal-title":"J. Comput. Sci. Technol."},{"key":"13_CR315","unstructured":"Logrippo, L., Andriantsiferana, L., Ghribi, B.: Prototyping and formal requirement validation of GPRS: a mobile data packet radio service for GSM. In: Weinstock, C.B., Rushby, J. (eds.) Proceedings of the 7th IFIP International Working Conference on Dependable Computing for Critical Applications (DCCA-7), San Jose, CA, USA, January 1999"},{"key":"13_CR316","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-540-24611-4_3","volume-title":"Validation of Stochastic Systems","author":"N L\u00f3pez","year":"2004","unstructured":"L\u00f3pez, N., N\u00fa\u00f1ez, M.: An overview of probabilistic process algebras and their equivalences. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 89\u2013123. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24611-4_3"},{"issue":"2","key":"13_CR317","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.ic.2002.08.001","volume":"191","author":"G L\u00fcttgen","year":"2004","unstructured":"L\u00fcttgen, G., Vogler, W.: Bisimulation on speed: worst-case efficiency. Inf. Comput. 191(2), 105\u2013144 (2004)","journal-title":"Inf. Comput."},{"key":"13_CR318","unstructured":"Luukkainen, M., Ahtiainen, A.: Compositional verification of large SDL systems. In: Proceedings of the 1st Workshop of the SDL Forum Society on SDL and MSC (SAM 1998), Berlin, Germany, June 1998"},{"key":"13_CR319","first-page":"110","volume":"47","author":"E Madelaine","year":"1992","unstructured":"Madelaine, E.: Verification tools from the CONCUR project. EATCS Bull. 47, 110\u2013120 (1992)","journal-title":"EATCS Bull."},{"key":"13_CR320","unstructured":"Madelaine, E., Simone, R.: ECRINS: un laboratoire de preuve pour les calculs de processus. Rapport de recherche 672, INRIA, May 1987"},{"key":"13_CR321","unstructured":"Madelaine, E., Vergamini, D.: AUTO: a verification tool for distributed systems using reduction of finite automata networks. In: Vuong, S.T. (ed.) Proceedings of the 2nd IFIP International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE\u201989), Vancouver, BC, Canada, pp. 61\u201366. North-Holland, December 1989"},{"key":"13_CR322","doi-asserted-by":"crossref","unstructured":"Madelaine, E., Vergamini, D.: Specification and verification of a sliding window protocol in LOTOS. In: Parker, K.R., Rose, G.A. (eds.) Formal Description Techniques, IV, Proceedings of the IFIP TC6\/WG6.1 4th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE 1991), Sydney, Australia. IFIP Transactions, vol. C-2, pp. 495\u2013510. North-Holland, November 1991","DOI":"10.1016\/B978-0-444-89402-1.50045-X"},{"key":"13_CR323","doi-asserted-by":"crossref","unstructured":"Madelaine, E., Vergamini, D.: Tool demonstration: tools for process algebras. In: Parker, K.R., Rose, G.A. (eds.) Formal Description Techniques, IV, Proceedings of the IFIP TC6\/WG6.1 4th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE 1991), Sydney, Australia. IFIP Transactions, vol. C-2, pp. 463\u2013466. North-Holland, November 1991","DOI":"10.1016\/B978-0-444-89402-1.50041-2"},{"key":"13_CR324","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1007\/3-540-55210-3_221","volume-title":"STACS 92","author":"E Madelaine","year":"1992","unstructured":"Madelaine, E., Vergamini, D.: Verification of communicating processes by means of automata reduction and abstraction. In: Finkel, A., Jantzen, M. (eds.) STACS 1992. LNCS, vol. 577, pp. 613\u2013614. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55210-3_221"},{"key":"13_CR325","volume-title":"Concurrency: State Models and Java Programs","author":"J Magee","year":"1999","unstructured":"Magee, J., Kramer, J.: Concurrency: State Models and Java Programs. Wiley, Hoboken (1999)"},{"key":"13_CR326","doi-asserted-by":"crossref","unstructured":"Malhotra, J., Smolka, S.A., Giacalone, A., Shapiro, R.: A tool for hierarchical design and simulation of concurrent systems. In: Proceedings of the BCS-FACS Workshop on Specification and Verification of Concurrent Systems, Stirling, Scotland, UK, pp. 140\u2013152. British Computer Society, July 1988","DOI":"10.1007\/978-1-4471-3534-0_7"},{"key":"13_CR327","unstructured":"Markopoulos, P., Rowson, J., Johnson, P.: Dialogue modelling in the framework of an interactor model. In: Bodart, F., Vanderdonckt, J. (eds.) Proceedings of the 3rd International Workshop on Design, Specification, and Verification of Interactive Systems DSV-IS 1996 (Namur, Belgium). University of Namur, June 1996"},{"key":"13_CR328","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-030-90636-8_7","volume-title":"Formal Aspects of Component Software","author":"J Martens","year":"2021","unstructured":"Martens, J., Groote, J.F., van den Haak, L., Hijma, P., Wijs, A.: A linear parallel algorithm to compute bisimulation and relational coarsest partitions. In: Sala\u00fcn, G., Wijs, A. (eds.) FACS 2021. LNCS, vol. 13077, pp. 115\u2013133. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90636-8_7"},{"key":"13_CR329","unstructured":"Mateescu, R.: Formal description and analysis of a bounded retransmission protocol. In: Brezo\u010dnik, Z., Kapus, T. (eds.) Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design (Maribor, Slovenia), pp. 98\u2013113. University of Maribor, Slovenia, June 1996. Also available as INRIA Research Report RR-2965"},{"issue":"6","key":"13_CR330","first-page":"725","volume":"16","author":"R Mateescu","year":"1997","unstructured":"Mateescu, R.: V\u00e9rification de syst\u00e8mes r\u00e9partis: l\u2019exemple du protocole BRP. Technique et Science Informatiques 16(6), 725\u2013751 (1997)","journal-title":"Technique et Science Informatiques"},{"key":"13_CR331","unstructured":"Mateescu, R.: Local model-checking of an alternation-free value-based modal mu-calculus. In: Bossi, A., Cortesi, A., Levi, F. (eds.) Proceedings of the 2nd International Workshop on Verification, Model Checking and Abstract Interpretation (VMCAI 1998), Pisa, Italy. University Ca\u2019 Foscari of Venice, September 1998"},{"key":"13_CR332","unstructured":"Mateescu, R.: V\u00e9rification des propri\u00e9t\u00e9s temporelles des programmes parall\u00e8les. Ph.D. thesis, Institut National Polytechnique de Grenoble, April 1998"},{"key":"13_CR333","doi-asserted-by":"crossref","unstructured":"Mateescu, R.: On-the-fly state space reductions for weak equivalences. In: Margaria, T., Massink, M. (eds.) Proceedings of the 10th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2005), Lisbon, Portugal, pp. 80\u201389. ERCIM, ACM Computer Society Press, September 2005","DOI":"10.1145\/1081180.1081191"},{"key":"13_CR334","doi-asserted-by":"crossref","unstructured":"Mateescu, R.: CAESAR_SOLVE: a generic library for on-the-fly resolution of alternation-free Boolean equation systems. Int. J. Softw. Tools Technol. Transfer (STTT) 8(1), 37\u201356 (2006). Full version available as INRIA Research Report RR-5948, July 2006","DOI":"10.1007\/s10009-005-0194-9"},{"key":"13_CR335","doi-asserted-by":"crossref","unstructured":"Mateescu, R.: Specification and analysis of asynchronous systems using CADP. In: Merz, S., Navet, N. (eds.) Modeling and Verification of Real-Time Systems - Formalisms and Software Tools, chap. 5, pp. 141\u2013170. ISTE Publishing\/Wiley (2008)","DOI":"10.1002\/9780470611012.ch5"},{"key":"13_CR336","doi-asserted-by":"crossref","unstructured":"Mateescu, R., Oudot, E.: Bisimulator 2.0: an on-the-fly equivalence checker based on Boolean equation systems. In: Proceedings of the 6th ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2008), Anaheim, CA, USA, pp. 73\u201374. IEEE Computer Society Press, June 2008","DOI":"10.1109\/MEMCOD.2008.4547690"},{"key":"13_CR337","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-540-85114-1_15","volume-title":"Model Checking Software","author":"R Mateescu","year":"2008","unstructured":"Mateescu, R., Oudot, E.: Improved on-the-fly equivalence checking using Boolean equation systems. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 196\u2013213. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85114-1_15 Full version available as INRIA Research Report RR-6777"},{"key":"13_CR338","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-89652-4_10","volume-title":"Service-Oriented Computing \u2013 ICSOC 2008","author":"R Mateescu","year":"2008","unstructured":"Mateescu, R., Poizat, P., Sala\u00fcn, G.: Adaptation of service protocols using process algebra and on-the-fly reduction techniques. In: Bouguettaya, A., Krueger, I., Margaria, T. (eds.) ICSOC 2008. LNCS, vol. 5364, pp. 84\u201399. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89652-4_10"},{"issue":"3","key":"13_CR339","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1016\/j.scico.2014.04.004","volume":"96","author":"R Mateescu","year":"2014","unstructured":"Mateescu, R., Wijs, A.: Property-dependent reductions adequate with divergence-sensitive branching bisimilarity. Sci. Comput. Program. 96(3), 354\u2013376 (2014)","journal-title":"Sci. Comput. Program."},{"key":"13_CR340","unstructured":"Mehta, M., Guha, S.: ReLTS 1.0 User Manual (2014). http:\/\/airbornemihir.github.io\/lts_reltool\/manual.pdf"},{"key":"13_CR341","unstructured":"Mehta, M., Guha, S., Arun-Kumar, S.: ReLTS: A Tool for Checking Generalized Behavioural Relations over LTSs (2014). http:\/\/airbornemihir.github.io\/lts_reltool\/NFM.pdf"},{"issue":"2","key":"13_CR342","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1145\/3318.3322","volume":"7","author":"GJ Milne","year":"1985","unstructured":"Milne, G.J.: CIRCAL and the representation of communication, concurrency, and time. ACM Trans. Progr. Lang. Syst. 7(2), 270\u2013298 (1985)","journal-title":"ACM Trans. Progr. Lang. Syst."},{"issue":"1","key":"13_CR343","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes I. Inf. Comput. 100(1), 1\u201340 (1992)","journal-title":"Inf. Comput."},{"issue":"1","key":"13_CR344","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/0890-5401(92)90009-5","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes II. Inf. Comput. 100(1), 41\u201377 (1992)","journal-title":"Inf. Comput."},{"key":"13_CR345","doi-asserted-by":"publisher","unstructured":"Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3","DOI":"10.1007\/3-540-10235-3"},{"key":"13_CR346","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R Milner","year":"1983","unstructured":"Milner, R.: Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25, 267\u2013310 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR347","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall (1989)"},{"key":"13_CR348","unstructured":"Moller, F.: The Edinburgh Concurrency Workbench (Version 6.1). User manual, Laboratory for the Foundations of Computer Science, University of Edinburgh (1992)"},{"issue":"2","key":"13_CR349","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/j.ic.2004.06.003","volume":"194","author":"F Moller","year":"2004","unstructured":"Moller, F., Smolka, S.A., Srba, J.: On the computational complexity of bisimulation. Redux. Inf. Comput. 194(2), 129\u2013143 (2004)","journal-title":"Redux. Inf. Comput."},{"key":"13_CR350","unstructured":"Montes, A.S.: VENUS: un outil d\u2019aide \u00e0 la v\u00e9rification des syst\u00e8mes communicants. Ph.D. thesis, Institut National Polytechnique de Grenoble, January 1987"},{"key":"13_CR351","unstructured":"Mounier, L.: M\u00e9thodes de v\u00e9rification de sp\u00e9cifications comportementales: \u00e9tude et mise en \u0153uvre. Ph.D. thesis, Universit\u00e9 Joseph Fourier (Grenoble), January 1992"},{"issue":"2","key":"13_CR352","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1142\/S012905411340011X","volume":"24","author":"M Mumme","year":"2013","unstructured":"Mumme, M., Ciardo, G.: An efficient fully symbolic bisimulation algorithm for non-deterministic systems. Int. J. Found. Comput. Sci. 24(2), 263\u2013282 (2013)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"13_CR353","unstructured":"Najm, E., Budkowski, S., Gilot, T., Lumbroso, L.: General presentation of SCAN - a distributed systems modelling and validation tool. In: Diaz, M. (ed.) Proceedings of the 5th IFIP International Workshop on Protocol Specification, Testing, and Verification (PSTV 1985), Moissac, France, pp. 103\u2013118. North-Holland, June 1985"},{"key":"13_CR354","doi-asserted-by":"crossref","unstructured":"Nistal, M.L., Quemada, J., Iglesias, M.J.F.: Direct verification of bisimulations. In: Gotzhein, R., Bredereke, J. (eds.) Formal Description Techniques IX: Theory, application and tools, IFIP TC6 WG6.1 International Conference on Formal Description Techniques IX\/Protocol Specification, Testing and Verification XVI, Kaiserslautern, Germany, 8\u201311 October 1996. IFIP Conference Proceedings, vol. 69, pp. 349\u2013363. Chapman & Hall (1996)","DOI":"10.1007\/978-0-387-35079-0_22"},{"key":"13_CR355","unstructured":"Notare, M.S.M.A., da Silva Cruz, F.A., Riso, B.G., Westphall, C.B.: Wireless communications: security management against cloned cellular phones. In: Proceedings of the IEEE Wireless Communications and Networking Conference WCNC 1999 (New Orleans, LA, USA), pp. 1412\u20131416. IEEE, September 1999"},{"key":"13_CR356","doi-asserted-by":"crossref","unstructured":"Notare, M., Boukerche, A., Cruz, F., Riso, B., Westphall, C.: Security management against cloning mobile phones. In: Seamless Interconnection for Universal Services, Global Telecommunications Conference, GLOBECOM 1999 (Cat. No.99CH37042), vol. 3, pp. 1969\u20131973 (1999)","DOI":"10.1109\/GLOCOM.1999.832514"},{"key":"13_CR357","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-319-15317-9_18","volume-title":"Formal Aspects of Component Software","author":"M Noureddine","year":"2015","unstructured":"Noureddine, M., Jaber, M., Bliudze, S., Zaraket, F.A.: Reduction and abstraction techniques for BIP. In: Lanese, I., Madelaine, E. (eds.) FACS 2014. LNCS, vol. 8997, pp. 288\u2013305. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15317-9_18"},{"key":"13_CR358","unstructured":"Orzan, S.: On distributed verification and verified distribution. Ph.D. thesis, Vrije Universiteit Amsterdam (2004)"},{"issue":"3","key":"13_CR359","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.entcs.2004.10.017","volume":"128","author":"S Orzan","year":"2005","unstructured":"Orzan, S., van de Pol, J., Espada, M.V.: A state space distribution policy based on abstract interpretation. Electron. Notes Theor. Comput. Sci. 128(3), 35\u201345 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"6","key":"13_CR360","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973\u2013989 (1987)","journal-title":"SIAM J. Comput."},{"key":"13_CR361","unstructured":"Parashkevov, A.N., Yantchev, J.: ARC - a verification tool for concurrent systems. In: Proceedings of the 3rd Australasian Parallel and Real-Time Conference (1996)"},{"key":"13_CR362","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167\u2013183. Springer, Heidelberg (1981). https:\/\/doi.org\/10.1007\/BFb0017309"},{"key":"13_CR363","doi-asserted-by":"crossref","unstructured":"Parrow, J., Victor, B.: The fusion calculus: expressiveness and symmetry in mobile processes. In: 13th Annual IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana, USA, 21\u201324 June 1998, pp. 176\u2013185. IEEE Computer Society (1998)","DOI":"10.1109\/LICS.1998.705654"},{"key":"13_CR364","unstructured":"Pecheur, C.: Advanced Modelling and Verification Techniques Applied to a Cluster File System. Research Report RR-3416, INRIA, Grenoble, May 1998"},{"key":"13_CR365","unstructured":"Pecheur, C.: Advanced modelling and verification techniques applied to a cluster file system. In: Hall, R.J., Tyugu, E. (eds.) Proceedings of the 14th IEEE International Conference on Automated Software Engineering (ASE 1999), Cocoa Beach, Florida, USA. IEEE Computer Society, October 1999. Extended version available as INRIA Research Report RR-3416"},{"key":"13_CR366","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-24730-2_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Piazza","year":"2004","unstructured":"Piazza, C., Pivato, E., Rossi, S.: CoPS \u2013 checker of persistent security. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 144\u2013152. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_11"},{"key":"13_CR367","unstructured":"Plotkin, G.: A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Denmark (1981)"},{"key":"13_CR368","first-page":"17","volume":"60\u201361","author":"GD Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Logic Algebraic Program. 60\u201361, 17\u2013139 (2004)","journal-title":"J. Logic Algebraic Program."},{"key":"13_CR369","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jlap.2004.03.009","volume":"60\u201361","author":"GD Plotkin","year":"2004","unstructured":"Plotkin, G.D.: The origins of structural operational semantics. J. Logic Algebraic Program. 60\u201361, 3\u201315 (2004)","journal-title":"J. Logic Algebraic Program."},{"issue":"6","key":"13_CR370","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1007\/s00165-019-00497-w","volume":"31","author":"D Pous","year":"2019","unstructured":"Pous, D., Sangiorgi, D.: Bisimulation and coinduction enhancements: a historical perspective. Formal Aspects of Comput. 31(6), 733\u2013749 (2019)","journal-title":"Formal Aspects of Comput."},{"key":"13_CR371","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/3-540-55719-9_115","volume-title":"Automata, Languages and Programming","author":"A Rabinovich","year":"1992","unstructured":"Rabinovich, A.: Checking equivalences between concurrent systems of finite agents (extended abstract). In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 696\u2013707. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55719-9_115"},{"key":"13_CR372","unstructured":"van Rangelrooij, A., Voeten, J.P.M.: CCSTOOL2: An Expansion, Minimization and Verification Tool for Finite State CCS Descriptions. Research Report 94-E-284, Eindhoven University of Technology (1994)"},{"key":"13_CR373","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1016\/0920-5489(95)00002-C","volume":"17","author":"C Reade","year":"1995","unstructured":"Reade, C.: Process algebra in the specification of graphics standards. Comput. Standards Interfaces 17, 277\u2013290 (1995)","journal-title":"Comput. Standards Interfaces"},{"key":"13_CR374","unstructured":"Romijn, J.: Analysing industrial protocols with formal methods. Ph.D. thesis, University of Twente, The Netherlands, September 1999"},{"key":"13_CR375","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall (1998)"},{"key":"13_CR376","doi-asserted-by":"crossref","unstructured":"Roy, V., de Simone, R.: Auto\/Autograph. In: Kurshan, R.P., Clarke, E.M. (eds.) Proceedings of the 2nd Workshop on Computer-Aided Verification (Rutgers, New Jersey, USA). DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 3, pp. 477\u2013491. AMS-ACM, June 1990","DOI":"10.1090\/dimacs\/003\/29"},{"issue":"2\/3","key":"13_CR377","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/BF00121126","volume":"1","author":"V Roy","year":"1992","unstructured":"Roy, V., de Simone, R.: Auto\/Autograph. Formal Methods Syst. Des. 1(2\/3), 239\u2013249 (1992)","journal-title":"Formal Methods Syst. Des."},{"key":"13_CR378","first-page":"373","volume":"2","author":"H Rudin","year":"1978","unstructured":"Rudin, H., West, C.H., Zafiropulo, P.: Automated protocol validation: one chain of development. Comput. Netw. 2, 373\u2013380 (1978)","journal-title":"Comput. Netw."},{"issue":"9","key":"13_CR379","doi-asserted-by":"publisher","first-page":"940","DOI":"10.1109\/26.35374","volume":"37","author":"KK Sabnani","year":"1989","unstructured":"Sabnani, K.K., Lapone, A.M., \u00dcmit Uyar, M.: An algorithmic procedure for checking safety properties of protocols. IEEE Trans. Commun. 37(9), 940\u2013948 (1989)","journal-title":"IEEE Trans. Commun."},{"key":"13_CR380","unstructured":"Sage, M., Johnson, C.W.: A declarative prototyping environment for the development of multi-user safety-critical systems. In: Proceedings of the 17th International System Safety Conference (ISSC 1999), Orlando, Florida, USA. System Safety Society, August 1999"},{"key":"13_CR381","unstructured":"Sage, M., Johnson, C.W.: Formally verified rapid prototyping for air traffic control. In: Proceedings of the 3rd Workshop on Human Error, Safety and Systems Development, Liege, Belgium (1999)"},{"issue":"2","key":"13_CR382","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/S0951-8320(01)00089-8","volume":"75","author":"M Sage","year":"2002","unstructured":"Sage, M., Johnson, C.W.: Formally verified rapid prototyping for air traffic control. Reliab. Eng. Syst. Saf. 75(2), 121\u2013132 (2002)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"13_CR383","unstructured":"Sanderson, M.T.: Proof Techniques for CCS. Internal Report CST-19-82, University of Edinburgh (1982)"},{"key":"13_CR384","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-57208-2_10","volume-title":"CONCUR\u201993","author":"D Sangiorgi","year":"1993","unstructured":"Sangiorgi, D.: A theory of bisimulation for the $$\\pi $$-calculus. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 127\u2013142. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57208-2_10"},{"key":"13_CR385","unstructured":"Saqui-Sannes, P., Courtiat, J.P.: From the simulation to the verification of ESTELLE$$^*$$ specifications. In: Vuong, S.T. (ed.) Proceedings of the 2nd International Conference on Formal Description Techniques FORTE 1989 (Vancouver B.C., Canada). North-Holland, December 1989"},{"key":"13_CR386","unstructured":"Schieferdecker, I.: Abruptly-terminated connections in TCP - a verification example. In: Brezo\u010dnik, Z., Kapus, T. (eds.) Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design, Maribor, Slovenia, pp. 136\u2013145. University of Maribor, Slovenia, June 1996"},{"key":"13_CR387","unstructured":"Sighireanu, M.: Model-checking validation of the LOTOS descriptions of the invoicing case study. In: Habrias, H. (ed.) Proceedings of the International Workshop on Comparing System Specification Techniques (Nantes, France), March 1998"},{"key":"13_CR388","doi-asserted-by":"crossref","unstructured":"Sighireanu, M., Mateescu, R.: Validation of the link layer protocol of the IEEE-1394 serial bus (\u201cFireWire\u201d): an experiment with E-LOTOS. In: Lovrek, I. (ed.) Proceedings of the 2nd COST 247 International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia), June 1997. Full version available as INRIA Research Report RR-3172","DOI":"10.1007\/s100090050018"},{"key":"13_CR389","unstructured":"Sighireanu, M., Turner, K.: Requirement Capture, Formal Description and Verification of an Invoicing System. Research Report RR-3575, INRIA, Grenoble, December 1998"},{"key":"13_CR390","unstructured":"de Simone, R., Vergamini, D.: Aboard AUTO. Technical Report 111, INRIA (1989)"},{"key":"13_CR391","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24611-4_1","volume-title":"Validation of Stochastic Systems","author":"A Sokolova","year":"2004","unstructured":"Sokolova, A., de Vink, E.P.: Probabilistic automata: system types, parallel composition and comparison. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 1\u201343. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24611-4_1"},{"key":"13_CR392","doi-asserted-by":"crossref","unstructured":"Song, L., Zhang, L., Hermanns, H., Godskesen, J.C.: Incremental bisimulation abstraction refinement. ACM Trans. Embed. Comput. Syst. 13(4s), 142:1\u2013142:23 (2014)","DOI":"10.1145\/2627352"},{"key":"13_CR393","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/BFb0035867","volume-title":"STACS 88","author":"A Soriano","year":"1988","unstructured":"Soriano, A.: Prototype de Venus: Un Outil d\u2019Aide \u00e0 la V\u00e9rification de Syst\u00e8mes Communicants. In: Cori, R., Wirsing, M. (eds.) STACS 1988. LNCS, vol. 294, pp. 401\u2013402. Springer, Heidelberg (1988). https:\/\/doi.org\/10.1007\/BFb0035867"},{"key":"13_CR394","unstructured":"Stevens, P.: The Edinburgh Concurrency Workbench (Version 7.1). User manual, Laboratory for the Foundations of Computer Science, University of Edinburgh (1997)"},{"issue":"2","key":"13_CR395","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s100090050019","volume":"2","author":"P Stevens","year":"1998","unstructured":"Stevens, P.: A verification tool developer\u2019s Vade Mecum. Int. J. Softw. Tools Technol. Transfer (STTT) 2(2), 89\u201394 (1998)","journal-title":"Int. J. Softw. Tools Technol. Transfer (STTT)"},{"key":"13_CR396","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/3-540-49059-0_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Stevens","year":"1999","unstructured":"Stevens, P.: Some issues in the software engineering of verification tools. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 435\u2013438. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_30"},{"issue":"4\u20135","key":"13_CR397","first-page":"346","volume":"2","author":"CA Sunshine","year":"1978","unstructured":"Sunshine, C.A.: Survey of protocol definition and verification techniques. Comput. Netw. 2(4\u20135), 346\u2013350 (1978)","journal-title":"Comput. Netw."},{"key":"13_CR398","unstructured":"Tai, K.C., Koppol, P.V.: An incremental approach to reachability analysis of distributed programs. In: Proceedings of the 7th International Workshop on Software Specification and Design, Los Angeles, CA, USA, pp. 141\u2013150. IEEE Press, Piscataway, December 1993"},{"key":"13_CR399","doi-asserted-by":"crossref","unstructured":"Tai, K.C., Koppol, P.V.: Hierarchy-based incremental reachability analysis of communication protocols. In: Proceedings of the IEEE International Conference on Network Protocols, San Francisco, CA, USA, pp. 318\u2013325. IEEE Press, Piscataway, October 1993","DOI":"10.1109\/ICNP.1993.340896"},{"key":"13_CR400","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-319-47958-3_5","volume-title":"Programming Languages and Systems","author":"A Tiu","year":"2016","unstructured":"Tiu, A., Nguyen, N., Horne, R.: SPEC: an equivalence checker for security protocols. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 87\u201395. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47958-3_5"},{"key":"13_CR401","unstructured":"Tripakis, S.: Extended KRONOS\/CADP Tool: Minimization, On-the-Fly Verification and Compositionality. Technical Report T226, VERIMAG, Grenoble, France, April 1999"},{"key":"13_CR402","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-61474-5_72","volume-title":"Computer Aided Verification","author":"S Tripakis","year":"1996","unstructured":"Tripakis, S., Yovine, S.: Analysis of timed systems based on time-abstracting bisimulations. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 232\u2013243. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_72"},{"key":"13_CR403","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-540-39958-2_17","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"F Tronel","year":"2003","unstructured":"Tronel, F., Lang, F., Garavel, H.: Compositional verification using CADP of the ScalAgent deployment protocol for software components. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 244\u2013260. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39958-2_17 Full version available as INRIA Research Report RR-5012"},{"key":"13_CR404","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-60729-5_11","volume-title":"Kommunikation in Verteilten Systemen","author":"A Ulrich","year":"1997","unstructured":"Ulrich, A.: A description model to support test suite derivation for concurrent systems. In: Zitterbart, M. (ed.) KiVS 1997, pp. 151\u2013166. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/978-3-642-60729-5_11"},{"key":"13_CR405","doi-asserted-by":"crossref","unstructured":"Ulrich, A., K\u00f6nig, H.: Specification-based testing of concurrent systems. In: Higashino, T., Togashi, A. (eds.) Proceedings of the IFIP Joint International Conference on Formal Description Techniques and Protocol Specification, Testing, and Verification (FORTE\/PSTV 1997), Ozaka, Japan. Chapman & Hall, November 1997","DOI":"10.1007\/978-0-387-35271-8_1"},{"key":"13_CR406","unstructured":"Valmari, A., Tienari, M.: An improved failure equivalence for finite-state systems with a reduction algorithm. In: Jonsson, B., Parrow, J., Pehrson, B. (eds.) Proceedings of the 11th IFIP International Workshop on Protocol Specification, Testing and Verification (Stockholm, Sweden). North-Holland, June 1991"},{"key":"13_CR407","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/3-540-56689-9_54","volume-title":"Advances in Petri Nets 1993","author":"A Valmari","year":"1993","unstructured":"Valmari, A.: Compositional state space generation. In: Rozenberg, G. (ed.) ICATPN 1991. LNCS, vol. 674, pp. 427\u2013457. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56689-9_54"},{"key":"13_CR408","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Stubborn set methods for process algebras. In: Peled, D.A., Pratt, V.R., Holzmann, G.J. (eds.) Proceedings of the DIMACS Workshop on Partial Order Methods in Verification, Princeton, New Jersey, USA. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29, pp. 213\u2013231. DIMACS\/AMS, July 1996","DOI":"10.1090\/dimacs\/029\/12"},{"key":"13_CR409","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1007\/BFb0024669","volume-title":"FME \u201993: Industrial-Strength Formal Methods","author":"A Valmari","year":"1993","unstructured":"Valmari, A., Kemppainen, J., Clegg, M., Levanto, M.: Putting advanced reachability analysis techniques together: The \u201cARA\u2019\u2019 tool. In: Woodcock, J.C.P., Larsen, P.G. (eds.) FME 1993. LNCS, vol. 670, pp. 597\u2013616. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/BFb0024669"},{"key":"13_CR410","unstructured":"Vergamini, D.: Verification by Means of Observational Equivalence on Automata. Research Report 0501, INRIA (1986)"},{"key":"13_CR411","unstructured":"Vergamini, D.: V\u00e9rification de r\u00e9seaux d\u2019automates finis par \u00e9quivalences observationnelles: le syst\u00e8me AUTO. Ph.D. thesis, Universit\u00e9 de Nice (1987)"},{"key":"13_CR412","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/BFb0013124","volume-title":"Formal Properties of Finite Automata and Applications","author":"D Vergamini","year":"1989","unstructured":"Vergamini, D.: Verification of distributed systems: an experiment. In: Pin, J.E. (ed.) LITP 1988. LNCS, vol. 386, pp. 249\u2013259. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/BFb0013124"},{"key":"13_CR413","unstructured":"Victor, B.: A verification tool for the polyadic $$\\pi $$-calculus. Licentiate thesis, Department of Computer Systems, Uppsala University, Sweden, May 1994. Available as report DoCS 94\/50"},{"key":"13_CR414","unstructured":"Victor, B.: The Mobility Workbench User\u2019s Guide, Polyadic version 3.122 (1995)"},{"key":"13_CR415","unstructured":"Victor, B.: The fusion calculus: expressiveness and symmetry in mobile processes. Ph.D. thesis, Department of Computer Systems, Uppsala University, Sweden, June 1998. Available as report DoCS 98\/98"},{"key":"13_CR416","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/3-540-58179-0_73","volume-title":"Computer Aided Verification","author":"B Victor","year":"1994","unstructured":"Victor, B., Moller, F.: The Mobility Workbench\u2014a tool for the $$\\pi $$-calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 428\u2013440. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58179-0_73"},{"key":"13_CR417","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-540-24730-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Virtanen","year":"2004","unstructured":"Virtanen, H., Hansen, H., Valmari, A., Nieminen, J., Erkkil\u00e4, T.: Tampere verification tool. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 153\u2013157. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_12"},{"key":"13_CR418","unstructured":"Walker, D.: Automated Analysis of Mutual Exclusion Algorithms using CCS. Research Report ECS-LFCS-89-91, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburg (1989)"},{"key":"13_CR419","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-642-00602-9_40","volume-title":"Hybrid Systems: Computation and Control","author":"F Wang","year":"2009","unstructured":"Wang, F.: Symbolic branching bisimulation-checking of dense-time systems in an environment. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 485\u2013489. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00602-9_40"},{"key":"13_CR420","doi-asserted-by":"crossref","unstructured":"Wehrheim, H.: Partial order reductions for failures refinement. In: Castellani, I., Victor, B. (eds.) 6th International Workshop on Expressiveness in Concurrency (EXPRESS 1999), Eindhoven, The Netherlands. Electronic Notes in Theoretical Computer Science, vol. 27, pp. 71\u201384. Elsevier, August 1999","DOI":"10.1016\/S1571-0661(05)80296-8"},{"key":"13_CR421","unstructured":"Willemse, T., Tretmans, J., Klomp, A.: A case study in formal methods: specification and validation of the OM\/RR protocol. In: Gnesi, S., Schieferdecker, I., Rennoch, A. (eds.) Proceedings of the 5th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2000), Berlin, Germany, pp. 331\u2013344. GMD Report 91, Berlin, April 2000"},{"key":"13_CR422","unstructured":"Willemse, T.A.: The specification and validation of the OM\/RR-protocol. Master\u2019s thesis, Department of Mathematics and Computing Science, Eindhoven University of Technology, Eindhoven, The Netherlands, June 1998"},{"key":"13_CR423","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Derisavi, S., Hermanns, H.: Symbolic partition refinement with dynamic balancing of time and space. In: Proceedings of the 5th International Conference on the Quantitative Evaluation of Systems (QEST 2008), Saint-Malo, France, pp. 65\u201374. IEEE Computer Society, September 2008","DOI":"10.1109\/QEST.2008.14"},{"key":"13_CR424","unstructured":"Wimmer, R., Herbstritt, M., Becker, B.: Minimization of large state spaces using symbolic branching bisimulation. In: Reorda, M.S., et al. (eds.) Proceedings of the 9th IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS 2006), Prague, Czech Republic, pp. 9\u201314. IEEE Computer Society, April 2006"},{"key":"13_CR425","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Herbstritt, M., Becker, B.: Optimization techniques for BDD-based bisimulation computation. In: Zhou, H., Macii, E., Yan, Z., Massoud, Y. (eds.) Proceedings of the 17th ACM Great Lakes Symposium on VLSI, Stresa, Lago Maggiore, pp. 405\u2013410. ACM, March 2007","DOI":"10.1145\/1228784.1228880"},{"key":"13_CR426","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/11901914_35","volume-title":"Automated Technology for Verification and Analysis","author":"R Wimmer","year":"2006","unstructured":"Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B.: Sigref \u2013 a symbolic bisimulation tool box. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 477\u2013492. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11901914_35"},{"key":"13_CR427","doi-asserted-by":"crossref","unstructured":"Wodey, P., Baray, F.: Linking codesign and verification by means of E-LOTOS FDT. In: J\u00f3zwiak, L. (ed.) Proceedings of the Euromicro Workshop on Digital System Design: Architectures, Methods and Tools (Milano, Italy). IEEE, September 1999","DOI":"10.1109\/EURMIC.1999.794515"},{"key":"13_CR428","doi-asserted-by":"crossref","unstructured":"Yeh, W.J., Young, M.: Compositional reachability analysis using process algebra. In: Proceedings of the ACM SIGSOFT Symposium on Testing, Analysis, and Verification (SIGSOFT 1991), Victoria, British Columbia, Canada, pp. 49\u201359. ACM Press, October 1991","DOI":"10.1145\/120807.120812"},{"key":"13_CR429","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/BFb0039080","volume-title":"CONCUR \u201990 Theories of Concurrency: Unification and Extension","author":"Y Wang","year":"1990","unstructured":"Wang, Y.: Real-time behaviour of asynchronous agents. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 502\u2013520. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0039080"},{"key":"13_CR430","unstructured":"Yi, W.: A Tool Environment for the Development of Embedded Systems (1999)"},{"key":"13_CR431","unstructured":"Yoeli, M.: Modulo-3 Transition Counter: A Case Study in LOTOS-Based Verification. Technical Report TR CS0950, Technion, Computer Science Department, Haifa, Israel, February 1998"},{"key":"13_CR432","unstructured":"Yoeli, M.: Examples of LOTOS-Based Verification of Asynchronous Circuits. Technical Report TR CS-2001-08, Technion, Computer Science Department, Haifa, Israel, February 2001"},{"key":"13_CR433","unstructured":"Yoeli, M., Ginzburg, A.: LOTOS\/CADP-Based Verification of Asynchronous Circuits. Technical Report TR CS-2001-09, Technion, Computer Science Department, Haifa, Israel, March 2001"},{"issue":"1\/2","key":"13_CR434","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S Yovine","year":"1997","unstructured":"Yovine, S.: KRONOS: a verification tool for real-time systems. Int. J. Softw. Tools Technol. Transfer (STTT) 1(1\/2), 123\u2013133 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer (STTT)"},{"key":"13_CR435","unstructured":"Zapreev, I., Jansen, C.: MRMC Test Suite - Version 1.4.1 (2009). http:\/\/www.mrmc-tool.org\/downloads\/MRMC\/Specs\/TS_Manual_1.4.1.pdf"},{"key":"13_CR436","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/3-540-52148-8_10","volume-title":"Automatic Verification Methods for Finite State Systems","author":"H Zuidweg","year":"1990","unstructured":"Zuidweg, H.: Verification by abstraction and bisimulation. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 105\u2013116. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_10"}],"container-title":["Lecture Notes in Computer Science","A Journey from Process Algebra via Timed Automata to Model Learning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-15629-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,4]],"date-time":"2024-10-04T15:55:31Z","timestamp":1728057331000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-15629-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031156281","9783031156298"],"references-count":436,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-15629-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"7 September 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}