{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T04:08:45Z","timestamp":1750910925145,"version":"3.41.0"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319680330"},{"type":"electronic","value":"9783319680347"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-68034-7_7","type":"book-chapter","created":{"date-parts":[[2017,9,13]],"date-time":"2017-09-13T17:32:45Z","timestamp":1505323965000},"page":"117-136","source":"Crossref","is-referenced-by-count":5,"title":["Compositional Model Checking Is Lively"],"prefix":"10.1007","author":[{"given":"Sander","family":"de Putter","sequence":"first","affiliation":[]},{"given":"Anton","family":"Wijs","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,14]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Andersen, H.: Partial model checking. In: LICS, pp. 398\u2013407. IEEE Computer Society Press (1995)","DOI":"10.1109\/LICS.1995.523274"},{"issue":"3","key":"7_CR2","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/s100090050032","volume":"2","author":"H Andersen","year":"1999","unstructured":"Andersen, H.: Partial model checking of modal equations: a survey. STTT 2(3), 242\u2013259 (1999)","journal-title":"STTT"},{"key":"7_CR3","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"issue":"5","key":"7_CR4","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1109\/MC.2016.127","volume":"49","author":"H Bal","year":"2016","unstructured":"Bal, H., Epema, D., de Laat, C., van Nieuwpoort, R., Romein, J., Seinstra, F., Snoek, C., Wijshoff, H.: A medium-scale distributed system for computer science research: infrastructure for the long term. IEEE Comput. 49(5), 54\u201363 (2016)","journal-title":"IEEE Comput."},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq\u2019 Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"issue":"1","key":"7_CR6","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0304-3975(94)00152-9","volume":"146","author":"B Bloom","year":"1995","unstructured":"Bloom, B.: Structural operational semantics for weak bisimulations. Theor. Comput. Sci. 146(1), 25\u201368 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BFb0028741","volume-title":"Computer Aided Verification","author":"EM Clarke","year":"1998","unstructured":"Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 147\u2013158. Springer, Heidelberg (1998). doi: 10.1007\/BFb0028741"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: LICS, pp. 353\u2013362. IEEE Computer Society Press, June 1989","DOI":"10.1109\/LICS.1989.39190"},{"key":"7_CR9","volume-title":"Model Checking","author":"E Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"7_CR10","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., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., de Vink, E.P., Wesselink, W., Willemse, T.A.C.: 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). doi: 10.1007\/978-3-642-36742-7_15"},{"key":"7_CR11","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). doi: 10.1007\/978-3-642-19811-3_9"},{"issue":"4\u20135","key":"7_CR12","doi-asserted-by":"crossref","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\u20135), 337\u2013392 (2015)","journal-title":"Acta Informatica"},{"issue":"3","key":"7_CR13","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"RJ Glabbeek van","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":"7_CR14","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R., Luttik, S., Trc\u0306ka, N.: Computation tree logic with deadlock detection. LMCS 5(4) (2009)","DOI":"10.2168\/LMCS-5(4:5)2009"},{"issue":"4","key":"7_CR15","doi-asserted-by":"crossref","first-page":"371","DOI":"10.3233\/FI-2009-109","volume":"93","author":"R Glabbeek van","year":"2009","unstructured":"van Glabbeek, R., Luttik, S., Tr\u010dka, N.: Branching bisimilarity with explicit divergence. Fundam. Inf. 93(4), 371\u2013392 (2009)","journal-title":"Fundam. Inf."},{"key":"7_CR16","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). doi: 10.1007\/978-3-662-49674-9_40"},{"issue":"2","key":"7_CR17","doi-asserted-by":"crossref","first-page":"13:1","DOI":"10.1145\/3060140","volume":"18","author":"J Groote","year":"2017","unstructured":"Groote, J., Jansen, D., Keiren, J., Wijs, A.: An $$O(m \\log n)$$ algorithm for computing stuttering equivalence and branching bisimulation. ACM Trans. Comput. Logic 18(2), 13:1\u201313:34 (2017)","journal-title":"ACM Trans. Comput. Logic"},{"key":"7_CR18","unstructured":"ISO\/IEC: LOTOS \u2013 A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization \u2013 Information Processing Systems \u2013 Open Systems Interconnection (1989)"},{"key":"7_CR19","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$ -calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR20","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). doi: 10.1007\/BFb0035392"},{"key":"7_CR21","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). doi: 10.1007\/11589976_6"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/11888116_13","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006","author":"F Lang","year":"2006","unstructured":"Lang, F.: Refined interfaces for compositional verification. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 159\u2013174. Springer, Heidelberg (2006). doi: 10.1007\/11888116_13"},{"key":"7_CR23","unstructured":"Lang, F.: Unpublished textual and PVS proof that branching bisimulation is a congruence for Networks of LTSs. This proof does not consider DPBB. Personal Communication (2016)"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1007\/BFb0084815","volume-title":"CONCUR \u201992","author":"F Maraninchi","year":"1992","unstructured":"Maraninchi, F.: Operational and compositional semantics of synchronous automaton compositions. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 550\u2013564. Springer, Heidelberg (1992). doi: 10.1007\/BFb0084815"},{"issue":"3","key":"7_CR25","doi-asserted-by":"crossref","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":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/11841197_17","volume-title":"Web Services and Formal Methods","author":"M Mazzara","year":"2006","unstructured":"Mazzara, M., Lanese, I.: Towards a unifying theory for web services composition. In: Bravetti, M., N\u00fa\u00f1ez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 257\u2013272. Springer, Heidelberg (2006). doi: 10.1007\/11841197_17"},{"key":"7_CR27","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, New York (1989)"},{"key":"7_CR28","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 Nicola De","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). doi: 10.1007\/3-540-53479-2_17"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73370-6_17","volume-title":"Model Checking Software","author":"R Pel\u00e1nek","year":"2007","unstructured":"Pel\u00e1nek, R.: BEEM: benchmarks for explicit model checkers. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263\u2013267. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-73370-6_17"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/BFb0028727","volume-title":"Computer Aided Verification","author":"D Peled","year":"1998","unstructured":"Peled, D.: Ten years of partial order reduction. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 17\u201328. Springer, Heidelberg (1998). doi: 10.1007\/BFb0028727"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-662-49665-7_23","volume-title":"Fundamental Approaches to Software Engineering","author":"S Putter de","year":"2016","unstructured":"de Putter, S., Wijs, A.: Verifying a verifier: on the formal correctness of an LTS transformation verification technique. In: Stevens, P., W\u0105sowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 383\u2013400. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49665-7_23"},{"key":"7_CR32","unstructured":"Roscoe, A.: The Theory and Practice of Concurrency. Prentice-Hall (1998)"},{"key":"7_CR33","unstructured":"Spaninks, L.: An Axiomatisation for Rooted Branching Bisimulation with Explicit Divergence. Master\u2019s thesis, Eindhoven University of Technology (2013)"},{"issue":"1","key":"7_CR34","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1016\/S0890-5401(02)93161-5","volume":"178","author":"I Ulidowski","year":"2002","unstructured":"Ulidowski, I., Phillips, I.: Ordered SOS process languages for branching and eager bisimulations. Inf. Comput. 178(1), 180\u2013213 (2002)","journal-title":"Inf. Comput."},{"key":"7_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-540-48654-1_32","volume-title":"CONCUR \u201994: Concurrency Theory","author":"C Verhoef","year":"1994","unstructured":"Verhoef, C.: A congruence theorem for structured operational semantics with predicates and negative premises. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 433\u2013448. Springer, Heidelberg (1994). doi: 10.1007\/978-3-540-48654-1_32"},{"key":"7_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-319-07602-7_21","volume-title":"Formal Aspects of Component Software","author":"A Wijs","year":"2014","unstructured":"Wijs, A.: Define, verify, refine: correct composition and transformation of concurrent system semantics. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 348\u2013368. Springer, Cham (2014). doi: 10.1007\/978-3-319-07602-7_21"},{"key":"7_CR37","doi-asserted-by":"crossref","unstructured":"Wijs, A.J.: Confluence detection for transformations of labelled transition systems. In: Proceedings of the 2nd Graphs as Models Workshop (GaM 2015). EPTCS, vol. 181, pp. 1\u201315. Open Publishing Association (2015)","DOI":"10.4204\/EPTCS.181.1"},{"key":"7_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1007\/978-3-642-36742-7_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Wijs","year":"2013","unstructured":"Wijs, A., Engelen, L.: Efficient property preservation checking of model refinements. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 565\u2013579. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-36742-7_41"},{"key":"7_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-319-06200-6_21","volume-title":"NASA Formal Methods","author":"A Wijs","year":"2014","unstructured":"Wijs, A., Engelen, L.: REFINER: towards formal verification of model transformations. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 258\u2013263. Springer, Cham (2014). doi: 10.1007\/978-3-319-06200-6_21"},{"key":"7_CR40","doi-asserted-by":"crossref","unstructured":"Wijs, A.: Achieving discrete relative timing with untimed process algebra. In: Proceedings of the 12th Conference on Engineering of Complex Computer Systems (ICECCS 2007), pp. 35\u201344. IEEE Computer Society Press (2007)","DOI":"10.1109\/ICECCS.2007.13"},{"key":"7_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-662-46681-0_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Wijs","year":"2015","unstructured":"Wijs, A.: GPU accelerated strong and branching bisimilarity checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 368\u2013383. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46681-0_29"},{"key":"7_CR42","doi-asserted-by":"crossref","unstructured":"Wijs, A., Fokkink, W.: From $$\\chi _{\\mathit{t}}$$ to $$\\mu $$ CRL: combining performance and functional analysis. In: Proceedings of the 10th Conference on Engineering of Complex Computer Systems (ICECCS 2005), pp. 184\u2013193. IEEE Computer Society Press (2005)","DOI":"10.1109\/ICECCS.2005.51"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68034-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T18:49:50Z","timestamp":1750877390000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68034-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319680330","9783319680347"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68034-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}