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

BENEŠ, Nikola, Luboš BRIM, Samuel PASTVA and David ŠAFRÁNEK. BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs. Logical Methods in Computer Science. Episciences, 2022, vol. 18, No 1, p. 1-27. ISSN 1860-5974. Available from: https://dx.doi.org/10.46298/LMCS-18(1:38)2022.

Basic information

• Original name: BDD-Based Algorithm for SCC Decomposition of Edge-Coloured Graphs
• Authors: BENEŠ, Nikola (203 Czech Republic, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution), Samuel PASTVA (703 Slovakia, belonging to the institution) and David ŠAFRÁNEK (203 Czech Republic, guarantor, belonging to the institution).
• Edition: Logical Methods in Computer Science, Episciences, 2022, 1860-5974.

Other information

• Original language: English
• Type of outcome: Article in a journal
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Germany
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• Impact factor: Impact factor: 0.600
• RIV identification code: RIV/00216224:14330/22:00125612
• Organization unit: Faculty of Informatics
• Doi: http://dx.doi.org/10.46298/LMCS-18(1:38)2022
• UT WoS: 000769134500001
• Keywords in English: strongly connected components; symbolic algorithm; BDD
• Tags: International impact, Reviewed

Abstract

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.

Links

• MUNI/A/1145/2021, interní kód MU: Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace XI. (Acronym: SV-FI MAV XI.)

Investor: Masaryk University