To model Stochastic systems, it requires presenting the formalism to support the probabilistic transition. Discrete-Time Markov Chain (DTMC) is formally defined as follows:

In this paper, states s ∈ S are not merely abstract indices but are defined by a valuation of a set of model variables V = { v 1 , v 2 , … , v k }. Thus, each state s can be represented as a vector v s = ( v a l ( v 1 ) , v a l ( v 2 ) , … , v a l ( v k ) ), which serves as the feature vector for our learning algorithms. We define a feature mapping function F : S → R k that maps each state to its corresponding valuation.

For any state s ∈ S, we use post ( s ) for the set of all immediate successor state of s and define it as post ( s ) = { s ′ ∈ S ∣ P ( s , s ′ ) > 0 }. A path in a Markov chain is a (finite or infinite) sequence of states with a positive transition probability function. That is, π = s 0 s 1 s 2 s 3 ⋯ is a path in DTMC such that ∀ i ⩾ 0: s i ∈ S, P ( s i , s i + 1 ) > 0. We use π [ i ] to denote the ( i + 1 )-th state of the path, i.e. π [ 0 ] for the first state of π, and so on. The probability of a finite path is calculated by multiplying the corresponding transition probability function, e.g. P r ( π ) = P ( s 0 , s 1 ) × P ( s 1 , s 2 ) × P ( s 2 , s 3 ) × ⋯ . For a set of infinite paths, a probability measure is defined on the corresponding set of cylinder set (Baier and Katoen, 2008).

A strongly connected component (SCC) of a DTMC is a non-empty set C ⊆ S where for each pair of states s and s ′ ∈ C there is a path from s to s ′ . A set C ⊆ S is a bottom strongly connected component (BSCC) if C is a maximal SCC and for each s ∈ C and s ′ ∈ S ∖ C we have P ( s , s ′ ) = 0. For the DTMC of Example 1, { s 5 } and { s 7 } are only the two non-trivial BSCCs. More details about probabilistic model checking, reachability probabilities, and the theory behind them are available in Baier and Katoen (2008), Baier et al. (2019).

The properties of a Markovian process can be formulated in a Probabilistic Computation Tree Logic (PCTL).

The semantics of a PCTL formula are defined as follows. Given a DTMC M = ( S , P , s 0 , G , A P ), state s ∈ S, and satisfaction relation ⊧: •

s ⊧ ϕ iff ϕ is valid in s,

It is worth noting that the above properties are all assertions, that is, we would expect a true or false answer to them. In some probabilistic model checkers such as PRISM (Kwiatkowska et al., 2011), quantitative properties can be directly specified that compute the exact probability instead of verifying whether the probability is in bound J or not. Thus, P = ? ( ψ ) computes the exact value of sum of probabilities in paths starting at s 0 and satisfying ψ.

Qualitative verification computes states where the probability of reaching G is exactly 0 or 1 (Baier et al. (2019)). S 1 denotes states with probability 1 of reaching goal states, while S 0 represents those with probability 0. Anther important set of states is S ? = S ∖ ( S 0 ∪ S 1 ). Formally, for DTMCs, we define S 0 = { s ∈ S | s ⊧ P = 0 [ true U G ] }, S 1 = { s ∈ S | s ⊧ P = 1 [ true U G ] }.

Quantitative reachability probabilities in DTMCs and Markov Decision Processes (MDPs) are computed using numerical iterative methods. MDPs generalize DTMCs by incorporating non-deterministic choices between states (Baier and Katoen, 2008). Qualitative verification employs iterative graph-based algorithms (Mohagheghi and Salehi, 2020). While bounded properties offer finer verification in SMC (Budde et al., 2020a; Hahn and Hartmanns, 2016; Arora and Rao, 2020), we focus on unbounded properties.

High-level modelling languages offer a more efficient alternative to detailed probabilistic models like DTMCs for describing stochastic systems. The PRISM language (Kwiatkowska et al., 2011), supported by PRISM, STORM (Dehnert et al., 2017), and ePMC (Calinescu et al., 2019), is a prominent example. PRISM models consist of modules with bounded integer variables and probabilistic guarded commands that define system evolution. These high-level programmes are translated into low-level probabilistic transition systems, where states are represented by valid variable valuations. Example 3.

