Computing Bottom SCCs Symbolically Using Transition Guided Reduction

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.We evaluate the suggested heuristic on an extensive collection of 125 real-world biologically motivated systems. We show that ITGR can easily handle all these models while being either the only method to finish, or providing at least an order-of-magnitude speedup over existing state-of-the-art methods. We then use a set of synthetic benchmarks to demonstrate that the technique also consistently scales to graphs with more than $$2^{1000}$$ 2 1000 vertices, which was not possible using previous methods.

Efficient CSP Model Checking for Symbolic State-space Exploration with Application in Bacterial Chemo-Taxis Modelings

Event locality is a class of theory that can clearly minimizes the memory and time required to store the state space. We present the multi-way decision diagrams to encode the next-state functions based on event locality and CSP’s stable failure. Instead of studying symbolic overall model, we apply the above thinking to the set of sub-models. Furthermore, we focus on saturation algorithms for CSP theory. And the algorithms consist of two phases, the universal process’s saturation checking and the single CSP symbol’s saturation checking. In the former case, the algorithms discuss better iteration strategy and recursive local fifix-point computations. In the latter case, the the single CSP symbol’s saturation checking calls the former algorithms, being combined preformed events and refusal events. Finally, we discuss bacterial chemotaxis modeled in CSP’s framework and saturation checking used to check the predefifined properties. The all algorithms are implemented in CSP tool FDR, the running results show that our algorithms often perform signifificantly faster than other conventional algorithms.