BDD-Based Algorithm for SCC Decomposition of Edge-Coloured
Graphs

J 2022

BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA a David ŠAFRÁNEK

Základní údaje

Originální název

BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs

Autoři

BENEŠ, Nikola (203 Česká republika, domácí), Luboš BRIM (203 Česká republika, domácí), Samuel PASTVA (703 Slovensko, domácí) a David ŠAFRÁNEK (203 Česká republika, garant, domácí)

Vydání

Logical Methods in Computer Science, Episciences, 2022, 1860-5974

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Odkazy

URL

Impakt faktor

Impact factor: 0.600

Kód RIV

RIV/00216224:14330/22:00125612

Organizační jednotka

Fakulta informatiky

DOI

http://dx.doi.org/10.46298/LMCS-18(1:38)2022

UT WoS

000769134500001

Klíčová slova anglicky

strongly connected components; symbolic algorithm; BDD

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 28. 3. 2023 10:11, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Edge-coloured directed graphs provide an essential structure for modelling and analysis of complex systems arising in many scientific disciplines (e.g. feature-oriented systems, gene regulatory networks, etc.). One of the fundamental problems for edge-coloured graphs is the detection of strongly connected components, or SCCs. The size of edge-coloured graphs appearing in practice can be enormous both in the number of vertices and colours. The large number of vertices prevents us from analysing such graphs using explicit SCC detection algorithms, such as Tarjan's, which motivates the use of a symbolic approach. However, the large number of colours also renders existing symbolic SCC detection algorithms impractical. This paper proposes a novel algorithm that symbolically computes all the monochromatic strongly connected components of an edge-coloured graph. In the worst case, the algorithm performs O(p . n . log n) symbolic steps, where p is the number of colours and n is the number of vertices. We evaluate the algorithm using an experimental implementation based on binary decision diagrams (BDDs). Specifically, we use our implementation to explore the SCCs of a large collection of coloured graphs (up to 2(48)) obtained from Boolean networks - a modelling framework commonly appearing in systems biology.

Návaznosti

MUNI/A/1145/2021, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace XI. (Akronym: SV-FI MAV XI.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace XI.

Citovat

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA a David ŠAFRÁNEK. BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs. Logical Methods in Computer Science. Episciences, 2022, roč. 18, č. 1, s. 1-27. ISSN 1860-5974. Dostupné z: https://dx.doi.org/10.46298/LMCS-18(1:38)2022.

@article{1845005,
   author = {Beneš, Nikola and Brim, Luboš and Pastva, Samuel and Šafránek, David},
   article_number = {1},
   doi = {http://dx.doi.org/10.46298/LMCS-18(1:38)2022},
   keywords = {strongly connected components; symbolic algorithm; BDD},
   language = {eng},
   issn = {1860-5974},
   journal = {Logical Methods in Computer Science},
   title = {BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs},
   url = {https://lmcs.episciences.org/9198},
   volume = {18},
   year = {2022}
}

TY  - JOUR
ID  - 1845005
AU  - Beneš, Nikola - Brim, Luboš - Pastva, Samuel - Šafránek, David
PY  - 2022
TI  - BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs
JF  - Logical Methods in Computer Science
VL  - 18
IS  - 1
SP  - 1-27
EP  - 1-27
PB  - Episciences
SN  - 18605974
KW  - strongly connected components
KW  - symbolic algorithm
KW  - BDD
UR  - https://lmcs.episciences.org/9198
N2  - Edge-coloured directed graphs provide an essential structure for modelling and analysis of complex systems arising in many scientific disciplines (e.g. feature-oriented systems, gene regulatory networks, etc.). One of the fundamental problems for edge-coloured graphs is the detection of strongly connected components, or SCCs. The size of edge-coloured graphs appearing in practice can be enormous both in the number of vertices and colours. The large number of vertices prevents us from analysing such graphs using explicit SCC detection algorithms, such as Tarjan's, which motivates the use of a symbolic approach. However, the large number of colours also renders existing symbolic SCC detection algorithms impractical. This paper proposes a novel algorithm that symbolically computes all the monochromatic strongly connected components of an edge-coloured graph. In the worst case, the algorithm performs O(p . n . log n) symbolic steps, where p is the number of colours and n is the number of vertices. We evaluate the algorithm using an experimental implementation based on binary decision diagrams (BDDs). Specifically, we use our implementation to explore the SCCs of a large collection of coloured graphs (up to 2(48)) obtained from Boolean networks - a modelling framework commonly appearing in systems biology.
ER  -

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA a David ŠAFRÁNEK. BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs. \textit{Logical Methods in Computer Science}. Episciences, 2022, roč.~18, č.~1, s.~1-27. ISSN~1860-5974. Dostupné z: https://dx.doi.org/10.46298/LMCS-18(1:38)2022.

Podrobný výpis o publikaci