A PRISM programme for the Zeroconf protocol in Example 1 is proposed in Fig. 1b. This programme contains one module that includes a variable s. The upper-bound of s depends on the constant n that is determined by the user. The states of the corresponding DTMC model are defined as value s where each value shows a valid valuation for the programme variable. start, error, and ok are three labels to specify the desired properties.

Decision tree (DT) classifiers are established and well-known supervised learning methods that predict target values using decision rules derived from training data features (Murphy, 2022). Visualized as top-down binary trees, DTs use Boolean predicates at nodes and true/false edges, with decisions at leaf nodes. For a given input, one traverses the tree, evaluating predicates to reach a decision. In this paper, we employ DTs to approximate the set of states that cannot reach a goal state.

Binary decision diagrams (BDDs), introduced by Bryant (1986), are powerful data structures encoding Boolean functions, widely used in formal verification. As rooted and directed acyclic graphs (DAGs), BDDs compactly represent sets or relations. They consist of leaves labelled 0 or 1, and nodes representing variables, with edges denoting Boolean values true or false. In this paper, BDDs capture set S 0 efficiently, enabling reuse and avoiding recomputation.

Despite SMC’s advantage in attacking state space explosion, simulation termination remains a key challenge. For bounded reachability properties P J [ true U ⩽ t G ], termination occurs naturally when simulation length exceeds t. However, unbounded properties pose a greater challenge, as runs may continue infinitely without reaching a goal state, particularly when stuck in a BSCC without any goal states. These states belong to S 0 , but their detection isn’t straightforward. For unbounded formulas ψ = ϕ 1 U ϕ 2 , approximating P J [ ψ ] first requires approximating S 0 , where s ∈ S 0 ⟺ s ⊧ P = 0 [ ψ ].

This approach applies machine learning classifiers to efficiently decide when to end SMC simulations (Algorithm 1). The algorithm takes a DTMC model D with parameters δ and ϵ for the SMC confidence interval. Based on these parameters, it computes the number of runs n required to satisfy the Chernoff bound (Eq. (1)), and uses n ′ runs for training the decision tree classifier D T. As a simple heuristic, we set n ′ = n 10 (Line 3 of Algorithm 1).

The algorithm runs n ′ simulations following the standard SMC method, e.g. in Legay and Viswanathan (2015), Legay et al. (2010). These simulations start from s 0 and stop at goal states or detected BSCCs with maximum uncertainty ϵ (Daca et al., 2017). Depending on each run π, if π reaches a goal state, its states are added to S s a m ? as they cannot be in S 0 . If π reaches a BSCC without any goal states, the whole detected BSCC states are added to S s a m 0 , as they cannot reach a goal.

After n ′ runs, the algorithm has two training sets S s a m 0 and S s a m ? . It then uses machine learning to construct a decision tree classifier D T that can classify any state as belonging to S 0 or not, based on state’s variable valuations as data features. The SMC method then applies D T to classify states during the remaining 90% of simulation runs. Starting from s 0 , DT can be applied on a state s ∈ S considered as a successor state during a run. If it classifies s as in S 0 , the run is terminated early, reporting a 0 outcome. The training set size n ′ can be reduced if sufficient to build an accurate classifier.

The key factors affecting the performance of our method are memory consumption, runtime, and the correctness of SMC using decision trees in detecting states of S 0 . We aim to achieve a suitable trade-off among these factors in our approaches.

Memory Consumption.  The SMC method stores all states from each simulation run, leading to a worst-case space complexity linear in the model size. In practice, only a small portion of states are typically encountered. The size of the training sets S s a m 0 and S s a m ? also affects memory consumption. To address potential state explosion, we limit the size of these sets and terminate the training if the number of states exceeds the limit. Notably in machine learning, appropriate classifiers work on a limited number of training samples and generalize the results to predict the label of unseen data (Pasupa and Sunhem, 2016; Tadjudin and Landgrebe, 1996).

Using BDDs to precisely maintain S s a m 0 states is another solution. BDDs mark states as S 0 members only when confirmed as BSCC states, while providing efficient and compact data storage for S s a m 0 and S s a m ? in large DTMC models with multiple BSCCs.

Instead of using a single DT for all BSCCs, we can incrementally construct a BDD D to represent BSCC members. Initially, D stores states of the first detected BSCC. For subsequent runs, D checks for BSCC entrance while parallel on-the-fly detection continues. When new BSCCs are found, their states are added to D, enabling immediate detection in future runs. Example 7.

