{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T00:28:32Z","timestamp":1791160112155,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":70,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540304920","type":"print"},{"value":"9783540322405","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11589976_6","type":"book-chapter","created":{"date-parts":[[2005,10,26]],"date-time":"2005-10-26T13:38:16Z","timestamp":1130333896000},"page":"70-88","source":"Crossref","is-referenced-by-count":46,"title":["Exp.Open 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-The-Fly Verification Methods"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Lang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/3-540-52148-8_11","volume-title":"Automatic Verification Methods for Finite State Systems","author":"A. Arnold","year":"1990","unstructured":"Arnold, A.: MEC: A System for Constructing and Analysing Transition Systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 117\u2013132. Springer, Heidelberg (1990)"},{"key":"6_CR2","unstructured":"A bird\u2019s eye view of JACK. Web page of the JACK project at CNR Pisa, http:\/\/fmt.isti.cnr.it\/jack\/OLD_JACK_PAGES\/JACK\/structure.html"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Barros, T., Henrio, L., Madelaine, E.: Behavioural Models for Hierarchical Components, Submitted to the 12th International SPIN Workshop on Model Checking of Software (2005)","DOI":"10.1007\/11537328_14"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-540-45069-6_40","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"2003","unstructured":"Behrmann, G., Larsen, K.G., Pel\u00e1nek, R.: To Store or Not to Store. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 433\u2013445. Springer, Heidelberg (2003)"},{"key":"6_CR5","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.\u00a03440, pp. 581\u2013585. Springer, Heidelberg (2005)"},{"key":"6_CR6","unstructured":"Best, E., Esparza, J., Grahlmann, B., Melzer, S., R\u00f6mer, S., Wallner, F.: The PEP verification system. In: Proceedings of FEmSys 1997 (1997)"},{"key":"6_CR7","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.\u00a02404, p. 596. Springer, Heidelberg (2002)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"A. Bouali","year":"1996","unstructured":"Bouali, A., Ressouche, A., Roy, V., de Simone, R.: The Fc2Tools set: a Toolset for the Verification of Concurrent Systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102. Springer, Heidelberg (1996)"},{"key":"6_CR9","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":"6_CR10","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1145\/256428.167071","volume-title":"Proceedings of the 1st ACM SIGSOFT International Symposium on the Foundations of Software Engineering","author":"S.C. Cheung","year":"1993","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, New York (1993)"},{"key":"6_CR11","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1145\/222124.222149","volume-title":"Proceedings of the 3rd ACM SIGSOFT International Symposium on the Foundations of Software Engineering","author":"S.C. Cheung","year":"1995","unstructured":"Cheung, S.C., Kramer, J.: Compositional Reachability Analysis of Finite-State Distributed Systems with User-Specified Constraints. In: Proceedings of the 3rd ACM SIGSOFT International Symposium on the Foundations of Software Engineering, Washington, DC, USA, pp. 140\u2013150. ACM Press, New York (1995)"},{"issue":"4","key":"6_CR12","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1145\/235321.235323","volume":"5","author":"S.C. Cheung","year":"1996","unstructured":"Cheung, S.C., Kramer, J.: Context Constraints for Compositional Reachability. ACM Transactions on Software Engineering Methodology TOSEM\u00a05(4), 334\u2013377 (1996)","journal-title":"ACM Transactions on Software Engineering Methodology TOSEM"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"Application and Theory of Petri Nets 1995","author":"S. Christensen","year":"1995","unstructured":"Christensen, S., Petrucci, L.: Modular State Space Analysis of Coloured Petri Nets. In: DeMichelis, G., D\u00edaz, M. (eds.) ICATPN 1995. LNCS, vol.\u00a0935. Springer, Heidelberg (1995)"},{"key":"6_CR14","unstructured":"Fernandez, J.-C.: ALDEBARAN\u00a0: un syst\u00e8me de v\u00e9rification par r\u00e9duction de processus communicants. Th\u00e8se de Doctorat, Universit\u00e9 Joseph\u00a0Fourier, Grenoble (1988)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Fernandez, J.-C., Jard, C., J\u00e9ron, T., Mounier, L.: On the Fly\u201d Verification of Finite Transition Systems. Formal Methods in System Design (1992)","DOI":"10.1007\/BF00121127"},{"key":"6_CR16","unstructured":"Fernandez, J.-C., Mounier, L.: Verifying Bisimulations On the Fly. In: Proceedings of the 3rd International Conference on Formal Description Techniques FORTE 1990, Madrid, Spain. North-Holland, Amsterdam (1990)"},{"key":"#cr-split#-6_CR17.1","doi-asserted-by":"crossref","unstructured":"Garavel, H.: OPEN\/C??SAR: An Open Software Architecture for Verification, Simulation, and Testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.??1384, pp. 68???84. Springer, Heidelberg (1998);","DOI":"10.1007\/BFb0054165"},{"key":"#cr-split#-6_CR17.2","unstructured":"Full version available as INRIA Research Report RR-3352"},{"key":"6_CR18","series-title":"IFIP","first-page":"377","volume-title":"Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE 2001","author":"H. Garavel","year":"2001","unstructured":"Garavel, H., Lang, F.: SVL: a Scripting Language for Compositional Verification. In: Proceedings of the 21st IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems FORTE 2001, Cheju Island, Korea. IFIP, pp. 377\u2013392. Kluwer Academic Publishers, Dordrecht (2001); Full version available as INRIA Research Report\u00a0RR-4223"},{"key":"6_CR19","unstructured":"Garavel, H., Lang, F., Mateescu, R.: An Overview of CADP 2001. European Association for Software Science and Technology (EASST) Newsletter, 4,13\u201324, 2002. Also available as INRIA Technical Report\u00a0RT-0254 (2001)"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-540-24732-6_11","volume-title":"Model Checking Software","author":"H. Garavel","year":"2004","unstructured":"Garavel, H., Mateescu, R.: SEQ.OPEN: A Tool for Efficient Trace-Based Verification. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 150\u2013155. Springer, Heidelberg (2004)"},{"key":"#cr-split#-6_CR21.1","doi-asserted-by":"crossref","unstructured":"Garavel, H., Mateescu, R., Smarandache, I.: Parallel State Space Construction for Model-Checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.??2057, pp. 217???234. Springer, Heidelberg (2001);","DOI":"10.1007\/3-540-45139-0_14"},{"key":"#cr-split#-6_CR21.2","unstructured":"Revised version available as INRIA Research Report??RR-4341"},{"key":"6_CR22","series-title":"IFIP","first-page":"379","volume-title":"Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification","author":"H. Garavel","year":"1990","unstructured":"Garavel, H., Sifakis, J.: Compilation and Verification of LOTOS Specifications. In: Proceedings of the 10th International Symposium on Protocol Specification, Testing and Verification, Ottawa, Canada. IFIP, pp. 379\u2013394. North-Holland, Amsterdam (1990)"},{"key":"6_CR23","series-title":"IFIP","first-page":"185","volume-title":"Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification FORTE\/PSTV 1999","author":"H. Garavel","year":"1999","unstructured":"Garavel, H., Sighireanu, M.: A Graphical Parallel Composition Operator for Process Algebras. In: Proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification FORTE\/PSTV 1999, Beijing, China. IFIP, pp. 185\u2013202. Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"#cr-split#-6_CR24.1","doi-asserted-by":"crossref","unstructured":"Gerth, R., Kuiper, R., Penczek, W., Peled, D.: A Partial Order Approach to Branching Time Logic Model Checking. Information and Computation??150(2), 132???152 (1999);","DOI":"10.1006\/inco.1998.2778"},{"key":"#cr-split#-6_CR24.2","unstructured":"A short version of this paper was previously published at the Third Israel Symposium on Theory of Computing and Systems ISTCS (1995)"},{"key":"6_CR25","unstructured":"Giannakopoulou, D.: Model Checking for Concurrent Software Architectures. PhD thesis, Imperial College of Science, Technology and Medicine \u2014 University of London \u2014 Department of Computer Science (1999)"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Using Partial Orders to Improve Automatic Verification Methods. In: Proceedings of the 2nd Workshop on Computer-Aided Verification, Rutgers, New Jersey, USA. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a03, pp. 321\u2013340. AMS-ACM (1990)","DOI":"10.1090\/dimacs\/003\/21"},{"issue":"5","key":"6_CR27","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 Minimisation of Finite State Systems using Interface Specifications. Formal Aspects of Computation\u00a08(5), 607\u2013616 (1996)","journal-title":"Formal Aspects of Computation"},{"key":"6_CR28","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., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531, pp. 186\u2013196. Springer, Heidelberg (1991)"},{"key":"6_CR29","unstructured":"Groote, J.F., Monin, F., Springintveld, J.: A Computer Checked Algebraic Verification of a Distributed Summation Algorithm. Computer Science Report 97\/14, Department of Mathematics and Computer Science, Eindhoven University of Technology (1997)"},{"key":"#cr-split#-6_CR30.1","doi-asserted-by":"crossref","unstructured":"Groote, J.F., van de Pol, J.: State Space Reduction using Partial ??-Confluence. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol.??1893, pp. 383???393. Springer, Heidelberg (2000);","DOI":"10.1007\/3-540-44612-5_34"},{"key":"#cr-split#-6_CR30.2","unstructured":"Also available as CWI Technical Report SEN-R0008, Amsterdam (2000)"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Ponse, A.: Syntax and semantics of \u03bc-CRL. In: Algebra of Communicating Processes, Workshops in Computing, pp. 26\u201362 (1995)","DOI":"10.1007\/978-1-4471-2120-6_2"},{"issue":"1\u20132","key":"6_CR32","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/S0304-3975(96)80702-X","volume":"170","author":"J.F. Groote","year":"1996","unstructured":"Groote, J.F., Sellink, M.P.A.: Confluence for process verification. Theoretical Computer Science\u00a0170(1\u20132), 47\u201381 (1996)","journal-title":"Theoretical Computer Science"},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"Hansen, H., Penczek, W., Valmari, A.: Stuttering-Insensitive Automata for On-the-fly Detection of Livelock Properties. In: 7th International ERCIM Workshop in Formal Methods for Industrial Critical Systems. Electronic Notes in Theoretical Computer Science, vol.\u00a066 (2002)","DOI":"10.1016\/S1571-0661(04)80411-0"},{"key":"6_CR34","volume-title":"Proceedings of the Third International Conference on Application of Concurrency to System Design","author":"H. Hansen","year":"2003","unstructured":"Hansen, H., Virtanen, H., Valmari, A.: Merging State-Based and Action-Based Verification. In: Proceedings of the Third International Conference on Application of Concurrency to System Design. IEEE Computer Society, Los Alamitos (2003)"},{"key":"6_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/3-540-45804-2","volume-title":"Interactive Markov Chains","author":"H. Hermanns","year":"2002","unstructured":"Hermanns, H.: Interactive Markov Chains. LNCS, vol.\u00a02428, p. 129. Springer, Heidelberg (2002)"},{"key":"6_CR36","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.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, pp. 244\u2013265. Springer, Heidelberg (1999)"},{"issue":"5","key":"6_CR37","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The Model Checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR38","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: On-The-Fly Model Checking. ACM Computing Surveys\u00a028(4) (1996)","DOI":"10.1145\/242224.242379"},{"key":"6_CR39","unstructured":"ISO\/IEC. LOTOS \u2014 A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. International Standard 8807, International Organization for Standardization \u2014 Information Processing Systems \u2014 Open Systems Interconnection, Gen\u00e8ve (1989)"},{"key":"6_CR40","unstructured":"ISO\/IEC. Enhancements to LOTOS (E-LOTOS). International Standard 15437:2001, International Organization for Standardization \u2014 Information Technology, Gen\u00e8ve (2001)"},{"key":"6_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-48683-6_12","volume-title":"Computer Aided Verification","author":"T. J\u00e9ron","year":"1999","unstructured":"J\u00e9ron, T., Morel, P.: Test generation derived from model-checking. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 108\u2013121. Springer, Heidelberg (1999)"},{"key":"#cr-split#-6_CR42.1","doi-asserted-by":"crossref","unstructured":"Krimm, J.-P., Mounier, L.: Compositional State Space Generation from LOTOS Programs. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol.??1217, Springer, Heidelberg (1997);","DOI":"10.1007\/BFb0035392"},{"key":"#cr-split#-6_CR42.2","unstructured":"Extended version with proofs available as Research Report VERIMAG??RR97-01"},{"key":"6_CR43","unstructured":"Lang, F.: The Exp.Open 2.0 manual page, Available online (2004), at http:\/\/www.inrialpes.fr\/vasy\/cadp\/man\/exp.open.html"},{"key":"6_CR44","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, pp. 140\u2013152. British Computer Society, Swinton (1988)","DOI":"10.1007\/978-1-4471-3534-0_7"},{"key":"#cr-split#-6_CR45.1","doi-asserted-by":"crossref","unstructured":"Mateescu, R.: A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.??2619, pp. 81???96. Springer, Heidelberg (2003);","DOI":"10.1007\/3-540-36577-X_7"},{"key":"#cr-split#-6_CR45.2","unstructured":"Full version available as INRIA Research Report??RR-4711"},{"issue":"3","key":"6_CR46","doi-asserted-by":"publisher","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. Science of Computer Programming\u00a046(3), 255\u2013281 (2003)","journal-title":"Science of Computer Programming"},{"key":"6_CR47","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"#cr-split#-6_CR48.1","doi-asserted-by":"crossref","unstructured":"Pace, G., Lang, F., Mateescu, R.: Calculating ??-Confluence Compositionally. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.??2725, pp. 446???459. Springer, Heidelberg (2003);","DOI":"10.1007\/978-3-540-45069-6_41"},{"key":"#cr-split#-6_CR48.2","unstructured":"Full version available as INRIA Research Report??RR-4918"},{"key":"6_CR49","unstructured":"Peled, D.: Partial Order Reduction: Linear and Branching Temporal Logics and Process Algebras. In: Peled, et al. (eds.) [51]"},{"key":"6_CR50","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"D.A. Peled","year":"1994","unstructured":"Peled, D.A.: Combining partial order reduction with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818. Springer, Heidelberg (1994)"},{"key":"6_CR51","doi-asserted-by":"crossref","unstructured":"Peled, D.A., Pratt, V.R., Holzmann, G.J. (eds.): Proceedings of the Workshop on Partial Order Methods in Verification. Dimacs Series in Discrete Mathematics, vol.\u00a029 (1997)","DOI":"10.1090\/dimacs\/029"},{"key":"6_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/3-540-63141-0_2","volume-title":"CONCUR\u201997: Concurrency Theory","author":"Y.S. Ramakrishna","year":"1997","unstructured":"Ramakrishna, Y.S., Smolka, S.A.: Partial-Order Reduction in the Weak Modal Mu-Calculus. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 5\u201324. Springer, Heidelberg (1997)"},{"key":"6_CR53","unstructured":"Romijn, J.: Model Checking the HAVi Leader Election Protocol. Technical Report SEN-R9915, CWI, Amsterdam, The Netherlands, submitted to Formal Methods in System Design (1999)"},{"key":"6_CR54","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1998","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)"},{"issue":"9","key":"6_CR55","doi-asserted-by":"publisher","first-page":"940","DOI":"10.1109\/26.35374","volume":"37","author":"K.K. Sabnani","year":"1989","unstructured":"Sabnani, K.K., Lapone, A.M., Uyar, M.U.: An Algorithmic Procedure for Checking Safety Properties of Protocols. IEEE Transactions on Communications\u00a037(9), 940\u2013948 (1989)","journal-title":"IEEE Transactions on Communications"},{"key":"6_CR56","first-page":"318","volume-title":"Proceedings of the IEEE International Conference on Network Protocols","author":"K.C. Tai","year":"1993","unstructured":"Tai, K.C., Koppol, V.: Hierarchy-Based Incremental Reachability Analysis of Communication Protocols. In: Proceedings of the IEEE International Conference on Network Protocols, San Francisco, CA, pp. 318\u2013325. IEEE Press, Piscataway (1993)"},{"key":"6_CR57","doi-asserted-by":"crossref","unstructured":"Valmari, A.: A Stubborn Attack on State Explosion. In: Proceedings of the 2nd Workshop on Computer-Aided Verification, Rutgers, New Jersey, USA. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a03, pp. 25\u201342. AMS-ACM (1990)","DOI":"10.1090\/dimacs\/003\/04"},{"key":"6_CR58","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Stubborn Set Methods for Process Algebras. In: Peled, et al. (eds.) [51]","DOI":"10.1090\/dimacs\/029\/12"},{"key":"6_CR59","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\u201d Tool. In: Larsen, P.G., Woodcock, J.C.P. (eds.) FME 1993. LNCS, vol.\u00a0670, pp. 597\u2013616. Springer, Heidelberg (1993)"},{"key":"6_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.) APN 1993. LNCS, vol.\u00a0674, pp. 427\u2013457. Springer, Heidelberg (1993)"},{"key":"6_CR61","unstructured":"van de Pol, J.: Proof using the PVS theorem prover that bisimulations are congruences for synchronization vectors that do not rename, cut, nor synchronize \u03c4-transitions. Personal communication (2003)"},{"key":"6_CR62","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 proc. IFIP 11th World Computer Congress, San Francisco (1989)"},{"key":"6_CR63","unstructured":"Yeh, W.J.: Controlling State Explosion in Reachability Analysis. PhD thesis, Software Engineering Research Center (SERC) Laboratory, Purdue University, Technical Report SERC-TR-147-P (1993)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11589976_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T14:06:55Z","timestamp":1586527615000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11589976_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540304920","9783540322405"],"references-count":70,"URL":"https:\/\/doi.org\/10.1007\/11589976_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}