{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:46:13Z","timestamp":1762458373061,"version":"3.41.0"},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"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":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1023\/a:1027328830731","type":"journal-article","created":{"date-parts":[[2003,11,9]],"date-time":"2003-11-09T22:46:39Z","timestamp":1068417999000},"page":"73-103","source":"Crossref","is-referenced-by-count":73,"title":["From Bisimulation to Simulation: Coarsest Partition Problems"],"prefix":"10.1007","volume":"31","author":[{"given":"R.","family":"Gentilini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"Piazza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Policriti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5147666_CR1","unstructured":"Aczel, P.: Non-Well-Founded Sets, CSLI Lecture Notes 14, Stanford University Press, 1988."},{"key":"5147666_CR2","doi-asserted-by":"crossref","unstructured":"Bloem, R., Gabow, H. N. and Somenzi, F.: An algorithm for strongly connected component analysis in n log n symbolic steps, in W. A. Hunt, Jr. and S. D. Johnson (eds.), Proceedings of International Conference on Formal Methods in Computer-Aided Design (FMCAD'00), Lecture Notes in Comput. Sci. 1954, Springer, 2000, pp. 37-54.","DOI":"10.1007\/3-540-40922-X_4"},{"key":"5147666_CR3","unstructured":"Bloom, B.: Ready simulation, bisimulation, and the semantics of CCS-like languages, Ph.D. thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, August 1989."},{"issue":"3","key":"5147666_CR4","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0167-6423(95)00003-B","volume":"24","author":"B. Bloom","year":"1995","unstructured":"Bloom, B. and Paige, R.: Transformational design and implementation of a new efficient solution to the ready simulation problem, Science of Computer Programming\n                  24(3) (June 1995), 189-220.","journal-title":"Science of Computer Programming"},{"key":"5147666_CR5","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Fernandez, J. C. and Halbwachs, N.:Minimal model generation, in E. Clarke and R. Kurshan (eds.), Proceedings of International Conference on Computer Aided Verification (CAV'90), Lecture Notes in Comput. Sci. 531, Springer, 1990, pp. 197-203.","DOI":"10.1007\/BFb0023733"},{"key":"5147666_CR6","doi-asserted-by":"crossref","unstructured":"Bouali, A.: XEVE, an ESTEREL verification environment, in A. J. Hu and M. Y. Vardi (eds.), Proceedings of International Conference on Computer Aided Verification (CAV'98), Lecture Notes in Comput. Sci. 1427, Springer, 1998, pp. 500-504.","DOI":"10.1007\/BFb0028770"},{"key":"5147666_CR7","doi-asserted-by":"crossref","unstructured":"Bouali, A. and de Simone, R.: Symbolic bisimulation minimization, in G. von Bochmann and D. K. Probst (eds.), Proceedings of International Conference on Computer Aided Verification (CAV'92), Lecture Notes in Comput. Sci. 663, Springer, 1992, pp. 96-108.","DOI":"10.1007\/3-540-56496-9_9"},{"key":"5147666_CR8","doi-asserted-by":"crossref","unstructured":"Bryant, R. E.: Symbolic manipulation of Boolean functions using a graphical representation, in Proceedings of Design Automation Conference (DAC'85), 1985.","DOI":"10.1145\/317825.317964"},{"key":"5147666_CR9","doi-asserted-by":"crossref","unstructured":"Bustan, D. and Grumberg, O.: Simulation based minimization, in D. A. McAllester (ed.), Proceedings of International Conference on Automated Deduction (CADE00), Lecture Notes in Comput. Sci. 1831, Springer, 2000, pp. 255-270.","DOI":"10.1007\/10721959_20"},{"key":"5147666_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E. M. and Emerson, E. A.: Design and synthesis of synchronization skeletons using brancing time temporal logic, in Proceedings ofWorkshop on Logic of Programs, Lecture Notes in Comput. Sci. 131, Springer, 1982, pp. 52-71.","DOI":"10.1007\/BFb0025774"},{"key":"5147666_CR11","unstructured":"Clarke, E. M., Grumberg, O. and Peled, D. A.: Model Checking, MIT Press, 1999."},{"issue":"1","key":"5147666_CR12","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Parrow, J. and Steffen, B.: The concurrency workbench: A semantics based tool for the verification of concurrent systems, ACM Transactions on Programming Languages and Systems\n                  15(1) (January 1993), 36-72.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5147666_CR13","doi-asserted-by":"crossref","unstructured":"Cleaveland, R. and Sims, S.: The NCSU concurrency workbench, in R. Alur and T. A. Henzinger (eds.), Proceedings of International Conference on Computer Aided Verification (CAV'96), Lecture Notes in Comput. Sci. 1102, Springer, 1996, pp. 394-397.","DOI":"10.1007\/3-540-61474-5_87"},{"key":"5147666_CR14","doi-asserted-by":"crossref","unstructured":"Cleaveland, R. and Steffen, B.: A linear-time model-checking algorithm for the alternation free modal mu-calculus, in K. G. Larsen and A. Skou (eds.), Proceedings of International Conference on Computer Aided Verification (CAV'91), Lecture Notes in Comput. Sci. 575, Springer, 1992, pp. 48-58.","DOI":"10.1007\/3-540-55179-4_6"},{"key":"5147666_CR15","doi-asserted-by":"crossref","unstructured":"Cleaveland, R. and Tan, L.: Simulation revised, in T. Margaria and W. Yi (eds.), Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01), Lecture Notes in Comput. Sci. 2031, Springer, 2001, pp. 480-495.","DOI":"10.1007\/3-540-45319-9_33"},{"key":"5147666_CR16","doi-asserted-by":"crossref","unstructured":"Dams, D., Gerth, R. and Grumberg, O.: Generation of reduced models for checking fragments of CTL, in C. Courcoubetis (ed.), Proceedings of International Conference on Computer Aided nVerification (CAV'93), Lecture Notes in Comput. Sci. 697, Springer, 1993, pp. 479-490.","DOI":"10.1007\/3-540-56922-7_39"},{"issue":"2","key":"5147666_CR17","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"Dams, D., Gerth, R. and Grumberg, O.: Abstract interpretation of reactive systems, ACM Transactions on Programming Languages and Systems\n                  19(2) (March 1997), 253-291.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5147666_CR18","doi-asserted-by":"crossref","unstructured":"Dovier, A., Gentilini, R., Piazza, C. and Policriti, A.: Rank-based symbolic bisimulation (and model checking), in Ruy J. Guerra B. de Queiroz (ed.), Proceedings of Workshop on Language, Logic, Information, and Computation (Wollic'02), ENTCS 67, Elsevier Science, 2002, pp. 167-184.","DOI":"10.1016\/S1571-0661(04)80547-4"},{"key":"5147666_CR19","doi-asserted-by":"crossref","unstructured":"Dovier, A., Piazza, C. and Policriti, A.: A fast bisimulation algorithm, in G. Berry, H. Comon and A. Finkel (eds.), Proceedings of International Conference on Computer Aided Verification (CAV'01), Lecture Notes in Comput. Sci. 2102, Springer, 2001, pp. 79-90.","DOI":"10.1007\/3-540-44585-4_8"},{"key":"5147666_CR20","unstructured":"Dovier, A., Piazza, C. and Policriti, A.: A fast bisimulation algorithm, J. Theoret. Comput. Sci. (2003). Accepted for publication, to appear."},{"key":"5147666_CR21","doi-asserted-by":"crossref","unstructured":"Fernandez, J. C., Garavel, H., Kerbrat, A., Mateescu, R., Mounier, L. and Sighireanu, M.: CADP: A protocol validation and verification toolbox, in R. Alur and T. A. Henzinger (eds.), Proceedings of International Conference on Computer Aided Verification (CAV'96), Lecture Notes in Comput. Sci. 1102, Springer, 1996, pp. 437-440.","DOI":"10.1007\/3-540-61474-5_97"},{"key":"5147666_CR22","doi-asserted-by":"crossref","unstructured":"Fisler, K. and Vardi, M. Y.: Bisimulation and model checking, in L. Pierre and T. Kropf (eds.), Proceedings of Correct Hardware Design and Verification Methods (CHARME'99), Lecture Notes in Comput. Sci. 1703, Springer, 1999, pp. 338-341.","DOI":"10.1007\/3-540-48153-2_29"},{"issue":"9","key":"5147666_CR23","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1109\/32.629493","volume":"23","author":"R. Focardi","year":"1997","unstructured":"Focardi, R. and Gorrieri, R.: The compositional security checker: A tool for the verification of information flow security properties, IEEE Transaction on Software Engineering\n                  23(9) (1997), 550-571.","journal-title":"IEEE Transaction on Software Engineering"},{"issue":"10","key":"5147666_CR24","first-page":"493","volume":"IV","author":"M. Forti","year":"1983","unstructured":"Forti, M. and Honsell, F.: Set theory with free construction principles, Ann. Scuola Norm. Sup. Pisa Cl. Sc.\n                  IV(10) (1983), 493-522.","journal-title":"Ann. Scuola Norm. Sup. Pisa Cl. Sc."},{"key":"5147666_CR25","doi-asserted-by":"crossref","unstructured":"Gentilini, R., Piazza, C. and Policriti, A.: Simulation as coarsest partition problem, in J. P. Katoen and P. Stevens (eds.), International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02), Lecture Notes in Comput. Sci. 2280, Springer, 2002, pp. 415-430.","DOI":"10.1007\/3-540-46002-0_29"},{"key":"5147666_CR26","doi-asserted-by":"crossref","unstructured":"Gentilini, R., Piazza, C. and Policriti, A.: Simulation reduction as constraint, in M. Comini and M. Falaschi (eds.), Proceedings ofWorkshop on Functional and Constraint Logic Programming (WFLP'02), ENTCS 76, Elsevier Science, 2002.","DOI":"10.1016\/S1571-0661(04)80791-6"},{"key":"5147666_CR27","volume-title":"From bisimulation to simulation: Coarsest partition problems","author":"R. Gentilini","year":"2003","unstructured":"Gentilini, R., Piazza, C. and Policriti, A.: From bisimulation to simulation: Coarsest partition problems, RR 12-2003, Dep. of Computer Science, University of Udine, Italy, 2003."},{"key":"5147666_CR28","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BF00264025","volume":"2","author":"D. Gries","year":"1973","unstructured":"Gries, D.: Describing an algorithm by Hopcroft, Acta Inform.\n                  2 (1973), 97-109.","journal-title":"Acta Inform."},{"issue":"3","key":"5147666_CR29","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O. and Long, D. E.: Model checking and modular verification, ACM Transactions on Programming Languages and Systems\n                  16(3) (May 1994), 843-871.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5147666_CR30","doi-asserted-by":"crossref","unstructured":"Henzinger, M. R., Henzinger, T. A. and Kopke, P. W.: Computing simulations on finite and infinite graphs, in Proceedings of Symposium on Foundations of Computer Science (FOCS'95), IEEE Computer Society Press, 1995, pp. 453-462.","DOI":"10.1109\/SFCS.1995.492576"},{"key":"5147666_CR31","doi-asserted-by":"crossref","unstructured":"Hopcroft, J. E.: An n log n algorithm for minimizing states in a finite automaton, in Z. Kohavi and A. Paz (eds.), Theory of Machines and Computations, Academic Press, 1971, pp. 189-196.","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"5147666_CR32","doi-asserted-by":"crossref","unstructured":"Kanellakis, C. and Smolka, S. A.: CCS expressions, finite state processes, and three problems of equivalence, in ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC), 1983, pp. 228-240.","DOI":"10.1145\/800221.806724"},{"issue":"1","key":"5147666_CR33","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P. C. Kannellakis","year":"1990","unstructured":"Kannellakis, P. C. and Smolka, S. A.: CCS expressions, finite state processes, and three problems of equivalence, Inform. and Comput.\n                  86(1) (1990), 43-68.","journal-title":"Inform. and Comput."},{"key":"5147666_CR34","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/S0304-3975(99)00150-4","volume":"250","author":"T. Knuutila","year":"2001","unstructured":"Knuutila, T.: Re-describing an algorithm by Hopcroft, Theoret. Comput. Sci.\n                  250 (2001) 333-363.","journal-title":"Theoret. Comput. Sci."},{"key":"5147666_CR35","doi-asserted-by":"crossref","unstructured":"Lee, D. and Yannakakis, M.: Online minimization of transition systems, in Proceedings of ACM Symposium on Theory of Computing (STOC'92), ACM Press, 1992, pp. 264-274.","DOI":"10.1145\/129712.129738"},{"key":"5147666_CR36","doi-asserted-by":"crossref","unstructured":"McMillan, K. L.: Symbolic Model Checking: An Approach to the State Explosion Problem, Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"5147666_CR37","unstructured":"Milner, R.: An algebraic definition of simulation between programs, in Proceedings of International Joint Conference on Artificial Intelligence (IJCAI'71), Morgan Kaufmann,1971, pp. 481-489."},{"key":"5147666_CR38","doi-asserted-by":"crossref","unstructured":"Milner, R.: A calculus of communicating systems, in G. Goos and J. Hartmanis (eds.), Lecture Notes in Comput. Sci. 92, Springer, 1980.","DOI":"10.1007\/3-540-10235-3"},{"issue":"6","key":"5147666_CR39","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"Paige, R. and Tarjan, R. E.: Three partition refinement algorithms, SIAM J. Comput.\n                  16(6) (1987), 973-989.","journal-title":"SIAM J. Comput."},{"issue":"1","key":"5147666_CR40","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/0304-3975(85)90159-8","volume":"40","author":"R. Paige","year":"1985","unstructured":"Paige, R., Tarjan, R. E. and Bonic, R.: A linear time solution to the single function coarsest partition problem, Theoret. Comput. Sci.\n                  40(1) (1985), 67-84.","journal-title":"Theoret. Comput. Sci."},{"key":"5147666_CR41","doi-asserted-by":"crossref","unstructured":"Park, D.: Concurrency and automata on infinite sequences, in P. Deussen (ed.), Proceedings of International Conference on Theorical Computer Science (TCS'81), Lecture Notes in Comput. Sci. 104, Springer, 1981, pp. 167-183.","DOI":"10.1007\/BFb0017309"},{"key":"5147666_CR42","unstructured":"Piazza, C.: Computing in Non Standard Set Theories, Ph.D. thesis, Department of Computer Science, University of Udine, 2002. Electronically available from http:\/\/www.dimi.uniud.it\/~piazza."},{"key":"5147666_CR43","unstructured":"Piazza, C. and Policriti, A.: Ackermann encoding, bisimulations, and OBDD's, in M. Leuschel, A. Podelski, C. R. Ramakrishnan and U. Ultes-Nitsche (eds.), Proceedings of International Workshop on Verification and Computational Logic (VCL'01), Southampton University Technical Report DSSE-TR-2001-3, ACM Digital Library, 2001, pp. 43-53."},{"key":"5147666_CR44","unstructured":"Roscoe, W. R.: A Classical Mind: Essays in Honour of C. A. R. Hoare, Prentice Hall, 1994, Chapter \u2018Model Checking CSP\u2019."},{"key":"5147666_CR45","unstructured":"van Benthem, J.: Modal correspondence theory, Ph.D. thesis, Universiteit van Amsterdam, Instituut voor Logica en Grondslagenonderzoek van Exacte Wetenschappen, 1976."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1027328830731.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1027328830731\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1027328830731.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:35:58Z","timestamp":1749123358000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1027328830731"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["5147666"],"URL":"https:\/\/doi.org\/10.1023\/a:1027328830731","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}