The corresponding BDD of Fig. 4a is demonstrated in Fig. 4b. Variables u, zx, and zy remain constant across states, thus ignoring in the BDD. The root of the BDD is conditioned on s = 3, if the condition is true, the left branch with solid line (labelled by T) is traversed; otherwise, the right branch with dashed line is followed. By evaluating the values of various parameters, the corresponding labels are derived at the terminal nodes labelled 1 and 0.

Applying a decision tree to simulation states incurs some overhead, potentially increasing computation time. To mitigate this, our approach can call the decision tree only every 10 or 20 times over states along a path. Using BDDs to store BSCCs accelerates SMC through early BSCC detection. With efficient set union operations, Algorithm 1 requires only one long run per BSCC, potentially reducing the required runs below n ′ .

Correctness of Computation. Correctness is measured by the error rate in reachability probability computations. Using classifiers like decision trees for determining S 0 membership introduces two types of errors: false positives (label an S ∖ S 0 state as in S 0 ) and false negatives (label an S 0 state as not in S 0 ). While false negatives merely cause redundant SMC computations and can be mitigated using parallel conservative methods (e.g. Daca et al., 2017), false positives critically affect correctness by causing incorrect simulation termination, thus impacting reachability probability calculations.

Although decision trees can achieve perfect classification on S s a m 0 and S s a m ? , they may misclassify new states. To reduce false positives, we can expand S s a m ? by randomly adding states not in S s a m 0 , leading to diversify S s a m ? . While this may increase false negatives by biasing the tree towards S ? , it reduces false positives.

Decision trees can generalize from a small training set, which is beneficial when only a portion of S 0 is in BSCCs (as in Fig. 2b). To terminate runs reaching S 0 as soon as possible and reduce overall running time, we should consider more S 0 states than just those in BSCCs for the training set. To this end, we propose two techniques that enable the decision tree to detect a larger portion of S 0 . In cases where explicitly representing the S s a m 0 set is infeasible, BDDs can be used to store it.

Adding States that Almost Surely Lead to S s a m 0 . We can add predecessor states to S s a m 0 if their successors are all in S s a m 0 , as these states almost surely lead to S 0 . Formally for s ∈ S s a m 0 , we add s ′ ∈ pre ( s ) to S s a m 0 if every s ″ ∈ post ( s ′ ) satisfies either s ″ = s ′ or s ″ ∈ S s a m 0 . Algorithm 2 uses this approach. Starting from the path’s final state in S s a m 0 , the algorithm processes states backwards. For each state, if all its successors belong to S s a m 0 , the algorithm adds it to S s a m 0 . Otherwise, it terminates, as the state’s membership in S s a m 0 cannot be determined. This algorithm can be called by Algorithm 1 after detecting a new BSCC, to expand S s a m 0 .

Using BDDs, hash tables, heap, or similar data structures may introduce overhead for this operation. An alternative is to consider only Dirac transitions (probability is 1). For state s = π [ i − 1 ], the algorithm adds s to S s a m 0 if it has a Dirac transition; otherwise, it terminates. This simplified check reduces overhead but may identify fewer states for S s a m 0 .

Statistical Analysis to Detect S 0 states. A large S 0 with small BSCCs may contains multiple SCCs that eventually reach a BSCC. Figure 5 illustrates this structure, where S 0 (shaded area) contains several nontrivial SCCs with paths to BSCCs. These nontrivial SCCs within S 0 can make simulation runs longer.

While simulation-based approaches exist for approximating SCCs (Brázdil et al., 2014), they cannot reliably identify S 0 due to potential goal state reachability. Our solution enhances S 0 detection beyond BSCC states through statistical sampling. For each randomly selected state, we run multiple simulations. If any simulation reaches a goal state, the state is excluded from S 0 . Otherwise, we can statistically infer its membership in S 0 with high confidence.

Algorithm 3 implements this approach. It first determines the required simulation count l based on confidence parameters δ and ϵ. Through k iterations, it selects states not in S s a m 0 and runs simulations until either reaching G or confirming BSCC containment without goal states. States reaching G are added to S s a m ? , while those confirmed unreachable are added to S s a m 0 along with their successor states.

