{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T09:14:28Z","timestamp":1743066868911,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572555"},{"type":"electronic","value":"9783031572562"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The computation of bottom strongly connected components (BSCCs) is a fundamental task in model checking, as well as in characterizing the attractors of dynamical systems. As such, symbolic algorithms for BSCCs have received special attention, and are based on the idea that the computation of an SCC can be stopped early, as soon as it is deemed to be non-bottom.<\/jats:p><jats:p>In this paper we introduce <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsc {Pendant}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>P<\/mml:mi>\n                    <mml:mstyle>\n                      <mml:mi>E<\/mml:mi>\n                      <mml:mi>N<\/mml:mi>\n                      <mml:mi>D<\/mml:mi>\n                      <mml:mi>A<\/mml:mi>\n                      <mml:mi>N<\/mml:mi>\n                      <mml:mi>T<\/mml:mi>\n                    <\/mml:mstyle>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, a new symbolic algorithm for computing BSCCs which runs in linear symbolic time. In contrast to the standard approach of <jats:italic>escaping<\/jats:italic> non-bottom SCCs, <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsc {Pendant}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>P<\/mml:mi>\n                    <mml:mstyle>\n                      <mml:mi>E<\/mml:mi>\n                      <mml:mi>N<\/mml:mi>\n                      <mml:mi>D<\/mml:mi>\n                      <mml:mi>A<\/mml:mi>\n                      <mml:mi>N<\/mml:mi>\n                      <mml:mi>T<\/mml:mi>\n                    <\/mml:mstyle>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> aims to <jats:italic>start<\/jats:italic> the computation from nodes that are likely to belong to BSCCs, and thus is more effective in sidestepping SCCs that are non-bottom. Moreover, we employ a simple yet powerful <jats:italic>deadlock-detection<\/jats:italic> technique, that quickly identifies singleton BSCCs before the main algorithm is run. Our experimental evaluation on three diverse datasets of 553 models demonstrates the efficacy of our two methods: <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsc {Pendant}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>P<\/mml:mi>\n                    <mml:mstyle>\n                      <mml:mi>E<\/mml:mi>\n                      <mml:mi>N<\/mml:mi>\n                      <mml:mi>D<\/mml:mi>\n                      <mml:mi>A<\/mml:mi>\n                      <mml:mi>N<\/mml:mi>\n                      <mml:mi>T<\/mml:mi>\n                    <\/mml:mstyle>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> is decisively faster than the standard existing algorithm for BSCC computation, while deadlock detection improves the performance of each algorithm significantly.<\/jats:p>","DOI":"10.1007\/978-3-031-57256-2_6","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T08:03:04Z","timestamp":1712217784000},"page":"110-128","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Fast Symbolic Computation of Bottom SCCs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-7892-7230","authenticated-orcid":false,"given":"Anna Blume","family":"Jakobsen","sequence":"first","affiliation":[]},{"given":"Rasmus Skibdahl Melanchton","family":"J\u00f8rgensen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-0625","authenticated-orcid":false,"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8943-0722","authenticated-orcid":false,"given":"Andreas","family":"Pavlogiannis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"6_CR1","unstructured":"EMBL-EBI\u2019s BioModels model repository (2023), https:\/\/www.ebi.ac.uk\/biomodels\/, Last accessed on 2023-10-10"},{"key":"6_CR2","unstructured":"PyBoolNet model repository (2023), https:\/\/github.com\/hklarner\/pyboolnet\/tree\/master\/pyboolnet\/repository, Last accessed on 2023-10-10"},{"key":"6_CR3","unstructured":"SBML models repository (2023), https:\/\/github.com\/sybila\/biodivine-lib-param-bn\/tree\/master\/sbml_models, Last accessed 2023-10-10"},{"key":"6_CR4","doi-asserted-by":"publisher","unstructured":"Abraham, E., Jansen, N., Wimmer, R., Katoen, J.P., Becker, B.: DTMC model checking by SCC reduction. In: Proceedings of the 2010 Seventh International Conference on the Quantitative Evaluation of Systems. p. 37\u201346. QEST \u201910, IEEE Computer Society, USA (2010). https:\/\/doi.org\/10.1109\/QEST.2010.13","DOI":"10.1109\/QEST.2010.13"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Amparore, E.G., Donatelli, S., Gall\u00e0, F.: starMC: an automata based CTL* model checker. PeerJ Comput. Sci. 8, \u00a0e823 (2022)","DOI":"10.7717\/peerj-cs.823"},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"Benes, N., Brim, L., Pastva, S., Safr\u00e1nek, D.: Computing bottom SCCs symbolically using transition guided reduction. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification, CAV 2021, Part I. LNCS, vol. 12759, pp. 505\u2013528. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_24","DOI":"10.1007\/978-3-030-81685-8_24"},{"key":"6_CR7","doi-asserted-by":"publisher","unstructured":"Benes, N., Brim, L., Pastva, S., Safr\u00e1nek, D.: BDD-based algorithm for SCC decomposition of edge-coloured graphs. Logical Methods in Computer Science 18(1) (2022). https:\/\/doi.org\/10.46298\/lmcs-18(1:38)2022","DOI":"10.46298\/lmcs-18(1:38)2022"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in n log n symbolic steps. Formal Methods in System Design 28(1), 37\u201356 (2006)","DOI":"10.1007\/s10703-006-4341-z"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Proceedings of the 11th International Conference on Computer Aided Verification. p. 222\u2013235. CAV \u201999, Springer (1999)","DOI":"10.1007\/3-540-48683-6_21"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992)","DOI":"10.1145\/136035.136043"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Buchholz, P., Katoen, J.P., Kemper, P., Tepper, C.: Model-checking large structured Markov chains. The Journal of Logic and Algebraic Programming 56(1), 69\u201397 (2003). https:\/\/doi.org\/10.1016\/S1567-8326(02)00067-X, probabilistic Techniques for the Design and Analysis of Systems","DOI":"10.1016\/S1567-8326(02)00067-X"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Dvo\u0159\u00e1k, W., Henzinger, M., Loitzenbauer, V.: Lower bounds for symbolic computation on graphs: Strongly connected components, liveness, safety, and diameter. In: Proc. 29th ACM-SIAM Symp. on Discrete Algorithms. p. 2341\u20132356. SODA \u201918, Soc. for Industrial and Applied Mathematics, USA (2018)","DOI":"10.1137\/1.9781611975031.151"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, M.: Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In: Proc. 22nd ACM-SIAM Symp. on Discrete Algorithms. p. 1318\u20131336. SODA \u201911, Society for Industrial and Applied Mathematics, USA (2011)","DOI":"10.1137\/1.9781611973082.101"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: CAV. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"van Dijk, T., van\u00a0de Pol, J.: Sylvan: multi-core framework for decision diagrams. Int. Journal on Software Tools for Technology Transfer 19(6), 675\u2013696 (2017)","DOI":"10.1007\/s10009-016-0433-2"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Fisler, K., Fraer, R., Kamhi, G., Vardi, M.Y., Yang, Z.: Is there a best symbolic cycle-detection algorithm? In: Proc. 7th IC on Tools and Algorithms for the Construction and Analysis of Systems. p. 420\u2013434. TACAS 2001, Springer (2001)","DOI":"10.1007\/3-540-45319-9_29"},{"key":"6_CR17","unstructured":"Gentilini, R., Piazza, C., Policriti, A.: Computing strongly connected components in a linear number of symbolic steps. In: Proceedings of the Fourteenth Annual ACM-SIAM Symposium on Discrete Algorithms. p. 573\u2013582. SODA \u201903, Society for Industrial and Applied Mathematics, USA (2003)"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Hardin, R.H., Kurshan, R.P., Shukla, S.K., Vardi, M.Y.: A new heuristic for bad cycle detection using BDDs. Form. Methods Syst. Des. 18(2), 131\u2013140 (mar 2001). https:\/\/doi.org\/10.1023\/A:1008727508722","DOI":"10.1023\/A:1008727508722"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and reasoning about systems. Cambridge university press (2004)","DOI":"10.1017\/CBO9780511810275"},{"key":"6_CR20","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. Lecture Notes in Computer Science, vol.\u00a09035, pp. 692\u2013707. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_61"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A., Raviv, L., Shahar, E.: Model checking with strong fairness. Formal Methods Syst. Des. 28(1), 57\u201384 (2006)","DOI":"10.1007\/s10703-006-4342-y"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Kordon, F., Garavel, H., Hillah, L., Paviot-Adet, E., Jezequel, L., Hulin-Hubard, F., Amparore, E.G., Beccuti, M., Berthomieu, B., Evrard, H., Jensen, P.G., Botlan, D.L., Liebke, T., Meijer, J., Srba, J., Thierry-Mieg, Y., van\u00a0de Pol, J., Wolf, K.: MCC\u20192017 - the seventh model checking contest. Trans. Petri Nets Other Model. Concurr. 13, 181\u2013209 (2018)","DOI":"10.1007\/978-3-662-58381-4_9"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Ku\u010dera, A., Stra\u017eovsk\u00fd, O.: On the controller synthesis for finite-state Markov decision processes. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. pp. 541\u2013552. Springer Berlin Heidelberg, Berlin, Heidelberg (2005)","DOI":"10.1007\/11590156_44"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: CAV. Lecture Notes in Computer Science, vol.\u00a06806, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Larsen, C.A., Schmidt, S.M., Steensgaard, J., Jakobsen, A.B., van de Pol, J., Pavlogiannis, A.: A truly symbolic linear-time algorithm for SCC decomposition (2023)","DOI":"10.1007\/978-3-031-30820-8_22"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf. 19(1), 9\u201330 (2017)","DOI":"10.1007\/s10009-015-0378-x"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Pel\u00e1nek, R.: BEEM: benchmarks for explicit model checkers. In: SPIN. Lecture Notes in Computer Science, vol.\u00a04595, pp. 263\u2013267. Springer (2007)","DOI":"10.1007\/978-3-540-73370-6_17"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Strength-Based Decomposition of the Property B\u00fcchi Automaton for Faster Model Checking. In: Piterman, N., Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 580\u2013593. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_42","DOI":"10.1007\/978-3-642-36742-7_42"},{"key":"6_CR29","doi-asserted-by":"publisher","unstructured":"Saadatpour, A., Albert, I., Albert, R.: Attractor analysis of asynchronous boolean models of signal transduction networks. Journal of Theoretical Biology 266(4), 641\u2013656 (2010). https:\/\/doi.org\/10.1016\/j.jtbi.2010.07.022","DOI":"10.1016\/j.jtbi.2010.07.022"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: TACAS. Lecture Notes in Computer Science, vol.\u00a03440, pp. 174\u2013190. Springer (2005)","DOI":"10.1007\/978-3-540-31980-1_12"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Wang, C., Bloem, R., Hachtel, G.D., Ravi, K., Somenzi, F.: Divide and compose: SCC refinement for language emptiness. In: Proceedings of the 12th International Conference on Concurrency Theory. p. 456\u2013471. CONCUR \u201901, Springer-Verlag, Berlin, Heidelberg (2001)","DOI":"10.1007\/3-540-44685-0_31"},{"key":"6_CR32","doi-asserted-by":"crossref","unstructured":"Xie, A., Beerel, P.A.: Implicit enumeration of strongly connected components and an application to formal verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 19(10), 1225\u20131230 (2000)","DOI":"10.1109\/43.875347"},{"key":"6_CR33","doi-asserted-by":"publisher","unstructured":"Yuan, Q., Mizera, A., Pang, J., Qu, H.: A new decomposition-based method for detecting attractors in synchronous boolean networks. Science of Computer Programming 180, 18\u201335 (2019). https:\/\/doi.org\/10.1016\/j.scico.2019.05.001","DOI":"10.1016\/j.scico.2019.05.001"},{"key":"6_CR34","doi-asserted-by":"crossref","unstructured":"Zhao, Y., Ciardo, G.: Symbolic computation of strongly connected components and fair cycles using saturation. Innov. Syst. Softw. Eng. 7(2), 141\u2013150 (2011)","DOI":"10.1007\/s11334-011-0146-3"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57256-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T08:06:57Z","timestamp":1712218017000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57256-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572555","9783031572562"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57256-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}