{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T08:40:02Z","timestamp":1748853602469,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662496732"},{"type":"electronic","value":"9783662496749"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_19","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"332-348","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Multi-core Symbolic Bisimulation Minimisation"],"prefix":"10.1007","author":[{"given":"Tom","family":"van Dijk","sequence":"first","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Bahar, R.I., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. In: Lightner, M.R., Jess, J.A.G. (eds.) ICCAD, pp. 188\u2013191. IEEE Computer Society \/ ACM (1993)","DOI":"10.1109\/ICCAD.1993.580054"},{"issue":"2","key":"19_CR2","first-page":"35","volume":"220","author":"S Blom","year":"2008","unstructured":"Blom, S., Haverkort, B.R., Kuntz, M., van de Pol, J.: Distributed markovian bisimulation reduction aimed at CSL model checking. ENTCS 220(2), 35\u201350 (2008)","journal-title":"ENTCS"},{"issue":"1","key":"19_CR3","first-page":"99","volume":"89","author":"S Blom","year":"2003","unstructured":"Blom, S., Orzan, S.: Distributed branching bisimulation reduction of state spaces. ENTCS 89(1), 99\u2013113 (2003)","journal-title":"ENTCS"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Blumofe, R.D.: Scheduling multithreaded computations by work stealing. In: FOCS, pp. 356\u2013368. IEEE Computer Society (1994)","DOI":"10.1109\/SFCS.1994.365680"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-56496-9_9","volume-title":"Computer Aided Verification","author":"A Bouali","year":"1992","unstructured":"Bouali, A., de Simone, R.: Symbolic bisimulation minimisation. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 96\u2013108. Springer, Heidelberg (1992)"},{"issue":"8","key":"19_CR6","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C\u201335","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C\u201335(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"4","key":"19_CR7","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J Burch","year":"1994","unstructured":"Burch, J., Clarke, E., Long, D., McMillan, K., Dill, D.: Symbolic model checking for sequential circuit verification. IEEE Trans. Comput. Aided Des. Integr. Circ. Syst. 13(4), 401\u2013424 (1994)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circ. Syst."},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., McMillan, K.L., Zhao, X., Fujita, M., Yang, J.: Spectral transforms for large boolean functions with applications to technology mapping. In: DAC, pp. 54\u201360 (1993)","DOI":"10.1145\/157485.164569"},{"issue":"2","key":"19_CR9","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R Nicola De","year":"1995","unstructured":"De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458\u2013487 (1995)","journal-title":"J. ACM"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-540-71209-1_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Derisavi","year":"2007","unstructured":"Derisavi, S.: A symbolic algorithm for optimal markov chain lumping. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 139\u2013154. Springer, Heidelberg (2007)"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Derisavi, S.: Signature-based symbolic algorithm for optimal markov chain lumping. In: QEST 2007, pp. 141\u2013150. IEEE Computer Society (2007)","DOI":"10.1109\/QEST.2007.27"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"van Dijk, T., Laarman, A.W., van de Pol, J.C.: Multi-Core BDD operations for symbolic reachability. In: 11th International Workshop on Parallel and Distributed Methods in verifiCation. ENTCS. Elsevier (2012)","DOI":"10.1016\/j.entcs.2013.07.009"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1007\/978-3-319-14313-2_18","volume-title":"Euro-Par 2014: Parallel Processing Workshops","author":"T Dijk van","year":"2014","unstructured":"van Dijk, T., van de Pol, J.C.: Lace: non-blocking split deque for work-stealing. In: Lopes, L., et al. (eds.) Euro-Par 2014, Part II. LNCS, vol. 8806, pp. 206\u2013217. Springer, Heidelberg (2014)"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1007\/978-3-662-46681-0_60","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Dijk van","year":"2015","unstructured":"van Dijk, T., van\u00a0de Pol, J.C.: Sylvan: multi-core decision diagrams. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 9035, pp. 677\u2013691. Springer, Heidelberg (2015)"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-642-17071-3_16","volume-title":"Formal Methods for Components and Objects","author":"H Hermanns","year":"2010","unstructured":"Hermanns, H., Katoen, J.-P.: The how and why of interactive markov chains. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 311\u2013337. Springer, Heidelberg (2010)"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J.C., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015)"},{"key":"19_CR17","unstructured":"Kulakowski, K.: Concurrent bisimulation algorithm. CoRR abs\/1311.7635 (2013)"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"issue":"2","key":"19_CR19","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1142\/S012905411340011X","volume":"24","author":"M Mumme","year":"2013","unstructured":"Mumme, M., Ciardo, G.: An efficient fully symbolic bisimulation algorithm for non-deterministic systems. Int. J. Found. Comput. Sci. 24(2), 263\u2013282 (2013)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"6","key":"19_CR20","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 J. Comput. 16(6), 973\u2013989 (1987)","journal-title":"SIAM J. Comput."},{"issue":"6","key":"19_CR21","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1145\/78973.78977","volume":"33","author":"W Pugh","year":"1990","unstructured":"Pugh, W.: Skip lists: a probabilistic alternative to balanced trees. Commun. ACM 33(6), 668\u2013676 (1990)","journal-title":"Commun. ACM"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1007\/978-3-662-46681-0_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Wijs","year":"2015","unstructured":"Wijs, A.: GPU accelerated strong and branching bisimilarity checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 368\u2013383. Springer, Heidelberg (2015)"},{"key":"19_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-12104-3_22","volume-title":"Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance","author":"R Wimmer","year":"2010","unstructured":"Wimmer, R., Becker, B.: Correctness issues of symbolic bisimulation computation for markov chains. In: M\u00fcller-Clostermann, B., Echtle, K., Rathgeb, E.P. (eds.) MMB & DFT 2010. LNCS, vol. 5987, pp. 287\u2013301. Springer, Heidelberg (2010)"},{"issue":"9","key":"19_CR24","doi-asserted-by":"publisher","first-page":"816","DOI":"10.1016\/j.peva.2009.12.008","volume":"67","author":"R Wimmer","year":"2010","unstructured":"Wimmer, R., Derisavi, S., Hermanns, H.: Symbolic partition refinement with automatic balancing of time and space. Perform. Eval. 67(9), 816\u2013836 (2010)","journal-title":"Perform. Eval."},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Herbstritt, M., Becker, B.: Optimization techniques for BDD-based bisimulation computation. In: 17th GLSVLSI, pp. 405\u2013410. ACM (2007)","DOI":"10.1145\/1228784.1228880"},{"key":"19_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/11901914_35","volume-title":"Automated Technology for Verification and Analysis","author":"R Wimmer","year":"2006","unstructured":"Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B.: SIGREF \u2013 a symbolic bisimulation tool box. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 477\u2013492. Springer, Heidelberg (2006)"},{"key":"19_CR27","unstructured":"Wimmer, R., Hermanns, H., Herbstritt, M., Becker, B.: Towards Symbolic Stochastic Aggregation. Technical report, SFB\/TR 14 AVACS (2007)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T08:27:23Z","timestamp":1748852843000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}