Algorithm 3 determines the number of simulation runs l needed to ensure, with high confidence, that the probability of reaching G from s is below threshold ϵ. While this condition likely holds for many states reachable from s that are added to S s a m 0 , some states with non-zero probability of reaching G might be incorrectly included, affecting correctness. To mitigate this, we can modify Algorithm 3 by limiting either the number of successor states or the search depth (e.g. to 4 steps) when adding states to S s a m 0 .

A limitation of Algorithm 3 is its tendency to select many states for S s a m 0 but few for S s a m ? , potentially increasing false positives. We propose two extensions: 1) Algorithm 3 (V2) randomly adds states to S s a m ? (between the sizes of current S s a m ? and S s a m 0 ), while 2) Algorithm 3 (V3) runs single simulation from random states, adding successful goal-reaching paths to S s a m ? . Unlike the original algorithm, V3 discards states after one failed simulation run.

To determine the minimum number of simulation runs to meet the conditions of the confidence interval for the membership of a state in S 0 , we recall X i in Section 3 as the Bernoulli distribution with parameter p, that is, P r ( X i = 1 ) = p, 0 ⩽ p ⩽ 1. After running n simulations, we observe the outcome x _ = ( x 1 , x 2 , … , x n ). The probability of p given the evidence x _ is denoted by P r ( p | x _ ) (the posterior probability). We use the following lemma to obtain a bound for n.

If any simulation run reaches a goal state, s cannot be in S 0 . Lemma 1 determines the required number of simulation runs to establish an upper-bound for reachability probability with a specified confidence level. When no simulation reaches a goal state, even if s is incorrectly added to S s a m 0 , we can be confident that the probability of reaching G is below threshold δ. This ensures that such misclassification maintains the overall correctness of the SMC approach.

Our approach aims to reduce simulation run lengths by efficiently identifying paths that cannot reach goal states. We propose a statistical method that computes the mean and standard deviation of successful goal-reaching paths to establish an upper bound ( u b) for path length. The SMC method can then terminate runs exceeding u b, marking them as non-reaching outcomes. Using parameters ϵ and δ for confidence intervals, we calculate the required number of simulation runs n to satisfy the Chernoff-Hoffeding bound. This enhancement consists of two steps:

Training Step. Using n ′ = n 10 simulations as a heuristic, we compute mean μ and standard deviation σ of goal-reaching path lengths. Chebyshev’s inequality helps establish an upper bound that ensures the probability of reaching a goal state beyond this bound is below threshold ϵ ( P r ( | X − μ | ⩾ k · σ ) ⩽ 1 k 2 ), where X represents path length to G. Having ϵ as an upper-bound for errors in detecting a state in S 0 , we can set k = 1 ϵ . Assuming X > μ, we define u b = μ + 1 ϵ · σ as the path length upper bound.

Remaining SMC Runs. Once u b is established, SMC terminates any simulation exceeding this bound, as these paths have probability of at least 1 − ϵ of never reaching a goal state. This eliminates the need for BSCC detection. This statistical approach differs from our other approaches by reducing computational overhead through direct path length analysis rather than invoking constructed decision trees or BDDs. Furthermore, it provides mathematical control over false negative rates, which is not possible with decision trees.

We evaluate our approaches using four standard DTMC model classes: Nand, brp, egl, and crowds, as documented in Kwiatkowska et al. (2012), Hartmanns et al. (2019), Budde et al. (2020b). The reachability properties under investigation are:

We implemented our algorithms in PRISM model checker, constructing models with varying parameter values. For fair comparison, we disabled pre-computation of S 0 and S 1 sets. To provide the reproducibility of our results and to maintain a balance between detection performance and computational overhead, we configured the DT classifiers with the following hyperparameters: Max Depth: limited to values between 4 and 10 (depending on model complexity) to avoid overfitting to specific simulation paths; Criterion: we used Gini impurity to measure the quality of splits, as it is computationally efficient for large state spaces; Random State: a fixed seed 0 was utilized for the training process to provide the reproducibility of the results across multiple executions. The other hyperparameters are set to their default values.

