Symbolic Coloured SCC Decomposition

N. Beneš, L. Brim, S. Pastva, D. Šafránek

Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2021

Problems arising in many scientific disciplines are often modelled using edge-coloured directed graphs. These can be enormous in the number of both vertices and colours. Given such a graph, the original problem frequently translates to the detection of the graph’s strongly connected components, which is challenging at this scale. We propose a new, symbolic algorithm that computes all the monochromatic strongly connected components of an edge-coloured graph. In the worst case, the algorithm performs 𝑂(𝑝⋅𝑛⋅log𝑛) symbolic steps, where p is the number of colours and n the number of vertices. We evaluate the algorithm using an experimental implementation based on Binary Decision Diagrams (BDDs).

Cite this paper as: Beneš N., Brim L., Pastva S., Šafránek D. (2021) Symbolic Coloured SCC Decomposition. In: Groote J.F., Larsen K.G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. Lecture Notes in Computer Science, vol 12652. Springer, Cham