TY - GEN

T1 - A Truly Symbolic Linear-Time Algorithm for SCC Decomposition

AU - Larsen, Casper Abild

AU - Schmidt, Simon Meldahl

AU - Steensgaard, Jesper

AU - Jakobsen, Anna Blume

AU - Pol, Jaco van de

AU - Pavlogiannis, Andreas

PY - 2023/4

Y1 - 2023/4

N2 - Decomposing a directed graph to its strongly connected components (SCCs) is a fundamental task in model checking. To deal with the state-space explosion problem, graphs are often represented symbolically using binary decision diagrams (BDDs), which have exponential compression capabilities. The theoretically-best symbolic algorithm for SCC decomposition is Gentilini et al’s SKELETON algorithm, that uses O(n) symbolic steps on a graph of n nodes. However, SKELETON uses Θ(n) symbolic objects, as opposed to (poly-)logarithmically many, which is the norm for symbolic algorithms, thereby relinquishing its symbolic nature. Here we present CHAIN, a new symbolic algorithm for SCC decomposition that also makes O(n) symbolic steps, but further uses logarithmic space, and is thus truly symbolic. We then extend CHAIN to COLOREDCHAIN, an algorithm for SCC decomposition on edge-colored graphs, which arise naturally in model-checking a family of systems. Finally, we perform an experimental evaluation of CHAIN among other standard symbolic SCC algorithms in the literature. The results show that CHAIN is competitive on almost all benchmarks, and often faster, while it clearly outperforms all other algorithms on challenging inputs.

AB - Decomposing a directed graph to its strongly connected components (SCCs) is a fundamental task in model checking. To deal with the state-space explosion problem, graphs are often represented symbolically using binary decision diagrams (BDDs), which have exponential compression capabilities. The theoretically-best symbolic algorithm for SCC decomposition is Gentilini et al’s SKELETON algorithm, that uses O(n) symbolic steps on a graph of n nodes. However, SKELETON uses Θ(n) symbolic objects, as opposed to (poly-)logarithmically many, which is the norm for symbolic algorithms, thereby relinquishing its symbolic nature. Here we present CHAIN, a new symbolic algorithm for SCC decomposition that also makes O(n) symbolic steps, but further uses logarithmic space, and is thus truly symbolic. We then extend CHAIN to COLOREDCHAIN, an algorithm for SCC decomposition on edge-colored graphs, which arise naturally in model-checking a family of systems. Finally, we perform an experimental evaluation of CHAIN among other standard symbolic SCC algorithms in the literature. The results show that CHAIN is competitive on almost all benchmarks, and often faster, while it clearly outperforms all other algorithms on challenging inputs.

KW - Binary decision diagrams

KW - Strongly connected components

KW - Colored graphs

UR - http://www.scopus.com/inward/record.url?scp=85161425068&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-30820-8_22

DO - 10.1007/978-3-031-30820-8_22

M3 - Article in proceedings

SN - 978-3-031-30819-2

T3 - Lecture Notes in Computer Science

SP - 353

EP - 371

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Sankaranarayanan, Sriram

A2 - Sharygina, Natasha

PB - Springer

CY - Cham

ER -