Abstract. The computation of bottom strongly connected components (BSCCs) is a fundamental task in model checking, as well as in characterizing the attractors of dynamical systems. As such, symbolic algorithms for BSCCs have received special attention, and are based on the idea that the computation of an SCC can be stopped early, as soon as it is deemed to be non-bottom.In this paper we introduce Pendant, a new symbolic algorithm for computing BSCCs which runs in linear symbolic time. In contrast to the standard approach of escaping non-bottom SCCs, Pendant aims to start the computation from nodes that are likely to belong to BSCCs, and thus is more effective in sidestepping SCCs that are non-bottom. Moreover, we employ a simple yet powerful deadlock-detection technique, that quickly identifies singleton BSCCs before the main algorithm is run. Our experimental evaluation on three diverse datasets of 553 models demonstrates the efficacy of our two methods: Pendant is decisively faster than the standard existing algorithm for BSCC computation, while deadlock detection improves the performance of each algorithm significantly.

This is the artifact for the paper "Fast Symbolic Computation of Bottom SCCs", by Anna B. Jakobsen, Rasmus S. M. Jørgensen, Jaco van de Pol and Andreas Pavlogiannis, appearing in TACAS 2024. The artifact contains the LTSmin toolset, extended with an implementation of the algorithms from the paper, to compute the Bottom Strongly Connected Components of a directed graph, provided symbolically by BDDs (Binary Decision Diagrams). The artifact also contains the data set, consisting of directed graphs (state spaces) specified in DVE (Divine), PNML (Petri Nets) and BN (Boolean Networks). The file README.md contains the instructions how to setup the artifact on Ubuntu and how to run the experiment scripts.