{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T12:56:47Z","timestamp":1760101007527},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,8,2]],"date-time":"2017-08-02T00:00:00Z","timestamp":1501632000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Johannes Kepler University Linz"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2018,4]]},"DOI":"10.1007\/s10009-017-0468-z","type":"journal-article","created":{"date-parts":[[2017,8,2]],"date-time":"2017-08-02T07:46:37Z","timestamp":1501659997000},"page":"157-177","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Multi-core symbolic bisimulation minimisation"],"prefix":"10.1007","volume":"20","author":[{"given":"Tom","family":"van Dijk","sequence":"first","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,2]]},"reference":[{"issue":"3","key":"468_CR1","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/s00165-005-0070-0","volume":"17","author":"B Badban","year":"2005","unstructured":"Badban, B., Fokkink, W., Groote, J.F., Pang, J., van de Pol, J.: Verification of a sliding window protocol in $$\\mu $$ \u03bc CRL and PVS. Formal Asp. Comput. 17(3), 342\u2013388 (2005)","journal-title":"Formal Asp. Comput."},{"key":"468_CR2","first-page":"188","volume":"1993","author":"RI Bahar","year":"1993","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. ICCAD 1993, 188\u2013191 (1993)","journal-title":"ICCAD"},{"key":"468_CR3","first-page":"57","volume-title":"TCS\u201908, IFIP","author":"R Bakhshi","year":"2008","unstructured":"Bakhshi, R., Fokkink, W., Pang, J., van de Pol, J.: Leader election in anonymous rings: Franklin goes probabilistic. In: Ausiello, G., Karhum\u00e4ki, J., Mauri, G., Ong, C.L. (eds.) TCS\u201908, IFIP, vol. 273, pp. 57\u201372. Springer, Berlin (2008)"},{"issue":"2","key":"468_CR4","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":"468_CR5","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":"468_CR6","doi-asserted-by":"crossref","unstructured":"Blom, S., van\u00a0de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: CAV, LNCS, vol. 6174, pp. 354\u2013359. Springer (2010)","DOI":"10.1007\/978-3-642-14295-6_31"},{"key":"468_CR7","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":"468_CR8","doi-asserted-by":"crossref","unstructured":"Bouali, A., de\u00a0Simone, R.: Symbolic bisimulation minimisation. In: Computer Aided Verification, 4th International Workshop, LNCS, vol. 663, pp. 96\u2013108. Springer (1992)","DOI":"10.1007\/3-540-56496-9_9"},{"key":"468_CR9","doi-asserted-by":"crossref","unstructured":"Brace, K.S., Rudell, R.L., Bryant, R.E.: Efficient implementation of a BDD package. In: DAC, pp. 40\u201345 (1990)","DOI":"10.1145\/123186.123222"},{"issue":"8","key":"468_CR10","doi-asserted-by":"crossref","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":"468_CR11","doi-asserted-by":"crossref","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. Circuits Syst. 13(4), 401\u2013424 (1994)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"468_CR12","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"},{"key":"468_CR13","doi-asserted-by":"crossref","unstructured":"Cranen, S., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., de\u00a0Vink, E.P., Wesselink, W., Willemse, T.A.C.: An overview of the mCRL2 toolset and its recent advances. In: TACAS, LNCS, vol. 7795, pp. 199\u2013213. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_15"},{"issue":"2","key":"468_CR14","doi-asserted-by":"crossref","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":"468_CR15","first-page":"139","volume":"2007","author":"S Derisavi","year":"2007","unstructured":"Derisavi, S.: A symbolic algorithm for optimal Markov chain lumping. TACAS 2007, 139\u2013154 (2007)","journal-title":"TACAS"},{"key":"468_CR16","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":"468_CR17","doi-asserted-by":"crossref","unstructured":"van Dijk, T.: Sylvan: multi-core decision diagrams. Ph.D. thesis, University of Twente (2016)","DOI":"10.1007\/s10009-016-0433-2"},{"key":"468_CR18","first-page":"127","volume":"296","author":"T Dijk van","year":"2013","unstructured":"van Dijk, T., Laarman, A., van de Pol, J.: Multi-core BDD operations for symbolic reachability. ENTCS 296, 127\u2013143 (2013)","journal-title":"ENTCS"},{"key":"468_CR19","doi-asserted-by":"crossref","unstructured":"van Dijk, T., van\u00a0de Pol, J.: Lace: non-blocking split deque for work-stealing. In: MuCoCoS, LNCS, vol. 8806, pp. 206\u2013217. Springer (2014)","DOI":"10.1007\/978-3-319-14313-2_18"},{"key":"468_CR20","doi-asserted-by":"crossref","unstructured":"van Dijk, T., van\u00a0de Pol, J.: Sylvan: multi-core decision diagrams. In: TACAS, LNCS, vol. 9035, pp. 677\u2013691. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_60"},{"key":"468_CR21","doi-asserted-by":"crossref","unstructured":"van Dijk, T., van\u00a0de Pol, J.: Multi-core symbolic bisimulation minimisation. In: TACAS, LNCS, vol. 9636, pp. 332\u2013348. Springer (2016)","DOI":"10.1007\/978-3-662-49674-9_19"},{"issue":"3","key":"468_CR22","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/0196-6774(82)90023-2","volume":"3","author":"D Dolev","year":"1982","unstructured":"Dolev, D., Klawe, M.M., Rodeh, M.: An $$o(n \\log n)$$ o ( n log n ) unidirectional distributed algorithm for extrema finding in a circle. J. Algorithms 3(3), 245\u2013260 (1982)","journal-title":"J. Algorithms"},{"issue":"5","key":"468_CR23","doi-asserted-by":"crossref","first-page":"336","DOI":"10.1145\/358506.358517","volume":"25","author":"WR Franklin","year":"1982","unstructured":"Franklin, W.R.: On an improved algorithm for decentralized extrema finding in circular configurations of processors. Commun. ACM 25(5), 336\u2013337 (1982)","journal-title":"Commun. ACM"},{"key":"468_CR24","first-page":"536","volume-title":"AMAST\u201996, LNCS 1101","author":"JF Groote","year":"1996","unstructured":"Groote, J.F., van de Pol, J.: A bounded retransmission protocol for large data packets. In: Wirsing, M., Nivat, M. (eds.) AMAST\u201996, LNCS 1101, pp. 536\u2013550. Springer, Berlin (1996)"},{"key":"468_CR25","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45804-2","volume-title":"Interactive Markov Chains: The Quest for Quantified Quality, Lecture Notes in Computer Science","author":"H Hermanns","year":"2002","unstructured":"Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality, Lecture Notes in Computer Science, vol. 2428. Springer, Berlin (2002)"},{"key":"468_CR26","doi-asserted-by":"crossref","unstructured":"Hermanns, H., Katoen, J.: The how and why of interactive Markov chains. In: FMCO\u201909, LNCS 6286, pp. 311\u2013337. Springer (2009)","DOI":"10.1007\/978-3-642-17071-3_16"},{"issue":"4","key":"468_CR27","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/S0020-0190(98)00158-6","volume":"68","author":"WH Hesselink","year":"1998","unstructured":"Hesselink, W.H.: Invariants for the construction of a handshake register. Inf. Process. Lett. 68(4), 173\u2013177 (1998)","journal-title":"Inf. Process. Lett."},{"key":"468_CR28","doi-asserted-by":"crossref","unstructured":"Kant, G., Laarman, A., Meijer, J., van\u00a0de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: TACAS 2015, LNCS, vol. 9035, pp. 692\u2013707. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_61"},{"key":"468_CR29","unstructured":"Kulakowski, K.: Concurrent bisimulation algorithm. CoRR. arXiv:1311.7635 (2013)"},{"key":"468_CR30","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: CAV, LNCS, vol. 6806, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"468_CR31","first-page":"204","volume-title":"HVC, LNCS","author":"J Meijer","year":"2014","unstructured":"Meijer, J., Kant, G., Blom, S., van de Pol, J.: Read, write and copy dependencies for symbolic model checking. In: Yahav, E. (ed.) HVC, LNCS, vol. 8855, pp. 204\u2013219. Springer, Berlin (2014)"},{"issue":"2","key":"468_CR32","doi-asserted-by":"crossref","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":"468_CR33","doi-asserted-by":"crossref","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."},{"key":"468_CR34","first-page":"54","volume-title":"ATVA\u201909, LNCS","author":"J Pol van de","year":"2009","unstructured":"van de Pol, J., Timmer, M.: State space reduction of linear processes using control flow reconstruction. In: Liu, Z., Ravn, A.P. (eds.) ATVA\u201909, LNCS, vol. 5799, pp. 54\u201368. Springer, Berlin (2009)"},{"issue":"6","key":"468_CR35","doi-asserted-by":"crossref","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":"468_CR36","doi-asserted-by":"crossref","unstructured":"Remenska, D., Willemse, T.A.C., Verstoep, K., Fokkink, W., Templon, J., Bal, H.E.: Using model checking to analyze the system behavior of the LHC production grid. In: CCGrid\u201912, pp. 335\u2013343. IEEE Computer Society (2012)","DOI":"10.1109\/CCGrid.2012.90"},{"key":"468_CR37","first-page":"368","volume":"2015","author":"A Wijs","year":"2015","unstructured":"Wijs, A.: GPU accelerated strong and branching bisimilarity checking. TACAS 2015, 368\u2013383 (2015)","journal-title":"TACAS"},{"key":"468_CR38","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Becker, B.: Correctness issues of symbolic bisimulation computation for Markov chains. In: MMB&DFT, LNCS, vol. 5987, pp. 287\u2013301. Springer (2010)","DOI":"10.1007\/978-3-642-12104-3_22"},{"issue":"9","key":"468_CR39","doi-asserted-by":"crossref","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":"468_CR40","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":"468_CR41","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B.: Sigref\u2014a symbolic bisimulation tool box. In: ATVA, LNCS, vol. 4218, pp. 477\u2013492. Springer (2006)","DOI":"10.1007\/11901914_35"},{"key":"468_CR42","unstructured":"Wimmer, R., Hermanns, H., Herbstritt, M., Becker, B.: Towards symbolic stochastic aggregation. Technical Report, SFB\/TR 14 AVACS (2007)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-017-0468-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0468-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0468-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T19:33:47Z","timestamp":1569958427000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-017-0468-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,2]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,4]]}},"alternative-id":["468"],"URL":"https:\/\/doi.org\/10.1007\/s10009-017-0468-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,8,2]]}}}