# An Approach to the State Explosion Problem: SOPC Case Study
## 2 Related Work  
In [12], [PERSON] et al. use distributed memory and computation for storing and exploring the state space of the model of a system. They present and compare different multi-thread, distributed, and cloud approaches to face the state space explosion problem. In [13], [PERSON] et al. propose an approach based on knowledge exploration for state space management in checking the reachability of complex software systems. The ensemble machine learning technique uses the Boosting method along with decision trees. This method generates k predictive models after sampling k times. Finally, it uses a voting mechanism to predict the labels of the final path. In [14], [PERSON] et al. propose a method based on symmetry reduction to reduce state space during model checking on secure routing protocols. They focus on the shapes of topologies. Loosely speaking, if the shape of the topology represented by the current state is the same as that of the searched state, the current state can be regarded as equivalent to the searched state by replacing nodes. In [15], in order to combat the state space explosion associated with BMC, [PERSON] et al. propose the method starts by combining module-level abstraction-refinement with slicing to reduce the size of the model under verification. In [16], [PERSON] et al. propose a novel supervisor synthesis framework using automata learning and compositional model checking to generate the permissive local supervisors in a distributed manner. In [17], [PERSON] et al. investigate the problems of applying the anti-chain approach to timed refinement checking and probabilistic refinement checking and show that the state space can be reduced considerably by employing the anti-chain approach. In [18], [PERSON] et al. propose methods to accelerate hardware security verification and vulnerability detection through state space reduction. Specifically, we reduce the state space of the model by performing value reduction and transition relation reduction. The control flow and data-dependent graphs control the process of value reduction and transition relation reduction. In [19], [PERSON] et al. present an approach for schedulability analysis of Distributed Integrated Modular Avionics (DIMA) systems that consist of spatially distributed ARINC-653 multicore modules connected by a unified Avionics Full-Duplex Switched Ethernet (AFDX) network. In [20], to circumvent the state space explosion, [PERSON] et al. rely on stochastic approximation techniques, which replace the large model with a simpler one guaranteed to be probabilistically consistent. In [21], [PERSON] et al. introduced parametric interval counter abstraction that allowed us to verify the safety and liveness of threshold-based fault-tolerant distributed algorithms (FTDAs). In [22], [PERSON] et al. focus on a major improvement in the analysis of reachabilityproperties in large-scale dynamical biological models. They introduce a hybrid approach, ASPReach, which combines static analysis and stochastic search to break the limits of existing approaches. In [23], [PERSON] et al. propose a numerical integration algorithm to approximate the probability that a process conforms to a specification that belongs to a subclass of deterministic timed automata (DTA). They combat the state space explosion problem by using a dynamic state space that contains only the most relevant states. In [24], [PERSON] et al. present several techniques to tackle the state explosion problem at some consistent global state of a distributed system. In [25], in order to shrink the state space being observed during the model-checking process of TV software, a method is proposed that relies on using previous test logs to generate a partly non-deterministic user agent model. In [26], [PERSON] presents a new timing analysis algorithm for efficient state space exploration during the synthesis of timed circuits or the verification of timed systems. In [27], [PERSON] et al.