To evaluate the performance of the DT classifier, we employed a series of standard machine learning metrics. For this analysis, 10 % of the whole set of states was allocated for training the model, while the remaining 90 % was reserved for testing its predictive accuracy. Precision measures the reliability of a positive prediction of S 0 . It answers: of all states of the model labelled as S 0 , how many were actually S 0 ? Recall (true positive rate) measures the model’s ability to find all positive instances, i.e. of all S 0 states that exist, how many did the model successfully find? Specificity measures the model’s ability to correctly identify negative instances, of all the non- S 0 ( S ? ) states, how many were correctly labelled as such? Negative Predictive Value (NPV) measures the reliability of a negative prediction. It answers: of all states the model labelled as S ? , how many were truly S ? ? False Positive Rate (FPR) answers a different question, i.e. of all the cases that were actually S ? , how many did the model incorrectly flag as S 0 ?. Finally, we used the Receiver Operating Characteristic (ROC) curve to visualize the classifier’s performance across various threshold settings. By plotting recall against FPR, the ROC curve illustrates the model’s fundamental ability to distinguish between classes.

To evaluate the S 0 detection, the egl model with parameters N = 5 and L = 6, as well as Algorithm 3 (V3) is considered. In the egl model with the predefined parameters, each state includes 84 feature values, used for training the DT. With a Precision of 97.5 %, we can deduce that when the model identifies something as S 0 , it is almost certainly correct. This high level of certainty is backed by a Specificity of 95.1 %, meaning it rarely confuses the background with our target. The trade-off for this high accuracy is that the model is somewhat conservative; it only catches about 67.4 % of all actual S 0 instances. In contrast, the model takes a wide-net approach for S ? . It achieves a high recall of 95 %, ensuring that very few actual S ? instances are missed. However, this inclusiveness comes at a cost to precision, a fact further reflected by the 50.9 % NPV. This tells us that while the model finds almost every S ? case, about half of those predictions are actually false alarms. Ultimately, with F1-scores of 80 % and 66 %, the data shows a classifier that is fine-tuned to be an expert at identifying the target class while serving as a sensitive, albeit less precise, detector for the rest. These findings are consistent with the discrete operating points observed in the precision-recall and ROC curves illustrated in Fig. 7.

Figure 7 illustrates a quantitative evaluation of the DT for identifying S 0 states by demonstrating precision-recall and ROC curves. Our evaluation reveals that the classifier is both reliable and highly discerning, achieving an average precision (AP) of 0.90 and an area under the curve (AUC) of 0.81. What stands out most is the model’s sweet spot at approximately 68 % recall. At this point, the classifier maintains nearly perfect precision while keeping false alarms to a remarkably low 5 %. While we can push the model to catch every single positive instance ( 100 % recall), it does so at a reasonable cost, with precision dipping to 0.74. Throughout this range, the model remains remarkably stable, consistently holding an F1-score of about 80 %. Essentially, these curves describe a classifier that is good at making high-confidence predictions. These results demonstrate that the constructed DT provides good separation, suggesting that our proposed DT-based methods are promising.

Table 1 presents our experimental results  showing for each case study: model name and parameter values, total number of states ( | S |), non-goal-reaching states ( | S 0 |) as reported by PRISM. Moreover, the number of approximated S 0 states ( | ≈ S 0 |) by our learning methods, as well as the correctness in computing reachability probability for the initial state are reported. The correctness metric for reachability probabilities is defined as x ˜ s 0 x s 0 , where x s 0 = P = ? ( Ψ ) represents the actual probability and x ˜ s 0 denotes the computed value using decision trees for S 0 and S ? labelling. We evaluate three versions of Algorithm 3: V1: original algorithm without S s a m 0 or S s a m ? additions, V2: adds randomly selected states to S s a m ? , and V3: adds goal-reaching path states.

Algorithms 1 and 2 yield more conservative results for the first three model classes. For these cases and PCTL properties, the models contain several small BSCCs where the constructed decision trees properly detect the states within them. The main limitation of these approaches (Algorithms 1 and 2) is its tendency to overfit to the states in BSCCs, resulting in poor generalization to other parts of S 0 . While this limitation affects the simulation run length, it maintains high precision in BSCC detection and run termination. For the last class of case studies (brp), the computational correctness varies across models depending on the parameter values. The first two algorithms suffer from overfitting, incorrectly labelling some unseen states in S ∖ S 0 as belonging to S 0 .

The experimental results demonstrate that in most cases, balancing the sizes of S s a m 0 and S s a m ? generally improves the computational correctness of Algorithm 3. While the first version of this algorithm (denoted as (V1) in Table 1) performs poorly and achieves correctness less than 95% in nine cases, there is only one case for version 2 and two cases for version 3 that the correctness is less than 95%. Notably, the main purpose of presenting the second and the third versions of Algorithm 3 is to cover its weaknesses in providing some results that are far from the exact value.

