Computing Bottom SCCs Symbolically Using Transition Guided Reduction.

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

International Conference on Computer Aided Verification (CAV) 2021

Detection of bottom strongly connected components (BSCC) in state-transition graphs is an important problem with many applications, such as detecting recurrent states in Markov chains or attractors in dynamical systems. However, these graphs’ size is often entirely out of reach for algorithms using explicit state-space exploration, necessitating alternative approaches such as the symbolic one.

Symbolic methods for BSCC detection often show impressive performance, but can sometimes take a long time to converge in large graphs. In this paper, we provide a symbolic state-space reduction method for labelled transition systems, called interleaved transition guided reduction (ITGR), which aims to alleviate current problems of BSCC detection by efficiently identifying large portions of the non-BSCC states.

Cite this paper as: Beneš N., Brim L., Pastva S., Šafránek D. (2021) Computing Bottom SCCs Symbolically Using Transition Guided Reduction. In: Silva A., Leino K.R.M. (eds) Computer Aided Verification. CAV 2021. Lecture Notes in Computer Science, vol 12759. Springer, Cham./citeas>