{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T03:28:53Z","timestamp":1770348533604,"version":"3.49.0"},"reference-count":140,"publisher":"Springer Science and Business Media LLC","issue":"4-5","license":[{"start":{"date-parts":[[2015,4,22]],"date-time":"2015-04-22T00:00:00Z","timestamp":1429660800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2015,6]]},"DOI":"10.1007\/s00236-015-0226-1","type":"journal-article","created":{"date-parts":[[2015,4,21]],"date-time":"2015-04-21T09:33:52Z","timestamp":1429608832000},"page":"337-392","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":32,"title":["Compositional verification of asynchronous concurrent systems using CADP"],"prefix":"10.1007","volume":"52","author":[{"given":"Hubert","family":"Garavel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Lang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Radu","family":"Mateescu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,4,22]]},"reference":[{"key":"226_CR1","doi-asserted-by":"crossref","unstructured":"Aceto, L., Fokkink, W., Verhoef, C.: Structural Operational Semantics (Chapter 3), pp. 197\u2013292. North-Holland, Amsterdam (2001)","DOI":"10.1016\/B978-044482830-9\/50021-7"},{"key":"226_CR2","doi-asserted-by":"crossref","unstructured":"Ajami, K., Haddad, S., Ili\u00e9, J.-M.: Exploiting symmetry in linear time temporal logic model checking: one step beyond. In: Proceedings of Tools and Algorithms for Construction and Analysis of Systems TACAS\u201998, Lecture Notes in Computer Science, vol. 1384, pp. 52\u201367. Springer (1998)","DOI":"10.1007\/BFb0054164"},{"issue":"1","key":"226_CR3","doi-asserted-by":"crossref","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. Theoret. Comput. Sci. 126(1), 3\u201330 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"226_CR4","doi-asserted-by":"crossref","unstructured":"Andersen, H.R.: Partial model checking. In: Proceedings of Logic in Computer Science LICS\u201995, pp. 398\u2013407. IEEE (1995)","DOI":"10.1109\/LICS.1995.523274"},{"key":"226_CR5","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/s100090050032","volume":"2","author":"HR Andersen","year":"1999","unstructured":"Andersen, H.R., Lind-Nielsen, J.: Partial model checking of modal equations: a survey. J. Softw. Tools Technol. Transf. 2, 242\u2013259 (1999)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"226_CR6","doi-asserted-by":"crossref","unstructured":"Andersen, H.R., Staunstrup, J., Maretti, N.: A comparison of modular verification techniques. In: Proceedings of CAAP\/FASE\u201997, Lecture Notes in Computer Science, vol. 1214. Springer (1997)","DOI":"10.1007\/BFb0030625"},{"key":"226_CR7","doi-asserted-by":"crossref","unstructured":"Andersen, H.R., Staunstrup, J., Maretti, N.: Partial model checking with robdds. In: Proceedings of Tools and Algorithms for Construction and Analysis of Systems TACAS\u201997, Lecture Notes in Computer Science, vol. 1217. Springer (1997)","DOI":"10.1007\/BFb0035379"},{"key":"226_CR8","doi-asserted-by":"crossref","unstructured":"Andersen, H.R., Winskel, G.: Compositional checking of satisfaction. In: Proceedings of Computer Aided Verification CAV\u201991, Lecture Notes in Computer Science, vol. 575, pp. 24\u201336. Springer (1991)","DOI":"10.1007\/3-540-55179-4_4"},{"key":"226_CR9","doi-asserted-by":"crossref","unstructured":"Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec temporal logic: a new temporal property-specification language. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS\u201902, Lecture Notes in Computer Science, vol. 2280, pp. 296\u2013211. Springer (2002)","DOI":"10.1007\/3-540-46002-0_21"},{"key":"226_CR10","doi-asserted-by":"crossref","unstructured":"Armstrong, P.J., Goldsmith, M., Lowe, G., Ouaknine, J., Palikareva, H., Roscoe, A.W., Worrell, J.: Recent developments in FDR. In: Proceedings of Computer Aided Verification CAV\u201912, Lecture Notes in Computer Science, vol. 7358, pp. 699\u2013704. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_52"},{"key":"226_CR11","doi-asserted-by":"crossref","unstructured":"Arnold, A.: MEC: a system for constructing and analysing transition systems. In: Proceedings of Automatic Verification Methods for Finite State Systems CAV\u201989, Lecture Notes in Computer Science, vol. 407, pp. 117\u2013132. Springer (1989)","DOI":"10.1007\/3-540-52148-8_11"},{"key":"226_CR12","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"3","key":"226_CR13","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1006\/jcss.1999.1660","volume":"59","author":"R Barbuti","year":"1999","unstructured":"Barbuti, R., de Francesco, N., Santone, A., Vaglini, G.: Selective mu-calculus and formula-based equivalence of transition systems. J. Comput. Syst. Sci. 59(3), 537\u2013556 (1999)","journal-title":"J. Comput. Syst. Sci."},{"key":"226_CR14","doi-asserted-by":"crossref","unstructured":"Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Proceedings of Verification, Model Checking, and Abstract Interpretation VMCAI\u201904, Lecture Notes in Computer Science, vol. 2937, pp. 44\u201357. Springer (2004)","DOI":"10.1007\/978-3-540-24622-0_5"},{"key":"226_CR15","doi-asserted-by":"crossref","unstructured":"Basu, S., Ramakrishnan, C.R.: Compositional analysis for verification of parameterized systems. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS\u201903, Lecture Notes in Computer Science, vol. 2619, pp. 315\u2013330. Springer (2003)","DOI":"10.1007\/3-540-36577-X_23"},{"key":"226_CR16","doi-asserted-by":"crossref","unstructured":"Beer, I., Ben-David, S., Landver, A.: On-the-fly model checking of RCTL formulas. In: Proceedings of Computer Aided Verification CAV\u201998, Lecture Notes in Computer Science, vol. 1427, pp. 184\u2013194. Springer (1998)","DOI":"10.1007\/BFb0028744"},{"key":"226_CR17","unstructured":"Berard, B., Laroussinie, F.: Verification compositionnelle des p-automates. Technical Report Lot 4.1, R\u00e9seau National des Technologies Logicielles, Project AVERROES (2003)"},{"key":"226_CR18","doi-asserted-by":"crossref","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. Theoret. Comput. Sci. 37, 77\u2013121 (1985)","journal-title":"Theoret. Comput. Sci."},{"key":"226_CR19","volume-title":"Handbook of Process Algebra","year":"2001","unstructured":"Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier, Amsterdam (2001)"},{"issue":"3","key":"226_CR20","doi-asserted-by":"crossref","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. Transf. 7(3), 280\u2013291 (2005)","journal-title":"Softw. Tools Technol. Transf."},{"key":"226_CR21","doi-asserted-by":"crossref","unstructured":"Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Proceedings of Computer Aided Verification CAV\u201910, Lecture Notes in Computer Science, vol. 6174, pp. 354\u2013359. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_31"},{"key":"226_CR22","doi-asserted-by":"crossref","unstructured":"Bodentien, N., Vestergaard, J., Friis, J., Kristoffersen, K., Larsen, K.G.: Verification of state\/event systems by quotienting. Technical Report RS-99-41, Basic Research in Computer Science (1999)","DOI":"10.7146\/brics.v6i41.20111"},{"key":"226_CR23","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Fernandez, J.-C., Graf, S., Rodr\u00edguez, C., Sifakis, J.: Safety for branching time semantics. In: Proceedings of ICALP. Springer (1991)","DOI":"10.1007\/3-540-54233-7_126"},{"key":"226_CR24","doi-asserted-by":"crossref","unstructured":"Bouali, A., Ressouche, A., Roy, V., de Simone, R.: The fc2tools set: a toolset for the verification of concurrent systems. In: Proceedings of Computer-Aided Verification CAV\u201996, Lecture Notes in Computer Science, vol. 1102. Springer (1996)","DOI":"10.1007\/3-540-61474-5_98"},{"key":"226_CR25","doi-asserted-by":"crossref","DOI":"10.1016\/B978-044482830-9\/50022-9","volume-title":"Modal Logics and Mu-Calculi: An Introduction (Chapter 4)","author":"JC Bradfield","year":"2001","unstructured":"Bradfield, J.C., Stirling, C.: Modal Logics and Mu-Calculi: An Introduction (Chapter 4). Elsevier, Amsterdam (2001)"},{"issue":"3","key":"226_CR26","doi-asserted-by":"crossref","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":"226_CR27","doi-asserted-by":"crossref","unstructured":"Cassez, F., Laroussinie, F.: Model-checking for hybrid systems by quotienting and constraints solving. In: Proceedings of Computer Aided Verification CAV\u201900, Lecture Notes in Computer Science, vol. 1855. Springer (2000)","DOI":"10.1007\/10722167_29"},{"key":"226_CR28","unstructured":"Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., McKinty, C., Powazny, V., Lang, F., Serwe, W., Smeding, G.: Reference Manual of the LNT to LOTOS Translator (Version 6.1). INRIA\/VASY and INRIA\/CONVECS (2014)"},{"key":"226_CR29","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: Proceedings of Formal Description Techniques for Distributed Systems and Communication Protocols \/ Protocol Specification, Testing, and Verification FORTE\/PSTV\u201996, pp. 435\u2013450. IFIP, Chapman & Hall (1996)","DOI":"10.1007\/978-0-387-35079-0_28"},{"key":"226_CR30","unstructured":"Cheung, K.H.: Compositional Analysis of Complex Distributed Systems. PhD thesis, Department of Computer Science, Hong Kong University of Science and Technology, Hong Kong (1998)"},{"key":"226_CR31","doi-asserted-by":"crossref","unstructured":"Cheung, S.C., Kramer, J.: Enhancing compositional reachability analysis with context constraints. In: Proceedings of Foundations of Software Engineering, pp. 115\u2013125. ACM Press (1993)","DOI":"10.1145\/256428.167071"},{"key":"226_CR32","doi-asserted-by":"crossref","unstructured":"Cheung, S.C., Kramer, J.: Compositional reachability analysis of finite-state distributed systems with user-specified constraints. In: Proceedings of Foundations of Software Engineering, pp. 140\u2013150. ACM Press (1995)","DOI":"10.1145\/222124.222149"},{"issue":"4","key":"226_CR33","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1145\/235321.235323","volume":"5","author":"SC Cheung","year":"1996","unstructured":"Cheung, S.C., Kramer, J.: Context constraints for compositional reachability. ACM Trans. Softw. Eng. Methodol. 5(4), 334\u2013377 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"226_CR34","volume-title":"Model Checking","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"226_CR35","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Jha, S., Prasad Sistla, A.: Symmetry reductions in model checking. In: Proceedings of Computer Aided Verification CAV\u201998, Lecture Notes in Computer Science, vol. 1427, pp. 147\u2013158. Springer (1998)","DOI":"10.1007\/BFb0028741"},{"issue":"1\/2","key":"226_CR36","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des. 9(1\/2), 77\u2013104 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"226_CR37","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench. In: Proceedings of Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science, vol. 407, pp. 24\u201337. Springer (1989)","DOI":"10.1007\/3-540-52148-8_3"},{"issue":"2","key":"226_CR38","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R Cleaveland","year":"1993","unstructured":"Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Form. Methods Syst. Des. 2(2), 121\u2013147 (1993)","journal-title":"Form. Methods Syst. Des."},{"key":"226_CR39","doi-asserted-by":"crossref","unstructured":"Coste, N., Garavel, H., Hermanns, H., Lang, F., Mateescu, R., Serwe, W.: Ten years of performance evaluation for concurrent systems using CADP. In: Proceedings of Leveraging Applications of Formal Methods, Verification and Validation ISoLA\u201910, Lecture Notes in Computer Science, vol. 6416, pp. 128\u2013142. Springer (2010)","DOI":"10.1007\/978-3-642-16561-0_18"},{"key":"226_CR40","doi-asserted-by":"crossref","unstructured":"Crouzen, P., Hermanns, H.: Aggregation ordering for massively parallel compositional models. In: Proceedings of Application of Concurrency to System Design ACSD\u201910. IEEE (2010)","DOI":"10.1109\/ACSD.2010.28"},{"key":"226_CR41","doi-asserted-by":"crossref","unstructured":"Crouzen, P., Lang, F.: Smart reduction. In: Proceedings of Fundamental Approaches to Software Engineering FASE\u20192011, Lecture Notes in Computer Science, vol. 6603, pp. 111\u2013126. Springer (2011)","DOI":"10.1007\/978-3-642-19811-3_9"},{"key":"226_CR42","doi-asserted-by":"crossref","unstructured":"Dam, M.: Model checking mobile processes. In: Proceedings of Concurrency Theory CONCUR\u201993, Lecture Notes in Computer Science, vol. 715, pp. 22\u201336. Springer (1993)","DOI":"10.1007\/3-540-57208-2_3"},{"issue":"3","key":"226_CR43","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/s100090050031","volume":"2","author":"X Du","year":"1999","unstructured":"Du, X., Smolka, S.A., Cleaveland, R.: Local model checking and protocol analysis. J. Softw. Tools Technol. Transf. 2(3), 219\u2013241 (1999)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"226_CR44","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time logic to synthesize synchronization skeletons. Sci. Comput. Program. 2, 241\u2013266 (1982)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"226_CR45","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"226_CR46","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus. In: Proceedings of Logic in Computer Science LICS\u201986, pp. 267\u2013278 (1986)"},{"key":"226_CR47","unstructured":"Fantechi, A., Gnesi, S., Ristori, G.: From actl to mu-calculus. In: Proceedings of Theory and Practice in Verification. IEI-CNR, pp. 3\u201310 (1992)"},{"key":"226_CR48","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/BF01384084","volume":"4","author":"A Fantechi","year":"1994","unstructured":"Fantechi, A., Gnesi, S., Ristori, G.: Model checking for action-based logics. Form. Methods Syst. Des. 4, 187\u2013203 (1994)","journal-title":"Form. Methods Syst. Des."},{"key":"226_CR49","unstructured":"Fernandez, J.-C.: ALDEBARAN : un syst\u00e8me de v\u00e9rification par r\u00e9duction de processus communicants. Th\u00e8se de Doctorat, Universit\u00e9 Joseph Fourier (Grenoble) (1988)"},{"key":"226_CR50","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: Proceedings of Software Engineering ICSE\u201914, pp. 246\u2013259. ACM (1992)","DOI":"10.1145\/143062.143124"},{"key":"226_CR51","doi-asserted-by":"crossref","unstructured":"Fernandez, J.-C., Mounier, L.: \u201con the fly\u201d verification of behavioural equivalences and preorders. In: Proceedings of Computer-Aided Verification CAV\u201991, Lecture Notes in Computer Science, vol. 575, pp. 181\u2013191. Springer (1991)","DOI":"10.1007\/3-540-55179-4_18"},{"key":"226_CR52","doi-asserted-by":"crossref","unstructured":"Fernandez, J.-C., Mounier, L.: A tool set for deciding behavioral equivalences. In: Proceedings of CONCUR\u201991 (1991)","DOI":"10.1007\/3-540-54430-5_78"},{"issue":"2","key":"226_CR53","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"MJ Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"226_CR54","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of Principles of Programming Languages POPL\u201905. ACM Press (2005)","DOI":"10.1145\/1040305.1040315"},{"key":"226_CR55","unstructured":"Garavel, H.: Compilation of lotos abstract data types. In: Proceedings of Formal Description Techniques FORTE\u201989, pp. 147\u2013162. North-Holland (1989)"},{"key":"226_CR56","doi-asserted-by":"crossref","unstructured":"Garavel, H.: Open\/c\u00e6sar: an open software architecture for verification, simulation, and testing. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS\u201998, Lecture Notes in Computer Science, vol. 1384, pp. 68\u201384. Springer (1998)","DOI":"10.1007\/BFb0054165"},{"key":"226_CR57","doi-asserted-by":"crossref","unstructured":"Garavel, H., Lang, F.: Svl: a scripting language for compositional verification. In: Proceedings of Formal Techniques for Networked and Distributed Systems FORTE\u20192001, pp. 377\u2013392. IFIP, Kluwer (2001)","DOI":"10.1007\/0-306-47003-9_24"},{"key":"226_CR58","doi-asserted-by":"crossref","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: Cadp 2010: A toolbox for the construction and analysis of distributed processes. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS\u20192011, Lecture Notes in Computer Science, vol. 6605, pp. 372\u2013387 (2011)","DOI":"10.1007\/978-3-642-19835-9_33"},{"issue":"3","key":"226_CR59","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1016\/j.scico.2008.09.011","volume":"74","author":"H Garavel","year":"2009","unstructured":"Garavel, H., Sala\u00fcn, G., Serwe, W.: On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP. Sci. Comput. Program. 74(3), 100\u2013127 (2009)","journal-title":"Sci. Comput. Program."},{"key":"226_CR60","unstructured":"Garavel, H., Sifakis, J.: Compilation and verification of LOTOS specifications. In: Proceedings of Protocol Specification, Testing and Verification PSTV\u201990, pp. 379\u2013394. IFIP, North-Holland (1990)"},{"key":"226_CR61","doi-asserted-by":"crossref","unstructured":"Garavel, H., Sighireanu, M.: A graphical parallel composition operator for process algebras. In: Proceedings of Formal Description Techniques for Distributed Systems and Communication Protocols\/Protocol Specification, Testing, and Verification FORTE\/PSTV\u201999, pp. 185\u2013202. IFIP, Kluwer (1999)","DOI":"10.1007\/978-0-387-35578-8_11"},{"key":"226_CR62","doi-asserted-by":"crossref","unstructured":"Garavel, H., Thivolle, D.: Verification of gals systems by combining synchronous languages and process calculi. In: Proceedings of Model Checking Software SPIN\u20192009, Lecture Notes in Computer Science, vol. 5578, pp. 241\u2013260. Springer (2009)","DOI":"10.1007\/978-3-642-02652-2_20"},{"key":"226_CR63","unstructured":"Giannakopoulou, D.: Model Checking for Concurrent Software Architectures. PhD thesis, Imperial College of Science, Technology and Medicine, University of London (1999)"},{"key":"226_CR64","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. In: Proceedings of Foundations of Software Engineering ESEC\/FSE\u20192003, pp. 257\u2013266. ACM (2003)","DOI":"10.1145\/940071.940106"},{"key":"226_CR65","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P.J., Boulgakov, A., Roscoe, A.W.: FDR3\u2014A modern refinement checker for CSP. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS\u201914, Lecture Notes in Computer Science, vol. 8413, pp. 187\u2013201. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_13"},{"key":"226_CR66","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Using partial orders to improve automatic verification methods. In: Proceedings of Computer-Aided Verification CAV\u201990, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 3, pp. 321\u2013340. AMS-ACM (1990)","DOI":"10.1090\/dimacs\/003\/21"},{"key":"226_CR67","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Wolper, P.: A partial approach to model checking. In: Proceedings of Logic in Computer Science LICS\u201991. IEEE (1991)","DOI":"10.1109\/LICS.1991.151664"},{"key":"226_CR68","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. In: Proceedings of Computer-Aided Verification CAV\u201991, Lecture Notes in Computer Science, vol. 575. Springer (1991)","DOI":"10.1007\/3-540-55179-4_32"},{"key":"226_CR69","doi-asserted-by":"crossref","unstructured":"Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Proceedings of Computer-Aided Verification CAV\u201990, Lecture Notes in Computer Science, vol. 531, pp. 186\u2013196. Springer (1990)","DOI":"10.1007\/BFb0023732"},{"issue":"5","key":"226_CR70","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1007\/BF01211911","volume":"8","author":"S Graf","year":"1996","unstructured":"Graf, S., Steffen, B., L\u00fcttgen, G.: Compositional minimisation of finite state systems using interface specifications. Form. Aspects Comput. 8(5), 607\u2013616 (1996)","journal-title":"Form. Aspects Comput."},{"key":"226_CR71","unstructured":"Groote, J.F., Kouters, T.W.D.M., Osaiweran, A.A.H.: Specification guidelines to avoid the state space explosion problem. J. Softw. Test. Verif. Reliab. 25(1), 4\u201333 (2015) (2014)"},{"key":"226_CR72","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Ponse, A.: The syntax and semantics of $$\\mu $$ \u03bc CRL. In: Proceedings of Workshop on the Algebra of Communicating Processes ACP\u201994, Workshops in Computing Series, pp. 26\u201362. Springer (1995)","DOI":"10.1007\/978-1-4471-2120-6_2"},{"key":"226_CR73","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Proceedings of ICALP\u201990, Lecture Notes in Computer Science, vol. 443, pp. 626\u2013638. Springer (1990)","DOI":"10.1007\/BFb0032063"},{"key":"226_CR74","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2231-4","volume-title":"Synchronous Pogramming of Reactive Systems","author":"N Halbwachs","year":"1993","unstructured":"Halbwachs, N.: Synchronous Pogramming of Reactive Systems. Kluwer, Amsterdam (1993)"},{"key":"226_CR75","doi-asserted-by":"crossref","unstructured":"Hamaguchi, K., Hiraishi, H., Yajima, S.: Branching time regular temporal logic for model checking with linear time complexity. In: Proceedings of Computer Aided Verification CAV\u201990, Lecture Notes in Computer Science, vol. 531, pp. 253\u2013262. Springer (1990)","DOI":"10.1007\/BFb0023739"},{"key":"226_CR76","volume-title":"The semantics of programming languages: an elementary introduction using structural operational semantics","author":"M Hennessy","year":"1990","unstructured":"Hennessy, M.: The semantics of programming languages: an elementary introduction using structural operational semantics. Wiley, New York (1990)"},{"issue":"8","key":"226_CR77","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"issue":"1\/2","key":"226_CR78","first-page":"41","volume":"9","author":"CN Ip","year":"1996","unstructured":"Ip, C.N., Dill, D.L.: Better verification through symmetry. Form. Methods Syst. Des. 9(1\/2), 41\u201375 (1996)","journal-title":"Form. Methods Syst. Des."},{"key":"226_CR79","unstructured":"ISO\/IEC: LOTOS\u2014A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization\u2014Information Processing Systems\u2014Open Systems Interconnection (1989)"},{"key":"226_CR80","unstructured":"ISO\/IEC: Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization\u2014Information Technology (2001)"},{"key":"226_CR81","doi-asserted-by":"crossref","unstructured":"Katz, S., Peled, D.: An efficient verification method for parallel and distributed programs. In: Proceedings of Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Lecture Notes in Computer Science, vol. 354, pp. 489\u2013507. Springer (1988)","DOI":"10.1007\/BFb0013032"},{"key":"226_CR82","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 $$ \u03bc -calculus. Theoret. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theoret. Comput. Sci."},{"key":"226_CR83","doi-asserted-by":"crossref","unstructured":"Krimm, J.-P., Mounier, L.: Compositional state space generation from lotos programs. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS\u201997, Lecture Notes in Computer Science, vol. 1217. Springer (1997)","DOI":"10.1007\/BFb0035392"},{"key":"226_CR84","doi-asserted-by":"crossref","unstructured":"Lang, F.: Compositional verification using svl scripts. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS\u20192002, Lecture Notes in Computer Science, vol. 2280, pp. 465\u2013469. Springer (2002)","DOI":"10.1007\/3-540-46002-0_33"},{"key":"226_CR85","doi-asserted-by":"crossref","unstructured":"Lang, F.: Exp.open 2.0: A flexible tool integrating partial order, compositional, and on-the-fly verification methods. In: Proceedings of Integrated Formal Methods IFM\u20192005, Lecture Notes in Computer Science, vol. 3771, pp. 70\u201388. Springer (2005)","DOI":"10.1007\/11589976_6"},{"key":"226_CR86","doi-asserted-by":"crossref","unstructured":"Lang, F.: Refined interfaces for compositional verification. In: Proceedings of Formal Techniques for Networked and Distributed Systems FORTE\u20192006, Lecture Notes in Computer Science, vol. 4229, pp. 159\u2013174. Springer (2006)","DOI":"10.1007\/11888116_13"},{"key":"226_CR87","doi-asserted-by":"crossref","unstructured":"Lang, F., Mateescu, R.: Partial model checking using networks of labelled transition systems and boolean equation systems. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS\u20192012, Lecture Notes in Computer Science, vol. 7214, pp. 141\u2013156. Springer (2012)","DOI":"10.1007\/978-3-642-28756-5_11"},{"issue":"4","key":"226_CR88","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. Log. Methods Comput. Sci. 9(4), 1\u201332 (2013)","journal-title":"Log. Methods Comput. Sci."},{"issue":"6","key":"226_CR89","doi-asserted-by":"crossref","first-page":"681","DOI":"10.1007\/s00165-009-0133-8","volume":"22","author":"F Lang","year":"2010","unstructured":"Lang, F., Sala\u00fcn, G., H\u00e9rilier, R., Kramer, J., Magee, J.: Translating fsp into lotos and networks of automata. Form. Aspects Comput. 22(6), 681\u2013711 (2010)","journal-title":"Form. Aspects Comput."},{"key":"226_CR90","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Larsen, K.G.: Compositional model checking of real time systems. In: Proceedings of Concurrency Theory CONCUR\u201995, Lecture Notes in Computer Science, vol. 962. Springer (1995)","DOI":"10.1007\/3-540-60218-6_3"},{"key":"226_CR91","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Larsen, K.G.: Cmc: A tool for compositional model checking of real-time systems. In: Proceedings of Formal Description Techniques for Distributed Systems and Communication Protocols\/Protocol Specification, Testing and Verification FORTE\/PSTV\u201998, IFIP Conference Proceedings, vol. 135. Kluwer (1998)","DOI":"10.1007\/978-0-387-35394-4_27"},{"key":"226_CR92","doi-asserted-by":"crossref","unstructured":"Larsen, K.G.: Proof systems for Hennessy-Milner logic with recursion. In: Proceedings of Trees in Algebra and Programming CAAP\u201988, Lecture Notes in Computer Science, vol. 299, pp. 215\u2013230. Springer (1988)","DOI":"10.1007\/BFb0026106"},{"key":"226_CR93","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Compositional and symbolic model checking of real-time systems. In: Proceedings of Real-Time Systems. IEEE (1995)","DOI":"10.1109\/REAL.1995.495198"},{"key":"226_CR94","volume-title":"Concurrency: State Models and Java Programs","author":"J Magee","year":"2006","unstructured":"Magee, J., Kramer, J.: Concurrency: State Models and Java Programs, 2006th edn. Wiley, New York (2006)","edition":"2006"},{"key":"226_CR95","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 Specification and Verification of Concurrent Systems, pp. 140\u2013152. British Computer Society (1988)","DOI":"10.1007\/978-1-4471-3534-0_7"},{"key":"226_CR96","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proceedings of Principles of Distributed Computing PODC\u201990, pp. 377\u2013408 (1990)","DOI":"10.1145\/93385.93442"},{"key":"226_CR97","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, vol. I (Specification). Springer (1992)","DOI":"10.1007\/978-1-4612-0931-7"},{"issue":"4","key":"226_CR98","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/BF01660034","volume":"1","author":"AJ Martin","year":"1986","unstructured":"Martin, A.J.: Compiling communicating processes into delay-insensitive VLSI circuits. Distrib. Comput. 1(4), 226\u2013234 (1986)","journal-title":"Distrib. Comput."},{"key":"226_CR99","doi-asserted-by":"crossref","unstructured":"Martinelli, F.: Symbolic partial model checking for security analysis. In: Proceedings of Mathematical Methods, Models, and Architectures for Computer Network Security MMM-ACNS, Lecture Notes in Computer Science, vol. 2776. Springer (2003)","DOI":"10.1007\/978-3-540-45215-7_10"},{"key":"226_CR100","unstructured":"Mateescu, R.: Local model-checking of an alternation-free value-based modal mu-calculus. In: Proceedings ofVerification, Model Checking and Abstract Interpretation VMCAI\u201998. University Ca\u2019 Foscari of Venice (1998)"},{"key":"226_CR101","doi-asserted-by":"crossref","unstructured":"Mateescu, R.: Efficient diagnostic generation for boolean equation systems. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS\u20192000, Lecture Notes in Computer Science, vol. 1785, pp. 251\u2013265. Springer (2000)","DOI":"10.1007\/3-540-46419-0_18"},{"issue":"1","key":"226_CR102","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/s10009-005-0194-9","volume":"8","author":"R Mateescu","year":"2006","unstructured":"Mateescu, R.: Caesar\\_solve: a generic library for on-the-fly resolution of alternation-free boolean equation systems. J. Softw. Tools Technol. Transf. 8(1), 37\u201356 (2006)","journal-title":"J. Softw. Tools Technol. Transf."},{"key":"226_CR103","doi-asserted-by":"crossref","unstructured":"Mateescu, R., Sala\u00fcn, G.: Translating pi-calculus into LOTOS NT. In: Proceedings of Integrated Formal Methods IFM\u20192010, Lecture Notes in Computer Science, vol. 6396, pp. 229\u2013244. Springer (2010)","DOI":"10.1007\/978-3-642-16265-7_17"},{"issue":"3","key":"226_CR104","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/S0167-6423(02)00094-1","volume":"46","author":"R Mateescu","year":"2003","unstructured":"Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Sci. Comput. Program. 46(3), 255\u2013281 (2003)","journal-title":"Sci. Comput. Program."},{"key":"226_CR105","doi-asserted-by":"crossref","unstructured":"Mateescu, R., Thivolle, D.: A model checking language for concurrent value-passing systems. In: Proceedings of Formal Methods FM\u201908, Lecture Notes in Computer Science, vol. 5014, pp. 148\u2013164. Springer (2008)","DOI":"10.1007\/978-3-540-68237-0_12"},{"issue":"3","key":"226_CR106","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":"226_CR107","doi-asserted-by":"crossref","unstructured":"Milner, R.: A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol. 92. Springer (1980)","DOI":"10.1007\/3-540-10235-3"},{"key":"226_CR108","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Upper Saddle River (1989)"},{"key":"226_CR109","volume-title":"Communicating and Mobile Systems: The Pi-Calculus","author":"R Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems: The Pi-Calculus. Cambridge University Press, Cambridge (1999)"},{"key":"226_CR110","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Schmidt, D., Steffen, B.: Model-checking: a tutorial introduction. In: Proceedings of Static Analysis Symposium SAS\u201999, Lecture Notes in Computer Science, vol. 1694, pp. 330\u2013354. Springer (1999)","DOI":"10.1007\/3-540-48294-6_22"},{"key":"226_CR111","doi-asserted-by":"crossref","unstructured":"De Nicola, R., Fantechi, A., Gnesi, S., Ristori, G.: An action-based framework for verifying logical and behavioural properties of concurrent systems. In: Proceedings of Computer Aided Verification CAV\u201991, Lecture Notes in Computer Science, vol. 575, pp. 37\u201347. Springer (1991)","DOI":"10.1007\/3-540-55179-4_5"},{"key":"226_CR112","doi-asserted-by":"crossref","unstructured":"De Nicola, R., Vaandrager, F.W.: Action Versus State Based Logics for Transition Systems, Lecture Notes in Computer Science, vol. 469, pp. 407\u2013419. Springer (1990)","DOI":"10.1007\/3-540-53479-2_17"},{"key":"226_CR113","unstructured":"Osaiweran, A.A.H.: Formal Development of Control Software in the Medical Systems Domain. PhD thesis, Eindhoven University of Technology (2012)"},{"key":"226_CR114","unstructured":"Overman, W.T., Crocker, S.D.: Verification of concurrent systems: function and timing. In: Proceedings of Protocol Specification, Testing and Verification PSTV\u201982, pp. 401\u2013409. North-Holland (1982)"},{"issue":"6","key":"226_CR115","doi-asserted-by":"crossref","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":"226_CR116","doi-asserted-by":"crossref","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Theoretical Computer Science, Lecture Notes in Computer Science, vol. 104, pp. 167\u2013183. Springer (1981)","DOI":"10.1007\/BFb0017309"},{"key":"226_CR117","doi-asserted-by":"crossref","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Proceedings of Computer Aided Verification CAV\u201993, Lecture Notes in Computer Science, vol. 697, pp. 409\u2013423. Springer (1993)","DOI":"10.1007\/3-540-56922-7_34"},{"key":"226_CR118","unstructured":"Plotkin, G.D.: A Structural Approach to Operational Semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University (1981)"},{"key":"226_CR119","first-page":"17","volume":"60\u201361","author":"GD Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60\u201361, 17\u2013139 (2004)","journal-title":"J. Log. Algebr. Program."},{"key":"226_CR120","doi-asserted-by":"crossref","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. Log. Algebr. Program. 60\u201361, 3\u201315 (2004)","journal-title":"J. Log. Algebr. Program."},{"key":"226_CR121","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of Foundations of Computer Science, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"226_CR122","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A Pnueli","year":"1981","unstructured":"Pnueli, A.: A temporal logic of concurrent programs. Theoret. Comput. Sci. 13, 45\u201360 (1981)","journal-title":"Theoret. Comput. Sci."},{"key":"226_CR123","first-page":"195","volume":"19","author":"J-P Queille","year":"1983","unstructured":"Queille, J.-P., Sifakis, J.: Fairness and related properties in transition systems\u2014a temporal logic to deal with fairness. Acta Inf. 19, 195\u2013220 (1983)","journal-title":"Acta Inf."},{"key":"226_CR124","unstructured":"Rathke, J., Hennessy, M.: Local Model Checking for a Value-Based Modal $$\\mu $$ \u03bc -Calculus. Report 5\/96, School of Cognitive and Computing Sciences, University of Sussex (1996)"},{"key":"226_CR125","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe","year":"1998","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Upper Saddle River (1998)"},{"issue":"9","key":"226_CR126","doi-asserted-by":"crossref","first-page":"940","DOI":"10.1109\/26.35374","volume":"37","author":"KK Sabnani","year":"1989","unstructured":"Sabnani, K.K., Lapone, A.M., Uyar, M.U.: An algorithmic procedure for checking safety properties of protocols. IEEE Trans. Commun. 37(9), 940\u2013948 (1989)","journal-title":"IEEE Trans. Commun."},{"key":"226_CR127","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"R Streett","year":"1982","unstructured":"Streett, R.: Propositional dynamic logic of looping and converse. Inf. Control 54, 121\u2013141 (1982)","journal-title":"Inf. Control"},{"key":"226_CR128","doi-asserted-by":"crossref","unstructured":"Tai, K.C., Koppol, V.: Hierarchy-based incremental reachability analysis of communication protocols. In: Proceedings of Network Protocols, pp. 318\u2013325. IEEE (1993)","DOI":"10.1109\/ICNP.1993.340896"},{"key":"226_CR129","unstructured":"Tai, K.C., Koppol, V.: An incremental approach to reachability analysis of distributed programs. In: Proceedings of Software Specification and Design, pp. 141\u2013150. IEEE Press (1993)"},{"key":"226_CR130","unstructured":"Thivolle, D.: Langages modernes pour la v\u00e9rification des syst\u00e8mes asynchrones. Th\u00e8se de Doctorat, Universit\u00e9 Joseph Fourier (Grenoble, France) and Universitatea Politehnica din Bucuresti (Bucharest, Romania) (2011)"},{"key":"226_CR131","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Computation Tree Logic and Regular $$\\omega $$ \u03c9 -Languages, Lecture Notes in Computer Science, vol. 354, pp. 690\u2013713 (1989)","DOI":"10.1007\/BFb0013041"},{"key":"226_CR132","doi-asserted-by":"crossref","unstructured":"Tronel, F., Lang, F., Garavel, H.: Compositional verification using cadp of the scalagent deployment protocol for software components. In: Proceedings of Formal Methods for Open Object-based Distributed Systems FMOODS\u20192003, Lecture Notes in Computer Science, vol. 2884, pp. 244\u2013260. Springer (2003)","DOI":"10.1007\/978-3-540-39958-2_17"},{"key":"226_CR133","doi-asserted-by":"crossref","unstructured":"Valmari, A.: A stubborn attack on state explosion. In: Proceedings of Computer-Aided Verification CAV\u201990, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 3, pp. 25\u201342. AMS-ACM (1990)","DOI":"10.1090\/dimacs\/003\/04"},{"key":"226_CR134","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Compositional state space generation. In: Proceedings of Advances in Petri Nets, Lecture Notes in Computer Science, vol. 674, pp. 427\u2013457. Springer (1993)","DOI":"10.1007\/3-540-56689-9_54"},{"key":"226_CR135","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.J.: The Linear Time-Branching Time Spectrum I. The Semantics of Concrete, Sequential Processes (Chapter 1), pp. 3-99. North-Holland, Amsterdam (2001)","DOI":"10.1016\/B978-044482830-9\/50019-9"},{"key":"226_CR136","unstructured":"van Glabbeek, R.J., Weijland, W.P.: Branching-time and abstraction in bisimulation semantics (extended abstract). CS R8911, Centrum voor Wiskunde en Informatica (1989)"},{"issue":"3","key":"226_CR137","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"},{"issue":"1\/2","key":"226_CR138","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1\/2), 72\u201399 (1983)","journal-title":"Inf. Control"},{"key":"226_CR139","unstructured":"Yeh, W.J.: Controlling State Explosion in Reachability Analysis. PhD thesis, Software Engineering Research Center (SERC) Laboratory, Purdue University, (1993). Technical Report SERC-TR-147-P"},{"key":"226_CR140","doi-asserted-by":"crossref","unstructured":"Yeh, W.J., Young, M.: Compositional reachability analysis using process algebra. In: Proceedings of Testing, Analysis, and Verification SIGSOFT\u201991, pp. 49\u201359. ACM Press (1991)","DOI":"10.1145\/120807.120812"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0226-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-015-0226-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0226-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T19:57:46Z","timestamp":1747943866000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-015-0226-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,4,22]]},"references-count":140,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["226"],"URL":"https:\/\/doi.org\/10.1007\/s00236-015-0226-1","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,4,22]]}}}