A Truly Symbolic Linear-Time Algorithm for SCC Decomposition

Casper Abild Larsen; Simon Meldahl Schmidt; Jesper Steensgaard; Anna Blume Jakobsen; Jaco van de Pol; Andreas Pavlogiannis

doi:10.1007/978-3-031-30820-8_22

A Truly Symbolic Linear-Time Algorithm for SCC Decomposition

Casper Abild Larsen, Simon Meldahl Schmidt, Jesper Steensgaard, Anna Blume Jakobsen, Jaco van de Pol, Andreas Pavlogiannis

Institut for Datalogi

Publikation: Bidrag til bog/antologi/rapport/proceeding › Konferencebidrag i proceedings › Forskning › peer review

Abstract

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.

Originalsprog	Engelsk
Titel	Tools and Algorithms for the Construction and Analysis of Systems : 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part II
Redaktører	Sriram Sankaranarayanan, Natasha Sharygina
Antal sider	19
Udgivelsessted	Cham
Forlag	Springer
Publikationsdato	apr. 2023
Sider	353-371
ISBN (Trykt)	978-3-031-30819-2
ISBN (Elektronisk)	978-3-031-30820-8
DOI	https://doi.org/10.1007/978-3-031-30820-8_22
Status	Udgivet - apr. 2023

Navn	Lecture Notes in Computer Science
Vol/bind	13994
ISSN	0302-9743

Adgang til dokumentet

10.1007/978-3-031-30820-8_22Licens: CC BY

Andre filer og links

Link to publication in Scopus

Citationsformater

Larsen, C. A., Schmidt, S. M., Steensgaard, J., Jakobsen, A. B., Pol, J. V. D., & Pavlogiannis, A. (2023). A Truly Symbolic Linear-Time Algorithm for SCC Decomposition. I S. Sankaranarayanan, & N. Sharygina (red.), Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part II (s. 353-371). Springer. https://doi.org/10.1007/978-3-031-30820-8_22

Larsen, Casper Abild ; Schmidt, Simon Meldahl ; Steensgaard, Jesper et al. / A Truly Symbolic Linear-Time Algorithm for SCC Decomposition. Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part II. red. / Sriram Sankaranarayanan ; Natasha Sharygina. Cham : Springer, 2023. s. 353-371 (Lecture Notes in Computer Science, Bind 13994).

@inproceedings{9cf24d7fc4634618956d0bc2d2e0bd66,

title = "A Truly Symbolic Linear-Time Algorithm for SCC Decomposition",

abstract = "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{\textquoteright}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.",

keywords = "Binary decision diagrams, Strongly connected components, Colored graphs",

author = "Larsen, {Casper Abild} and Schmidt, {Simon Meldahl} and Jesper Steensgaard and Jakobsen, {Anna Blume} and Pol, {Jaco van de} and Andreas Pavlogiannis",

year = "2023",

month = apr,

doi = "10.1007/978-3-031-30820-8_22",

language = "English",

isbn = "978-3-031-30819-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "353--371",

editor = "Sriram Sankaranarayanan and Natasha Sharygina",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "Netherlands",

}

Larsen, CA, Schmidt, SM, Steensgaard, J, Jakobsen, AB, Pol, JVD & Pavlogiannis, A 2023, A Truly Symbolic Linear-Time Algorithm for SCC Decomposition. i S Sankaranarayanan & N Sharygina (red), Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part II. Springer, Cham, Lecture Notes in Computer Science, bind 13994, s. 353-371. https://doi.org/10.1007/978-3-031-30820-8_22

A Truly Symbolic Linear-Time Algorithm for SCC Decomposition. / Larsen, Casper Abild; Schmidt, Simon Meldahl; Steensgaard, Jesper et al.
Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part II. red. / Sriram Sankaranarayanan; Natasha Sharygina. Cham: Springer, 2023. s. 353-371 (Lecture Notes in Computer Science, Bind 13994).

Publikation: Bidrag til bog/antologi/rapport/proceeding › Konferencebidrag i proceedings › Forskning › peer review

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 -

Larsen CA, Schmidt SM, Steensgaard J, Jakobsen AB, Pol JVD , Pavlogiannis A. A Truly Symbolic Linear-Time Algorithm for SCC Decomposition. I Sankaranarayanan S, Sharygina N, red., Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part II. Cham: Springer. 2023. s. 353-371. (Lecture Notes in Computer Science, Bind 13994). doi: 10.1007/978-3-031-30820-8_22

A Truly Symbolic Linear-Time Algorithm for SCC Decomposition

Abstract

Adgang til dokumentet

Andre filer og links

Fingeraftryk

Citationsformater