TY - GEN
T1 - Fast Symbolic Computation of Bottom SCCs
AU - Jakobsen, Anna Blume
AU - Jørgensen, Rasmus Skibdahl Melanchton
AU - van de Pol, Jaco
AU - Pavlogiannis, Andreas
N1 - Publisher Copyright:
© The Author(s) 2024.
PY - 2024
Y1 - 2024
N2 - 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. In this paper we introduce PENDANT, a new symbolic algorithm for computing BSCCs which runs in linear symbolic time. In contrast to the standard approach of escaping non-bottom SCCs, PENDANT aims to start 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 deadlock-detection 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: PENDANT is decisively faster than the standard existing algorithm for BSCC computation, while deadlock detection improves the performance of each algorithm significantly.
AB - 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. In this paper we introduce PENDANT, a new symbolic algorithm for computing BSCCs which runs in linear symbolic time. In contrast to the standard approach of escaping non-bottom SCCs, PENDANT aims to start 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 deadlock-detection 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: PENDANT is decisively faster than the standard existing algorithm for BSCC computation, while deadlock detection improves the performance of each algorithm significantly.
KW - BDDs
KW - strongly connected components
KW - symbolic algorithms
UR - http://www.scopus.com/inward/record.url?scp=85192224735&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-57256-2_6
DO - 10.1007/978-3-031-57256-2_6
M3 - Article in proceedings
AN - SCOPUS:85192224735
SN - 9783031572555
T3 - Lecture Notes in Computer Science
SP - 110
EP - 128
BT - Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024
A2 - Finkbeiner, Bernd
A2 - Kovács, Laura
PB - Springer
CY - Cham
T2 - 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024
Y2 - 6 April 2024 through 11 April 2024
ER -