{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:52Z","timestamp":1776333412106,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540472377","type":"print"},{"value":"9783540472384","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901914_35","type":"book-chapter","created":{"date-parts":[[2006,10,10]],"date-time":"2006-10-10T05:21:43Z","timestamp":1160457703000},"page":"477-492","source":"Crossref","is-referenced-by-count":35,"title":["Sigref \u2013 A Symbolic Bisimulation Tool Box"],"prefix":"10.1007","author":[{"given":"Ralf","family":"Wimmer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Herbstritt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kelley","family":"Strampp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"35_CR1","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Herbstritt, M., Becker, B.: Minimization of Large State Spaces using Symbolic Branching Bisimulation. In: Proc.\u00a0of IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS), pp. 9\u201314 (2006)","DOI":"10.1109\/DDECS.2006.1649562"},{"key":"35_CR2","doi-asserted-by":"crossref","unstructured":"Chehaibar, G., et al.: Specification and Verification of the PowerScale TM Bus Arbitration Protocol: An Industrial Experiment with LOTOS. In: Proc.\u00a0of FORTE, vol.\u00a069, pp. 435\u2013450 (1996)","DOI":"10.1007\/978-0-387-35079-0_28"},{"key":"35_CR3","unstructured":"Giannakopoulou, D.: Model Checking for Concurrent Software Architectures. PhD thesis, Imperial College, University of London (1999)"},{"issue":"5","key":"35_CR4","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BF01211911","volume":"8","author":"S. Graf","year":"1996","unstructured":"Graf, S., Steffen, B., Luttgen, G.: Compositional minimisation of finite state systems using interface specifications. Formal Asp. of Comp.\u00a08(5), 607\u2013616 (1996)","journal-title":"Formal Asp. of Comp."},{"issue":"1","key":"35_CR5","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P. Kanellakis","year":"1990","unstructured":"Kanellakis, P., Smolka, S.: CCS expressions, finite state processes, and three problems of equivalence. Information and Computation\u00a086(1), 43\u201368 (1990)","journal-title":"Information and Computation"},{"issue":"6","key":"35_CR6","doi-asserted-by":"publisher","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 Jour.\u00a0on Computing\u00a016(6), 973\u2013989 (1987)","journal-title":"SIAM Jour.\u00a0on Computing"},{"issue":"2","key":"35_CR7","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. Burch","year":"1992","unstructured":"Burch, J., et al.: Symbolic Model Checking: 1020 States and Beyond. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"35_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/BFb0023733","volume-title":"Computer-Aided Verification","author":"A. Bouajjani","year":"1991","unstructured":"Bouajjani, A., Fernandez, J.C., Halbwachs, N.: Minimal model generation. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531, pp. 197\u2013203. Springer, Heidelberg (1991)"},{"key":"35_CR9","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1016\/0167-6423(92)90018-7","volume":"18","author":"A. Bouajjani","year":"1992","unstructured":"Bouajjani, A., Fernandez, J.C., Halbwachs, N., Ratel, C., Raymond, P.: Minimal state graph generation. Science of Computer Programming\u00a018, 247\u2013269 (1992)","journal-title":"Science of Computer Programming"},{"key":"35_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/3-540-56496-9_9","volume-title":"Computer Aided Verification","author":"A. Bouali","year":"1993","unstructured":"Bouali, A., de Simone, R.: Symbolic Bisimulation Minimisation. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 96\u2013108. Springer, Heidelberg (1993)"},{"issue":"1","key":"35_CR11","first-page":"113","volume":"89","author":"S. Blom","year":"2003","unstructured":"Blom, S., Orzan, S.: Distributed Branching Bisimulation Reduction of State Spaces. ENTCS\u00a089(1), 113\u2013990 (2003)","journal-title":"ENTCS"},{"key":"35_CR12","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"35_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communication Systems","author":"R. Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communication Systems. LNCS, vol.\u00a092. Springer, Heidelberg (1980)"},{"key":"35_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-15670-4_10","volume-title":"Seminar on Concurrency","author":"R. Milner","year":"1985","unstructured":"Milner, R.: Lectures on a Calculus for Communicating Systems. In: Brookes, S.D., Winskel, G., Roscoe, A.W. (eds.) Seminar on Concurrency. LNCS, vol.\u00a0197, pp. 197\u2013220. Springer, Heidelberg (1985)"},{"issue":"3","key":"35_CR15","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R. Glabbeek van","year":"1996","unstructured":"van Glabbeek, R., Weijland, W.: Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM\u00a043(3), 555\u2013600 (1996)","journal-title":"Journal of the ACM"},{"key":"35_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-18088-5_8","volume-title":"Automata, Languages and Programming","author":"J. Baeten","year":"1987","unstructured":"Baeten, J., van Glabbeek, R.: Another Look at Abstraction in Process Algebra. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol.\u00a0267, pp. 84\u201394. Springer, Heidelberg (1987)"},{"key":"35_CR17","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1016\/S0304-3975(03)00277-9","volume":"309","author":"J.A. Bergstra","year":"2003","unstructured":"Bergstra, J.A., Ponse, A., van der Zwaag, M.B.: Branching time and orthogonal bisimulation equivalence. Theor. Comp. Sci.\u00a0309, 313\u2013355 (2003)","journal-title":"Theor. Comp. Sci."},{"key":"35_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/3-540-10828-9_52","volume-title":"Proc. of CAAP","author":"R. Milner","year":"1981","unstructured":"Milner, R.: A Modal Characterization of Observable Machine-Behaviour. In: Astesiano, E., B\u00f6hm, C. (eds.) CAAP 1981. LNCS, vol.\u00a0112, pp. 25\u201334. Springer, Heidelberg (1981)"},{"issue":"1","key":"35_CR19","doi-asserted-by":"crossref","first-page":"171","DOI":"10.3233\/FI-1992-16206","volume":"16","author":"U. Montanari","year":"1992","unstructured":"Montanari, U., Sassone, V.: Dynamic congruence vs. progressing bisimulation for CCS. Fundam. Inform.\u00a016(1), 171\u2013199 (1992)","journal-title":"Fundam. Inform."},{"key":"35_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1007\/3-540-54233-7_126","volume-title":"Automata, Languages and Programming","author":"A. Bouajjani","year":"1991","unstructured":"Bouajjani, A., et al.: Safety for Branching Time Semantics. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510, pp. 76\u201392. Springer, Heidelberg (1991)"},{"key":"35_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/3-540-57208-2_6","volume-title":"CONCUR\u201993","author":"R.J. Glabbeek van","year":"1993","unstructured":"van Glabbeek, R.J.: The linear time \u2013 branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol.\u00a0715, pp. 66\u201381. Springer, Heidelberg (1993)"},{"key":"35_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BFb0055626","volume-title":"CONCUR \u201998 Concurrency Theory","author":"H. Hermanns","year":"1998","unstructured":"Hermanns, H., Lohrey, M.: Priority and maximal progress are completely axiomatisable. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 237\u2013252. Springer, Heidelberg (1998)"},{"key":"35_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D. Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol.\u00a0104, pp. 167\u2013183. Springer, Heidelberg (1981)"},{"key":"35_CR24","doi-asserted-by":"crossref","unstructured":"Dovier, A., Gentilini, R., Piazza, C., Policriti, A.: Rank-based symbolic bisimulation (and model checking). ENTCS 67 (2002)","DOI":"10.1016\/S1571-0661(04)80547-4"},{"key":"35_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/3-540-63166-6_13","volume-title":"Computer Aided Verification","author":"N. Klarlund","year":"1997","unstructured":"Klarlund, N.: An nlogn algorithm for online BDD refinement. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 107\u2013118. Springer, Heidelberg (1997)"},{"key":"35_CR26","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package Release 2.4.1. University of Colorado at Boulder (2005)"},{"key":"35_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1007\/BFb0032063","volume-title":"Automata, Languages and Programming","author":"J.F. Groote","year":"1990","unstructured":"Groote, J.F., Vaandrager, F.W.: An Efficient Algorithm for Branching Bisimulation and Stuttering Equivalence. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol.\u00a0443, pp. 626\u2013638. Springer, Heidelberg (1990)"},{"issue":"8","key":"35_CR28","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans.\u00a0on Comp.\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Trans.\u00a0on Comp."},{"key":"35_CR29","series-title":"SIAM Monographs on Discrete Mathematics and Applications","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898719789","volume-title":"Branching programs and binary decision diagrams","author":"I. Wegener","year":"2000","unstructured":"Wegener, I.: Branching programs and binary decision diagrams. SIAM Monographs on Discrete Mathematics and Applications. SIAM, Philadelphia (2000)"},{"key":"35_CR30","unstructured":"Strampp, K.: Symbolische Berechnung von Bisimulationen. Diploma thesis, Albert-Ludwigs-University Freiburg, Germany (2006)"},{"key":"35_CR31","first-page":"260","volume-title":"Proc.\u00a0of DAC","author":"Y. Matsunaga","year":"1993","unstructured":"Matsunaga, Y., McGeer, P.C., Brayton, R.K.: On computing the transitive closure of a state transition relation. In: Proc.\u00a0of DAC, pp. 260\u2013265. ACM Press, New York (1993)"},{"key":"35_CR32","first-page":"46","volume-title":"Proc.\u00a0of DAC","author":"J.R. Burch","year":"1990","unstructured":"Burch, J.R., et al.: Sequential circuit verification using symbolic model checking. In: Proc.\u00a0of DAC, pp. 46\u201351. ACM Press, New York (1990)"},{"key":"35_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45614-7_23","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"H. Garavel","year":"2002","unstructured":"Garavel, H., Hermanns, H.: On Combining Functional Verification and Performance Evaluation using CADP. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, Springer, Heidelberg (2002)"},{"key":"35_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/3-540-61474-5_97","volume-title":"Computer Aided Verification","author":"J.C. Fernandez","year":"1996","unstructured":"Fernandez, J.C., et al.: CADP: A Protocol Validation and Verification Toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 437\u2013440. Springer, Heidelberg (1996)"},{"key":"35_CR35","unstructured":"Herbstritt, M., Wimmer, R., Peikenkamp, T., B\u00f6de, E., Adelaide, M., Johr, S., Hermanns, H., Becker, B.: Analysis of Large Safety-Critical Systems: A quantitative Approach. Reports of SFB\/TR 14 AVACS\u00a08 (2006) ISSN 1860-9821"},{"key":"35_CR36","unstructured":"Ciardo, G., Tilgner, M.: On the use of Kronecker operators for the solution of generalized stochastic Petri nets. Technical Report 96-35, ICASE (1996)"},{"key":"35_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-540-30233-9_22","volume-title":"Applying Formal Methods: Testing, Performance, and M\/E-Commerce","author":"M. Kuntz","year":"2004","unstructured":"Kuntz, M., Siegle, M., Werner, E.: Symbolic Performance and Dependability Evaluation with the Tool CASPA. In: N\u00fa\u00f1ez, M., Maamar, Z., Pelayo, F.L., Pousttchi, K., Rubio, F. (eds.) FORTE 2004. LNCS, vol.\u00a03236, pp. 293\u2013307. Springer, Heidelberg (2004)"},{"key":"35_CR38","volume-title":"Modelling Reactive Systems with Statecharts: The Statemate Approach","author":"D. Harel","year":"1998","unstructured":"Harel, D., Politi, M.: Modelling Reactive Systems with Statecharts: The Statemate Approach. McGraw-Hill, New York (1998)"},{"key":"35_CR39","unstructured":"ERTMS: Project (May 16, 2006), Website http:\/\/ertms.uic.asso.fr\/etcs.html"},{"key":"35_CR40","unstructured":"ARP\u00a04761: Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment. Aerospace Recommended Practice, Society of Automotive Engineers, Detroit, USA (1996)"},{"key":"35_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45804-2","volume-title":"Interactive Markov Chains","author":"H. Hermanns","year":"2002","unstructured":"Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. In: Hermanns, H. (ed.) Interactive Markov Chains. LNCS, vol.\u00a02428, Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901914_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,2]],"date-time":"2021-08-02T00:18:21Z","timestamp":1627863501000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901914_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540472377","9783540472384"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/11901914_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}