In addition to computational correctness, we report the number of detected states for S 0 (denoted by | ≈ S 0 |) for each approach. For egl and crowds models, the values of | ≈ S 0 | are not far away from | S 0 |. For the crowds models, Algorithm 2 demonstrates the best performance in detecting a substantial portion of | S 0 | while maintaining computational correctness. For these models and other model classes, Algorithm 3 (V1) labels the widest range of states as | S 0 | and achieves the highest | ≈ S 0 | among all proposed approaches.

In the case of Nand models, Algorithms 1 and 2 overfit to the training set and detect only a small portion of states in S 0 . For these models, the first and second versions of Algorithm 3 label an excessive number of states as S 0 , which degrades computational correctness. Similarly, in egl models, Algorithm 1 exhibits overfitting.

To evaluate the impact of the statistical approach for terminating simulation runs, we apply the method proposed in Section 4.3 to the selected case study models. The results are presented in Table 2. For each model, we execute 10% of the required simulations for the training step. The average and standard deviation of the lengths for each model are reported in the table. Based on the relation proposed in Section 4.3 and to bound the errors to less than 0.01, we determine the computed upper bounds for the length of remaining simulation runs. In three classes of models (egl, crowds, and brp), the computed upper bounds for terminating simulation runs are completely perfect and correctly terminate runs that have reached S 0 . For the Nand models, the correctness exceeds 99.6%, indicating near-perfect run termination.

Statistical model checking reliability requires multiple runs to evaluate result stability, defined as the consistency of results across multiple experimental runs. This evaluation employs t-test and Levene’s test (Milton and Arnold, 2002), where Levene’s test examines variance equality, and t-test verifies mean equality between independent result groups.

In the evaluation process, the proposed algorithms were independently executed 30 times and the probability of reachability properties was computed for a single instance, i.e. in the case of egl, N = 6, and L = 8. Algorithm 3 (V3) and the instance were selected as a representative example of all possible parameters and instances. The experimental runs were subsequently partitioned into two distinct groups, each comprising 15 independent runs. Table 3 represents the stability analysis of the experimental results.

The Levene’s test significance value (Sig. = 0.598) exceeds 0.01, confirming equal variance assumption. The t-test significance (0.520) and the difference interval containing 0 indicate no statistically significant differences between group means at 99% confidence, confirming result stability in the sense that the number of runs is sufficient.

Based on their superior performance and robustness within the DTMC models for the SMC task, we selected Algorithm 2 and Algorithm 3 (V3) as the basis for our comparison. In the literature, SimTermination and SimAnalysis developed by Younes et al. (2010), SimAdaptive by Daca et al. (2017), and the method developed by Brázdil et al. (2015) represent the state-of-the-art. Since the approach by Daca et al. has been shown to dominate these existing methods (Daca et al., 2017), we evaluate it against our proposed algorithms. The results, obtained using a machine equipped with a 1.8 GHz Intel(R) Core(TM) i7-10510U processor and 12 GB of RAM running Ubuntu 24.04, are presented in Table 4. In the table, the running time in seconds, memory consumption for both the training step and the active simulation phase of SMC process, and the number of detected S 0 states are reported.

As demonstrated in Table 4, in most cases, our proposed approaches run significantly faster than the state-of-the-art SimAdaptive method while maintaining the computational correctness of the results. For example, in the case of egl for N = 5 and L = 6, Algorithm 2 and Algorithm 3(V3) consume 7.6 and 8.3 seconds, respectively, while SimAdaptive takes three to four times longer. For the Nand and brp cases, Algorithm 3(V3) works faster than Algorithm 2. Compared to SimAdaptive, our proposed framework labels a significantly larger portion of states as belonging to S 0 without dramatically degrading the precision of reachability probabilities. This ability to identify a wider range of S 0 states leads to the early termination of simulation runs that would otherwise enter BSCCs. In contrast, SimAdaptive detects only a small part of S 0 and continues simulations on many states that actually have zero probability of reaching a goal state. For example, in the case of egl for N = 5 and L = 8, Algorithm 2 and Algorithm 3(V3) detect 114 869 and 112 263 states of 115 136 states in S 0 , while SimAdaptive detects 522 states. Regarding resource efficiency, the memory consumption of our compared approaches remains highly manageable, with usage in most cases staying below 1MB.