{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:19Z","timestamp":1761611299001,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540564966"},{"type":"electronic","value":"9783540475729"}],"license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"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":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56496-9_9","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:13:23Z","timestamp":1330254803000},"page":"96-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":28,"title":["Symbolic bisimulation minimisation"],"prefix":"10.1007","author":[{"given":"Amar","family":"Bouali","sequence":"first","affiliation":[]},{"given":"Robert","family":"de Simone","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"9_CR1","unstructured":"A. Arnold and M. Nivat. Comportements de processus. In Les Math\u00e9matiques de l'Informatique, pages 35\u201368. Colloque AFCET, 1982."},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"D. Austry and G. Boudol. Alg\u00e8bre de processus et synchronisation. Theorical Computer Sciences, 1(30), 1984.","DOI":"10.1016\/0304-3975(84)90067-7"},{"key":"9_CR3","unstructured":"A. Bouali. Weak and branching bisimulation in fctool. Technical Report 1575, INRIA, 1991."},{"issue":"8","key":"9_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"Randal E. E. Bryant","year":"1986","unstructured":"Randal E. Bryant. Graph-based algorithms for boolean function manipulaiton. Transactions on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"Transactions on Computers"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 and beyond. In 5 th IEEE Symposium on Logic in Computer Science, pages 428\u2013439, Philadelphia, 1990.","DOI":"10.1109\/LICS.1990.113767"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench. In Automatic Verification Methods for Finite State Systems, pages 24\u201337. LNCS, 1989.","DOI":"10.1007\/3-540-52148-8_3"},{"key":"9_CR7","unstructured":"O. Coudert, C. Berthet, and J.C. Madre. Verification of sequential machines using boolean vectors. In IFIP Internationnal Workshop, Applied Formal Methods for Correct VLSI design, Leuven, November 1990."},{"key":"9_CR8","volume-title":"CONCUR'91","author":"R. Simone de","year":"1991","unstructured":"R. de Simone and A. Bouali. Causal models for rationnal algebraic processes. In J.C.M. Baeten and J.F. Groote, editors, 2nd internationnal Conference on Concurrency Theory, Amsterdam, August 1991. CONCUR'91, Springer-Verlag."},{"key":"9_CR9","unstructured":"R. Enders, T. Filkorn, and D. Taubner. Generating bdds for symbolic model checking. In Third Workshop on Computer Aided Verification, volume 1, pages 263\u2013278. University of Aalborg, July 1991."},{"key":"9_CR10","unstructured":"J.C. Fernandez. Ald\u00e9baran: un syst\u00e8me de v\u00e9rificatoin par r\u00e9duction de processus communiquants. PhD thesis, Grenoble, 1989."},{"key":"9_CR11","first-page":"232","volume-title":"Automatic Verification Methods For Finite State Systems","author":"J. C. Godskesen","year":"1989","unstructured":"J.C. Godskesen, K.G. Larsen, and M. Zeeberg. Tav, tools for automatic verification. In Automatic Verification Methods For Finite State Systems, pages 232\u2013246, Grenoble, France, 1989. LNCS, Springer-Verlag."},{"key":"9_CR12","unstructured":"J.F. Groote and F. Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. ICALP '90, 1990."},{"key":"9_CR13","unstructured":"G.J. Holzmann. Algorithms for automated protocol validation. In International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, June 1989."},{"key":"9_CR14","unstructured":"C. Jard and T. J\u00e9ron. Bounded-memory algorithm for verification on-the-fly. In Larsen. K.G. and A. Skou, editors, Third Workshop on Computer Aided Verification, volume 1, pages 251\u2013262, July 1991."},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"P.C. Kanellakis and S.A. Smolka. Ccs expressions, finite state processes, and three problems of equivalence. In ACM Symposium on Principles of Distributed Computing, pages 228\u2013240, 1983.","DOI":"10.1145\/800221.806724"},{"key":"9_CR16","unstructured":"B. Lin and A.R. Newton. Efficient manipulation of equivalence relations and classes. In ACM International Workshop on Formal Methods in VLSI design, Miami, January 1991."},{"key":"9_CR17","unstructured":"Robin Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989."},{"key":"9_CR18","unstructured":"Laurent Mounier. M\u00e9thodes de v\u00e9rification de sp\u00e9cifications comportementales: \u00e9tude et mise en oeuvre. PhD thesis, LGI Grenoble, 1991."},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"R. Paige and R. Tarjan. Three partition refinement algorithms. SIAM, 16(6), 1987.","DOI":"10.1137\/0216062"},{"key":"9_CR20","volume-title":"Technical report","author":"H. Qin","year":"1991","unstructured":"Huajun Qin. Efficient verification of determinate processes. Technical report, Dep. of Comp. Sc., SUNY, Stony Brook, 1991."},{"key":"9_CR21","unstructured":"M. Raynal. Algorithmes du Parall\u00e9lisme: le Probl\u00e8me de l'Exclusion Mutuelle. Dunod Informatique, 1984."},{"key":"9_CR22","unstructured":"H.J. Touati, H. Savoj, B. Lin, and Sangiovanni-Vincentelli. Implicit state enumeration of finite state machines using bdd's. In Internationnal Conference on Computer Aided Design, 1990."},{"key":"9_CR23","unstructured":"R.J. Van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). Information processing '89 (G.X. Ritter, ed.) Elsevier Science, pages 613\u2013618, 1984."},{"key":"9_CR24","unstructured":"D. Vergamini. V\u00e9rification de r\u00e9seau d'automates finis par equivalence observationnelle: le syst\u00e8me AUTO. PhD thesis, Universit\u00e9 de Nice, 1987."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56496-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T21:49:23Z","timestamp":1742593763000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56496-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540564966","9783540475729"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-56496-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]},"assertion":[{"value":"30 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}