{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:59:21Z","timestamp":1767927561533,"version":"3.49.0"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,7,1]],"date-time":"2002-07-01T00:00:00Z","timestamp":1025481600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2002,7]]},"DOI":"10.1023\/a:1016091902809","type":"journal-article","created":{"date-parts":[[2002,12,28]],"date-time":"2002-12-28T20:59:24Z","timestamp":1041109164000},"page":"39-78","source":"Crossref","is-referenced-by-count":28,"title":["Bisimulation Minimization and Symbolic Model Checking"],"prefix":"10.1007","volume":"21","author":[{"given":"Kathi","family":"Fisler","sequence":"first","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5087919_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi, \u201cAn implementation of three algorithms for timing verification based on automata emptiness,\u201d in IEEE Real-Time Systems Symposium, 1992, pp. 157-166.","DOI":"10.1109\/REAL.1992.242667"},{"key":"5087919_CR2","unstructured":"A. Aziz, V. Singhal, G. Swamy, and R. Brayton, \u201cMinimizing interacting finite state machines:Acompositional approach to language containment,\u201d in International Conference on Computer Design, 1994."},{"key":"5087919_CR3","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, D. Geist, R. Gewirtzman, and M. Yoeli, \u201cMethodology and system for practical formal verification of reactive hardware,\u201d in Proc. 6th Conference on Computer Aided Verification, Stanford, June 1994, Vol. 818 of Lecture Notes in Computer Science, pp. 182-193.","DOI":"10.1007\/3-540-58179-0_53"},{"key":"5087919_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/BFb0014325","volume-title":"Symbolic bisimulation for timed processes","author":"M. Boreale","year":"1996","unstructured":"M. Boreale, \u201cSymbolic bisimulation for timed processes,\u201d in International Conference on Algebraic Methodology and Software Technology, Vol. 1101 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1996, pp. 321-335."},{"key":"5087919_CR5","series-title":"Lecture Notes in Computer Science","first-page":"197","volume-title":"Minimal model generation","author":"A. Bouajjani","year":"1990","unstructured":"A. Bouajjani, J.-C. Fernandez, and N. Halbwachs, \u201cMinimal model generation,\u201d in E. Clarke and R. Kurshan (Eds.), International Conference on Computer-Aided Verification, Vol. 531 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1990, pp. 197-203."},{"key":"5087919_CR6","doi-asserted-by":"crossref","unstructured":"A. Bouali, \u201cXEVE, an ESTEREL verification environment,\u201d in International Conference on Computer-Aided Verification, 1998, pp. 500-504.","DOI":"10.1007\/BFb0028770"},{"key":"5087919_CR7","series-title":"Lecture Notes in Computer Science","first-page":"96","volume-title":"Symbolic bisimulation minimization","author":"A. Bouali","year":"1992","unstructured":"A. Bouali and R. de Simone, \u201cSymbolic bisimulation minimization,\u201d in International Conference on Computer-Aided Verification, Vol. 663 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1992, pp. 96-108."},{"key":"5087919_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1007\/3-540-61474-5_98","volume-title":"The FC2TOOLS set","author":"A. Bouali","year":"1996","unstructured":"A. Bouali, A. Ressouche, V. Roy, and R. de Simone, \u201cThe FC2TOOLS set,\u201d in International Conference on Computer-Aided Verification, Vol. 1102 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1996, pp. 441-445."},{"key":"5087919_CR9","unstructured":"M. Bourdell\u00e8s, \u201cThe steam boiler controller problem in ESTEREL and its verification by means of symbolic analysis,\u201d Technical Report 3285, INRIA Sophia Antipolis, October 1997."},{"issue":"1","key":"5087919_CR10","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E. Clarke","year":"1996","unstructured":"E. Clarke, R. Enders, T. Filkorn, and S. Jha, \u201cExploiting symmetry in temporal logic model checking,\u201d Formal Methods in System Design, Vol. 9, No. 1\/2, pp. 77-104, 1996.","journal-title":"Formal Methods in System Design"},{"key":"5087919_CR11","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, and D. Long, \u201cModel-checking and abstraction,\u201d in ACM Symposium on Principles of Programming Languages, 1992, pp. 343-354.","DOI":"10.1145\/143165.143235"},{"key":"5087919_CR12","doi-asserted-by":"crossref","unstructured":"E. Clarke, M. Khaira, and X. Zhao, \u201cWord level model checking-Avoiding the Pentium FDIV error,\u201d in International Conference on Design Automation, June 1996, pp. 645-648.","DOI":"10.1109\/DAC.1996.545654"},{"key":"5087919_CR13","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1109\/6.499951","volume":"33","author":"E. Clarke","year":"1986","unstructured":"E. Clarke and R. Kurshan, \u201cComputer aided verification,\u201d IEEE Spectrum, Vol. 33, pp. 61-67, 1986.","journal-title":"IEEE Spectrum"},{"key":"5087919_CR14","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, J. Gada, P. Lewis, S.A. Smolka, O. Sokolsky, and S. Zhang, \u201cThe concurrency factory-Practical tools for specification, simulation, verification, and implementation of concurrent systems,\u201d in Proc. of DIMACS Workshop on Specification of Parallel Algorithms, Vol. 18 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 1994, pp. 75-90.","DOI":"10.1090\/dimacs\/018\/06"},{"issue":"1","key":"5087919_CR15","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland, J. Parrow, and B. Steffen, \u201cThe concurrency workbench: A semantics-based tool for the verification of concurrent systems,\u201d ACM Transactions on Programming Languages and Systems, Vol. 15, No. 1, pp. 36-72, 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5087919_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/3-540-61474-5_87","volume-title":"The NCSU concurrency workbench","author":"R. Cleaveland","year":"1996","unstructured":"R. Cleaveland and S. Sims, \u201cThe NCSU concurrency workbench,\u201d in International Conference on Computer-Aided Verification, Vol. 1102 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1996, pp. 394-397."},{"key":"5087919_CR17","unstructured":"S.J. Creese and A. Roscoe, \u201cTTP: A case study in combining induction and data independence,\u201d unpublished draft manuscript, 1998."},{"key":"5087919_CR18","unstructured":"D. Dams, \u201cAbstract interpretation and partition refinement for model checking,\u201d Ph.D. Thesis, Technische Universiteit Eindhoven, 1996."},{"key":"5087919_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/3-540-56922-7_39","volume-title":"Generation of reduced models for checking fragments of CTL","author":"D. Dams","year":"1993","unstructured":"D. Dams, O. Grumberg, and R. Gerth, \u201cGeneration of reduced models for checking fragments of CTL,\u201d in International Conference on Computer-Aided Verification, Vol. 697 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1993, pp. 479-490."},{"key":"5087919_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"The formal design of 1M-gate ASICs","author":"A.T. Eiriksson","year":"1998","unstructured":"A.T. Eiriksson, \u201cThe formal design of 1M-gate ASICs,\u201d in G. Gopalakrishnan and P. Windley (Eds.), International Conference on Formal Methods in Computer-Aided Verification, Vol. 1522 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1998."},{"key":"5087919_CR21","series-title":"Rapport SPECTRE","volume-title":"Ald\u00e9baran: A tool for verification of communicating processes","author":"J.-C. Fernandez","year":"1989","unstructured":"J.-C. Fernandez, \u201cAld\u00e9baran: A tool for verification of communicating processes,\u201d Rapport SPECTRE C14, Laboratoire de G\u00e9nie Informatique, Institut IMAG, Grenoble, September 1989."},{"key":"5087919_CR22","series-title":"Lecture Notes in Computer Science","first-page":"181","volume-title":"\u201cOn the fly\u201d verification of behavioral equivalences and preorders","author":"J.-C. Fernandez","year":"1991","unstructured":"J.-C. Fernandez and L. Mounier, \u201c \u201cOn the fly\u201d verification of behavioral equivalences and preorders,\u201d in International Conference on Computer-Aided Verification, Vol. 575 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1991, pp. 181-191."},{"key":"5087919_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/3-540-49519-3_9","volume-title":"Bisimulation minimization in an automata-theoretic verification framework","author":"K. Fisler","year":"1998","unstructured":"K. Fisler and M.Y. Vardi, \u201cBisimulation minimization in an automata-theoretic verification framework,\u201d in G. Gopalakrishnan and P. Windley (Eds.), International Conference on Formal Methods in Computer-Aided Verification, Vol. 1522 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1998, pp. 115-132."},{"issue":"3","key":"5087919_CR24","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D. Long, \u201cModel checking and modular verification,\u201d ACM Trans. on Programming Languages and Systems, Vol. 16, No. 3, pp. 843-871, 1994.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"5087919_CR25","doi-asserted-by":"crossref","unstructured":"N. Halbwachs and D. Peled (Eds.), International Conference on Computer-Aided Verification, Vol. 1633 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1999.","DOI":"10.1007\/3-540-48683-6"},{"key":"5087919_CR26","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1016\/0304-3975(94)00172-F","volume":"138","author":"M. Hennessey","year":"1995","unstructured":"M. Hennessey and H. Lin, \u201cSymbolic bisimulations,\u201d Theoretical Computer Science, Vol. 138, pp. 353-389, 1995.","journal-title":"Theoretical Computer Science"},{"key":"5087919_CR27","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"M. Hennessy and R. Milner, \u201cAlgebraic laws for nondeterminism and concurrency,\u201d Journal of ACM, Vol. 32, pp. 137-161, 1985.","journal-title":"Journal of ACM"},{"key":"5087919_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-64358-3","volume-title":"Computer Aided Verification, Proc. 10th Int. Conference","author":"T. Henzinger","year":"1998","unstructured":"T. Henzinger, O. Kupferman, and S. Qadeer, \u201cFrom pre-historic to post-modern symbolic model checking,\u201d in Computer Aided Verification, Proc. 10th Int. Conference, Vol. 1427 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1998."},{"key":"5087919_CR29","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/B978-0-12-417750-5.50022-1","volume-title":"Theory of Machines and Computations","author":"J.E. Hopcroft","year":"1971","unstructured":"J.E. Hopcroft, \u201cAn n log n algorithm for minimizing states in a finite automaton,\u201d in Z. Kohavi and A. Paz (Eds.), Theory of Machines and Computations, Academic Press, San Diego, CA, 1971, pp. 189-196."},{"key":"5087919_CR30","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P.C. Kanellakis","year":"1990","unstructured":"P.C. Kanellakis and S.A. Smolka, \u201cCCS expressions, finite state processes, and three problems of equivalence,\u201d Information and Computation, Vol. 86, pp. 43-68, 1990.","journal-title":"Information and Computation"},{"key":"5087919_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/3-540-60218-6_31","volume-title":"Proc. 6th Conference on Concurrency Theory","author":"O. Kupferman","year":"1995","unstructured":"O. Kupferman and M.Y. Vardi, \u201cOn the complexity of branching modular model checking,\u201d in Proc. 6th Conference on Concurrency Theory, Vol. 962 of Lecture Notes in Computer Science, Philadelphia, Springer-Verlag, Berlin, 1995, pp. 408-422."},{"key":"5087919_CR32","series-title":"Lecture Notes in Computer Science","volume-title":"Model checking of safety properties","author":"O. Kupferman","year":"1999","unstructured":"O. Kupferman and M.Y. Vardi, \u201cModel checking of safety properties,\u201d in International Conference on Computer-Aided Verification, Vol. 1633 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1999."},{"key":"5087919_CR33","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"R.P. Kurshan, Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach, Princeton University Press, Princeton, NJ, 1994."},{"key":"5087919_CR34","doi-asserted-by":"crossref","unstructured":"D. Lee and M. Yannakakis, \u201cOnline minimization of transition systems,\u201d in Proc. 24th ACM Symposium on Theory of Computing, Victoria, May 1992, pp. 264-274.","DOI":"10.1145\/129712.129738"},{"key":"5087919_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R. Milner","year":"1980","unstructured":"R. Milner, A Calculus of Communicating Systems, Vol. 92 of Lecture Notes in Computer Science, Springer Verlag, Berlin, 1980."},{"key":"5087919_CR36","doi-asserted-by":"crossref","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"R. Paige and R. Tarjan, \u201cThree partition refinement algorithms,\u201d SIAM Journal of Computing, Vol. 16, pp. 973-989, 1987.","journal-title":"SIAM Journal of Computing"},{"key":"5087919_CR37","unstructured":"F. Rahim, \u201cProperty-dependent reduction of finite state machines for modular model checking: Application to VHDL with computational results,\u201d in Proc. Third IEEE International High Level Design Validation and Test Workshop (HLDVT), 1998."},{"key":"5087919_CR38","series-title":"Series in Computer Science","volume-title":"The Theory and Practice of Concurrency","author":"A. Roscoe","year":"1998","unstructured":"A. Roscoe, The Theory and Practice of Concurrency, Series in Computer Science, Prentice-Hall, Englewood Cliffs, NJ, 1998."},{"key":"5087919_CR39","series-title":"Lecture Notes in Computer Science","first-page":"428","volume-title":"VIS: A system for verification and synthesis","author":"The VIS Group","year":"1996","unstructured":"The VIS Group, \u201cVIS: A system for verification and synthesis,\u201d in R. Alur and T. Henzinger (Eds.), International Conference on Computer-Aided Verification, Vol. 1102 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1996, pp. 428-432."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1016091902809.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1016091902809\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1016091902809.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:20:30Z","timestamp":1754421630000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1016091902809"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,7]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,7]]}},"alternative-id":["5087919"],"URL":"https:\/\/doi.org\/10.1023\/a:1016091902809","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,7]]}}}