Detecting strongly connected components in large distributed state spaces

Detecting cycles in a state space is a key task in verification algortihms like LTL/CTL model checking and, less well known, reduction modulo branching bisimulation. This paper focuses on the problem of finding cycles (strongly connected components) in very large distributed state spaces. We present a collection of state space transformations meant as building blocks for custom algorithms. We also describe two example algorithms and show that they perform well on practical case studies