Probabilistic black-box reachability checking (extended version)

Model checking has a long-standing tradition in software verification. Given a system design, model-checking techniques determine whether requirements stated as formal properties are satisfied. These techniques and other forms of model-based verification fall short if no design is available. Model learning provides a solution to this issue. It establishes the basis for model-based verification by automatically learning automata models of black-box systems from observed data. Data used as basis for learning is usually given in the form of system traces, that is, sequences of system events, which may be partitioned into input and output events. Note that model learning is also often referred to as model inference, thus we use both terms interchangeably.

There are two main forms of model learning: passive learning and active learning. Passive learning learns from preexisting data such as system logs, while active learning actively queries the system that is examined to gain relevant information. This can for instance be done via testing. Noteworthy early examples of passive learning techniques are RPNI for regular languages [27, 41] and Alergia [11] for stochastic regular languages, which learn deterministic finite automata (DFAs) and their stochastic counterparts, respectively. Both, RPNI and Alergia, apply a principle called state-merging. More recent work based on this principle extends the applicability of passive model learning to timed systems [52], Moore machines [24] and to stochastic systems involving non-deterministic choices [35, 36], which we use in this article. All these approaches have in common that the models they learn depend on given sampled training data.

In contrast to this, active learning approaches rely on the possibility to query relevant information. Angluin formalised this by introducing the minimally adequate teacher framework in her seminal work on the \(L^*\) algorithm [4]. This framework assumes the existence of a teacher that is able to answer two types of queries: membership queries and equivalence queries. When a model of a software system is learned, membership queries basically check whether a given traces can be observed and equivalence queries check whether a hypothesised system model is equivalent to the system under investigation. In practice, both queries are usually implemented via testing. Since the introduction of \(L^*\), it has been adapted and extended to various types of systems like Mealy machines [37, 46], timed systems [25] and non-deterministic systems [28, 53]. There are also \(L^*\)-based learning approaches applicable for probabilistic system models [9, 19], but they place strong assumptions on the information that can be queried. These approaches are therefore unsuitable considering a testing scenario, which allows interaction with a black-box system only via testing.

In this paper, we consider such a testing scenario, in which we know the interface of a black-box system and we can gain information by testing the system. Furthermore, we assume that inputs to the system can be freely chosen and that reactions are stochastic. This makes Markov decision processes (MDPs) a well-suited choice of model type. MDPs allow for non-deterministic choices of inputs, while state transitions are stochastic, whereby outputs are produced depending on the entered state. Given such a system, we aim at generating testing strategies that produce desired outputs with high probability. For learning, we rely on an adaptation of Alergia [11] called IOAlergia [35, 36], which learns MDPs. While this learning technique is passive in general, our technique is active, as we generate new data for learning by testing. In an iterative approach, we steer the data generation based on learned models towards desired outputs to explore relevant parts of the system more thoroughly. That way, we aim at iteratively improving the accuracy of learning with respect to these outputs. This is in contrast to the application of IOAlergia in an active setting by Chen and Nielsen [13], as they aimed at actively improving the overall accuracy of learned models.

Model learning enables various forms of verification for black-box systems, such as differential equivalence testing on model-level [5, 48, 49], model-checking [20, 21] and model-based testing with learned models [1]. A particularly interesting technique combining model learning, model checking and testing is black-box checking introduced by Peled et al. [42]. This technique learns models of black-box systems in the form of DFAs on-the-fly and iteratively via \(L^*\). Whenever a hypothesis automaton model is created, the hypothesis is model checked which may reveal a fault in the system or show that learning was incomplete and needs to be continued. If model checking does not reveal a fault, equivalence between the hypothesis and the black-box system is checked via testing. In case, non-equivalence is detected the learned hypothesis is extended and learning continues.

Inspired by black-box checking, we propose an approach to analyse reactive systems exhibiting stochastic behaviour in a black-box setting. We also follow a learning-based approach involving repeated testing and probabilistic model-checking. Instead of targeting general properties, e.g., formulated in probabilistic temporal logics, we check reachability as a first step. Since we follow a simulation-based approach, we check bounded reachability. Rather than learning DFAs, we assume that systems can be modelled by MDPs. Hence, we consider systems controllable by inputs, chosen by an environment or a tester. As such, these systems involve non-determinism resulting from the choice of inputs and stochastic behaviour reflected in state transitions and outputs. Given such a system, our goal in bounded reachability checking is to find an input-selection strategy, i.e. a resolution of non-determinism, which maximises the probability of reaching a certain property within a bounded number of steps. Properties can, for example, be the observation of desired outputs. A possible application scenario for our technique is stress testing of systems with stochastic failures. We could generate a testing strategy that provokes such failures.

The approach we follow is shown in Fig. 1. First, we sample system traces randomly. Then, we infer an MDP from these traces via the state-merging-based method described by Mao et al. [35, 36], which as noted above is called IOAlergia. Once we inferred a hypothesis model \({\mathcal {M}_\mathrm {h}}_1\), we use the Prism model checker [29] for a reachability analysis to find the maximal probability of reaching a state satisfying a property \(\psi \). Prism computes a probability p and a strategy \(s_1\) (also called adversary or scheduler) to reach \(\psi \) with p. Since IOAlergia infers models from system traces, the quality of the model \({\mathcal {M}_\mathrm {h}}_1\) depends on these traces. If \(\psi \) is not adequately covered, \(s_1\) inferred from \({\mathcal {M}_\mathrm {h}}_1\) may perform poorly and rarely reach \(\psi \). To account for that, we follow an incremental process. After initial random sampling, we iteratively infer models \({\mathcal {M}_\mathrm {h}}_i\) from which we infer strategies \(s_i\). To sample new traces for \({\mathcal {M}_\mathrm {h}}_{i+1}\) we select inputs randomly and based on \(s_i\), that is, we use the strategy \(s_i\) for directed testing. Selecting inputs with \(s_i\) ensures that paths relevant to \(\psi \) will be explored more thoroughly. This process is repeated until either a maximal number of rounds n has been executed, or a heuristic detects that the search has converged to a scheduler.

We mainly use Prism to generate strategies, but ignore the probabilities computed in the reachability analysis. Since the computations are based on possibly inaccurate learned models, the probabilities may significantly differ from the true probabilities. Strategies, however, may serve as testing strategies regardless of the accuracy of the learned models. In fact, we evaluate the final strategy generated in the process described above via directed testing of the the system under test (SUT). Since the behaviour under a strategy is purely probabilistic, this is a form of Monte Carlo simulation, which is commonly used in statistical model-checking (SMC) [31]. The evaluation provides an estimation of the probability of reaching \(\psi \) with the actual SUT under strategy \(s_l\), where l is the last round that has been executed. By directly interacting with the SUT during evaluation, the computed estimation is an approximate lower bound for the optimal probability. In contrast to this, the reachability probabilities computed by Prism based on the learned model do not enjoy this property.

In summary, we combine techniques from various disciplines to optimise the probability of observing desired outputs within a bounded number of steps.Parts of this paper have already been published in the proceedings of the \(17\mathrm{th}\) International Conference on Runtime Verification [3]. Additional content presented in the current paper covers the heuristic check for detecting convergence, a more thorough evaluation including two new case studies and several further improvements throughout the paper.

The rest of this paper is structured as follows. In Sect. 2, we will discuss related work. Section 3 introduces preliminaries used in Sect. 4 which discusses the proposed approach. We present evaluation results in Sect. 5. Finally, we provide an outlook on future work and conclude in Sect. 6.

As discussed before, black-box checking [42] is closely related. In contrast to our technique, it considers non-stochastic systems, but more general properties. Various follow-up work demonstrates the potential of learning-based verification. Extensions, e.g., take existing models into account [26], focus on the composition of black-box and white-box components [17], or check security properties [47].

Mao et al. [34‐36] also inferred probabilistic models with the purpose of model checking. In fact, we apply the model-inference technique for MDPs described by them. Wang et al. [54] apply a variant of Alergia as well and take properties into account during model inference with the goal of probabilistic model-checking. They apply automated property-specific abstraction/refinement to decrease the model-checking runtime. Nouri et al. [39] also combine stochastic learning and abstraction with respect to some property. Their goal is to improve the runtime of SMC. Notably, their approach could also be applied for black-box systems, but does not consider controllability via inputs. Further work on SMC of black-box systems can be found in [45, 55].

Although we did not adapt IOAlergia, a passive model-inference technique, we apply it in an active setting. Chen and Nielsen [13] describe active learning of MDPs based on IOAlergia. However, they do not aim at model checking, but try to reduce the required number of samples by directing sampling towards uncertainties.

We try to find optimal schedulers for MDPs. This problem has been solved in other simulation-based verification approaches as well, like in SMC. A lightweight approach for finding schedulers in SMC is described in [14, 33]. By representing schedulers efficiently, they are able to consider history-dependent schedulers and through “smart sampling” they accomplish finding near-optimal schedulers with low simulation budget. Brázdil et al. [10] presented an approach to unbounded reachability analysis via SMC. The technique is based on delayed Q-learning, a form of reinforcement learning, requiring only limited knowledge of the system (but more than our technique). Another approach using reinforcement learning for strategy inference for reachability objectives has been presented by David et al. [15]. They minimise expected cost while respecting worst-case time bounds.

Learning-based synthesis of control strategies for MDPs has also been studied by Fu and Topcu [23]. They obtain control strategies which are approximately optimal with respect to linear temporal logic (LTL) specifications. They consider transition probabilities to be initially unknown, but in contrast to our setting they assume the MDP structure to be known.

We introduce background material following [22, 36], but consider only finite traces, finite paths, and bounded reachability, as we use a simulation-based approach. The restriction to bounded properties is also commonly found in SMC [31], which is also simulation-based and from which we apply concepts. Moreover, SMC of unbounded properties is especially challenging in a black-box setting [32].

Basics. Let \(\varSigma ^\mathrm {in}\) and \(\varSigma ^\mathrm {out}\) be sets of input and output symbols. An input/output string s is an alternating sequence of inputs and outputs, starting with an output, i.e. \(s\in \varSigma ^\mathrm {out} \times (\varSigma ^\mathrm {in} \times \varSigma ^\mathrm {out})^*\). We denote by |s| the number of input symbols in s and refer to it also as string/trace length. Given a set S, we denote by \( Dist (S)\) the set of probability distributions over S, i.e. for all \(\mu \) in \( Dist (S)\) we have \(\mu : S \rightarrow [0,1]\) such that \(\sum _{s\in S} \mu (s) = 1\). We denote the indicator function by \(\mathbf {1}_A\) which returns 1 for \(e \in A\) and 0 otherwise.

In Sect. 4, we apply two pseudo-random functions \( coinFlip \) and \( randSel \). These require an initialisation operation which takes a seed-value for a pseudo-random number generator and which returns implementations of both functions. The function \( coinFlip \) implements a biased coin flip and is defined for \(p \in [0,1]\) by \(\mathbb {P}( coinFlip (p) = \top ) = p\) and \(\mathbb {P}( coinFlip (p) = \bot ) = 1-p\). The function \( randSel \) takes a set as input and returns a single element of the set, whereby the element is chosen according to a uniform distribution, i.e. \(\forall e \in S: \mathbb {P}( randSel (S) = e) = \frac{1}{|S|}\).

We begin with an overview of the approach, discussing each of the steps briefly. Subsequently, we provide in-depth descriptions. For the remainder of this paper, we assume that we interact with an MDP \(\mathcal {M} = \langle Q,\varSigma ^{\mathrm {in}}, \varSigma ^\mathrm {out},q_0, \delta , L\rangle \) representing the SUT of which we only know \(\varSigma ^\mathrm {in}\). Basically, we try to find an optimal scheduler for satisfying a given reachability property \(\phi = F^{<k} \psi \) with the SUT \(\mathcal {M}\). For this purpose, we iteratively sample system traces, learn models from the traces and infer schedulers from the learned models. The inferred schedulers also serve to refine the sampling strategy. This process is also shown in Fig. 1. 2. For at most\( maxRounds \)rounds doCreate initial samples In the first step, we sample system traces by choosing input actions randomly according to a uniform distribution. Hence, we sample with a scheduler \(s_\mathrm {unif}\) defined as follows: \(\forall q \in Q, s_\mathrm {unif}: q \mapsto \mu _\mathrm {unif}(\varSigma ^\mathrm {in})\) where \(\forall i \in \varSigma ^\mathrm {in}: \mu _\mathrm {unif}: i \mapsto \frac{1}{|\varSigma ^\mathrm {in}|}\). Sampling is further controlled by the length probability \(p_l\) and by the batch size \(n_\mathrm {batch}\), i.e. the number of traces collected at once. These parameters also affect subsequent sampling. Additionally, we set a seed-value for the initialisation of pseudo-random functions.

As discussed in Sect. 3, we set \(p_l(j) = 0\) for \(j < k - 1\) if k is the step bound of the property we test for. This would not be necessary for learning but we generally apply this constraint. The length of suffixes, i.e. the trace extensions beyond k, follows a geometric distribution parameterised by \(p_\mathrm {quit} \in [0,1]\). Before each step, we stop with probability \(p_\mathrm {quit}\). Hence, the number of input steps |t| in a trace t is distributed according to \(p_l(|t|) = (1-p_\mathrm {quit})^{|t| - k + 1} p_\mathrm {quit}\) for \(|t| \ge k - 1\) and \(p_l(|t|) = 0\) otherwise. Both \(p_\mathrm {quit}\) and \(n_\mathrm {batch}\) must be supplied by the user. In the following, \(\mathcal {S}_i\) denotes the multiset of traces created by the \(i\mathrm{th}\) sampling step, and \(\mathcal {S}_\mathrm {all}\) refers to the multiset of all traces. Hence, \(\mathcal {S}_\mathrm {all}\) is initially set to \(\mathcal {S}_1\), containing \(n_\mathrm {batch}\) traces distributed according to \(\mathbb {P}_{\mathcal {M},s_\mathrm {unif}}^l\), collected by random testing.

Infer model In this step, we use IOAlergia [35, 36] to infer an MDP \({\mathcal {M}_\mathrm {h}}_i = \langle Q_\mathrm {h},\varSigma ^{\mathrm {in}}, {\varSigma ^\mathrm {out}}_\mathrm {h},{q_0}_\mathrm {h}, \delta _\mathrm {h}, L_\mathrm {h}\rangle \), from \(\mathcal {S}_\mathrm {all} = \bigcup _{j \le i} \mathcal {S}_j\), i.e. an approximate system model. Strictly speaking, we infer an MDP with a partial transition function, which we make input-complete with a function \( complete \). The transition function of an inferred MDP may be undefined for some state-input pair if there is no corresponding execution in \(\mathcal {S}_\mathrm {all}\). For this reason, we add transitions to a special state labelled with \( dontKnow \) for undefined state-input pairs. Once we enter that state, we cannot leave it. The label \( dontKnow \) is more generally a special output label, which is not part of the original output alphabet.

Formally, \(\mathcal {M}_\mathrm {h}' = \langle Q_\mathrm {h}',\varSigma ^{\mathrm {in}}, {\varSigma ^\mathrm {out}}_\mathrm {h}',{q_0}_\mathrm {h}', \delta _\mathrm {h}', L_\mathrm {h}'\rangle = \textsc {IOAlergia}{} (\mathcal {S}_\mathrm {all}, \epsilon _\mathrm {\textsc {Alergia}{}})\) and \({\mathcal {M}_\mathrm {h}}_i = complete (\mathcal {M}_\mathrm {h}')\) where \(Q_\mathrm {h} = Q_\mathrm {h}' \cup \{q_\mathrm {undef}\}\), \({\varSigma ^\mathrm {out}}_\mathrm {h} = {\varSigma ^\mathrm {out}}_\mathrm {h}' \cup \{ dontKnow \}\), with \( dontKnow \notin {\varSigma ^\mathrm {out}}_\mathrm {h}'\), \({q_0}_\mathrm {h}' = {q_0}_\mathrm {h}\), \(\delta _\mathrm {h} = \delta _\mathrm {h}' \cup \{(q_\mathrm {undef},i) \mapsto \mathbf {1}_{\{q_\mathrm {undef}\}} | i \in \varSigma ^\mathrm {in}\} \cup \{(q,i) \mapsto \mathbf {1}_{\{q_\mathrm {undef}\}} | q \in Q_\mathrm {h}', i \in \varSigma ^{\mathrm {in}}, \not \exists d: (q,i) \mapsto d \in \delta _\mathrm {h}' \}\) and \(L_\mathrm {h} = L_\mathrm {h}' \cup \{q_\mathrm {undef} \mapsto dontKnow \}\).

Following the terminology of active automata learning [4], we refer to \({\mathcal {M}_\mathrm {h}}_i\) as the current hypothesis. Input completion via \( complete \) is required by Definition 1, but does not affect the reachability analysis. We aim at maximising the probability of desired events, therefore generated schedulers will not choose to execute inputs leading to the state \(q_\mathrm {undef}\) labelled \( dontKnow \). This is due to the fact that once we reached \(q_\mathrm {undef}\), we have a probability of zero to observe anything other than \( dontKnow \) according to our hypothesis.

Reachability analysis Given the current hypothesis inferred in the last step, our implementation of the approach uses the Prism model checker [29] to derive a scheduler for satisfying the property \(\phi \). This is achieved by performing the following steps in a fully automated manner:These steps implicitly create an MDP \(\mathcal {M}_ steps \) containing \(k+1\) copies (q, st) of each state q of \({\mathcal {M}_\mathrm {h}}_i\), one for each value st the variable \( steps \) can take. Note that not all \(k+1\) copies of a state are reachable. If \(q'\) is reachable from q in \({\mathcal {M}_\mathrm {h}}_i\), then \((q',st+1)\) is reachable from (q, st) if \(st < k\). If \(st=k\), then \((q',st)\) is reachable from (q, st). The target states in \(\mathcal {M}_ steps \) for the unbounded reachability property \(\phi ' = F(\psi \wedge steps < k)\) are all (q, st) with \(L(q) \models \psi \) and \(st < k\). Furthermore, all (q, st) with \(st = k\) are non-target states from which we cannot reach target states, as required by the original bounded reachability property \(\phi \). Given \(\mathcal {M}_ steps \) and the unbounded reachability property \(\phi '\), Prism exports memoryless deterministic schedulers. These schedulers, however, do not define input choices for all states, but only for states reachable by the composition of scheduler and corresponding model. To account for cases with undefined scheduler behaviour, we use the notation \({s_\mathrm {h}}_i(q) = \bot \). It denotes that scheduler \({s_\mathrm {h}}_i\) does not define a choice for q.

Sample with scheduler.

Property-directed sampling with inferred schedulers aims at exploring parts of the system more thoroughly that have been identified as being relevant to the property. To avoid getting trapped in local minima, we also explore new paths by choosing actions randomly with probability \({p_\mathrm {rand}}_i\), where i corresponds to the current round. This probability is decreased in each round to explore more broadly in the beginning and focus on relevant parts in later rounds. Two parameters control \({p_\mathrm {rand}}_i\): \(p_\mathrm {start} \in [0,1]\) for the initial probability and \(c_\mathrm {change} \in [0,1]\) specifying an exponential decrease, i.e. \({p_\mathrm {rand}}_1 = p_\mathrm {start}\) and \({p_\mathrm {rand}}_{i+1} = c_\mathrm {change} \cdot {p_\mathrm {rand}}_i \) for \(i \ge 1\).

Basically, we execute both SUT and \({\mathcal {M}_\mathrm {h}}_i\) in parallel. The former ensures that we sample traces of the actual system while the latter is necessary because the inferred scheduler \({s_\mathrm {h}}_i\) is defined for \({\mathcal {M}_\mathrm {h}}_i\). Stated differently, we need to simulate the path taken by the SUT on the current hypothesis \({\mathcal {M}_\mathrm {h}}_i\). This enables selecting actions with \({s_\mathrm {h}}_i\). As \({\mathcal {M}_\mathrm {h}}_i\) is an approximation, two scenarios may occur in which we cannot use \({s_\mathrm {h}}_i\). In the following scenarios, we default to choose inputs randomly:The sampling is detailed in Algorithm 1. In addition to artefacts generated by other steps, such as the input-enabled hypothesis¹\({\mathcal {M}_\mathrm {h}}_i\) and the generated scheduler \({s_\mathrm {h}}_i\), sampling requires two auxiliary operations:Both operations are realised by a test adapter. Lines 1 to 5 of the algorithm collect traces by calling the \(\textsc {Sample}\) function and update \({p_\mathrm {rand}}_i\). The \(\textsc {Sample}\) function returns a single trace, which is created on-the-fly and initialised with the output produced upon resetting the SUT (line 7). Line 8 initialises the current model state. Afterwards, an input is chosen (lines 10 to 13). It is chosen randomly with probability \({p_\mathrm {rand}}_i\) or if we cannot determine an input (line 10 and 11). Otherwise, the input is selected with \({s_\mathrm {h}}_i\) (Line 13). We record the output of the SUT in response to the input and extend the trace in lines 14 and 15. The next two lines update the model state. In case, the SUT produces an output which is not allowed by the model, the new model state is undefined (second case in Line 17). This corresponds to the first scenario, in which we default to choose inputs randomly. Trace creation stops if the trace is long enough and if a probabilistic Boolean choice returns \( true \) (Line 9), i.e. the actual length follows a probability distribution. Note that lines 10 to 17 implement a randomised scheduler derived from \({s_\mathrm {h}}_i\). We will refer to this scheduler as \( randomised ({s_\mathrm {h}}_i)\). In the taxonomy of Utting et al. [51], property-directed sampling can be categorised as model-checking-based online testing with a combination of requirements coverage and random input-selection as criterion.

Evaluate. As a result of the reachability analysis, Prism calculates a probability of reaching \(\phi \). This probability, however, is derived from a learned model which is possibly inaccurate. Therefore, it may greatly differ from the actual probability of reachability with the SUT. To account for that, we evaluate the scheduler \(s_\mathrm {h} = {s_\mathrm {h}}_l\), where l is the last round we executed. We accomplish this by sampling a multiset of traces \(\mathcal {S}_\mathrm {eval}\), while generally selecting inputs with \(s_\mathrm {h}\), i.e. we execute Algorithm 1 with \({p_\mathrm {rand}}_i = 0\). Thereby, we implicitly sample traces from the DTMC induced by the composition of \(\mathcal {M}\) and \( randomised (s_\mathrm {h})\). Since this DTMC behaves entirely probabilistic, we can apply SMC. Hence, we estimate \(\mathbb {P}_{\mathcal {M}, randomised (s_\mathrm {h})}(\phi )\) by \(\hat{p}_{\mathcal {M},s_\mathrm {h}} = \frac{\left| \{s \in \mathcal {S}_\mathrm {eval} | s \models \phi \}\right| }{\left| \mathcal {S}_\mathrm {eval}\right| }\). To achieve a given error bound \(\epsilon _\mathrm {eval}\) with a given confidence \(1-\delta _\mathrm {eval}\), we compute the required number of samples \(\left| \mathcal {S}_\mathrm {eval}\right| = n_\mathrm {batch}\) based on a Chernoff bound [40], i.e. we apply (2). The estimation provides an approximate lower bound of the maximal reachability probability with the SUT. We consider \(\hat{p}_{\mathcal {M},s_\mathrm {h}}\) an approximate lower bound, because we know with confidence \(1{-}\delta _\mathrm {eval}\) that \(\max _s \mathbb {P}_{\mathcal {M},s}(\phi )\) is at least as large as \(\hat{p}_{\mathcal {M},s_\mathrm {h}}-\epsilon _\mathrm {eval}\).

Check early stop We have observed that the performance of schedulers usually increases with the total amount of available data. Probability estimations derived with intermediate schedulers showed that schedulers generated in later rounds tend to perform better than those generated in earlier. However, we have also seen fluctuations in these estimations over time, i.e. some schedulers may perform worse than schedulers generated in previous rounds. With increasing number of rounds these fluctuations generally diminish and the estimations converge. Intuitively, this can be explained by the influence of \({p_\mathrm {rand}}_{i}\) in Algorithm 1, which controls the probability of selecting random inputs and decreases over time. As this probabilities \({p_\mathrm {rand}}_{i}\) approaches zero, we will almost always select inputs with generated schedulers. This will generally only increase the confidence in parts of the system we have already explored, but will not explore new parts and therefore new schedulers are likely to show similar behaviour to previous ones.

Based on these observations, we developed a heuristic check for convergence. If it detects convergence, we stop the iteration early before executing \( maxRounds \) rounds. Two simpler checks actually form the basis of the heuristic. The first, called \(\textsc {similarSched}\), basically compares the scheduler generated in the current round to the scheduler from the previous round and returns \( true \) if both behave similarly. The second check, called \(\textsc {conv}\) builds upon the first and reports convergence if we detect statistically similar behaviour via \(\textsc {similarSched}\) in multiple consecutive rounds. The rationale behind this is that schedulers should behave alike after convergence. We check for similarity rather than for equivalence because there may be several optimal inputs in a state and slight variations in transition probabilities in the inferred models may lead to the different choices of inputs. Furthermore, we can compare schedulers during sampling by comparing whether they would choose the same inputs. This gives us a large number of events as basis for our decision and does not require additional sampling.

The convergence check has three parameters: \(\alpha _\mathrm {conv}\) controlling the confidence level, an error bound \(\epsilon _\mathrm {conv}\), and a bound on the number of rounds \(r_\mathrm {conv}\). The first two parameters control a statistical test which checks whether two schedulers behave similarly. For this test, we consider Bernoulli random variables \(E_i\) for \(i \in [2.\,.\, maxRounds ]\). \(E_i\) is equal to one if two consecutive schedulers \({s_\mathrm {h}}_i\) and \({s_\mathrm {h}}_{i-1}\) behave equivalently, i.e. choose the same input in some state, and zero otherwise. Let \(p_{E_i}\) be the success probability, the probability of \(E_i\) being equal to one. We observe samples of \(E_i\) in Line 13 of Algorithm 1. Each time we choose an input i with \({s_\mathrm {h}}_i\), we also determine which input \(i'\) the previous scheduler \({s_\mathrm {h}}_{i-1}\) would have chosen. We record a positive outcome if \(i = i'\) and a negative outcome otherwise.

Let \(\hat{p}_{E_i}\) be the relative number of positive outcomes, which is an estimate of \(p_{E_i}\). If \(p_{E_i}\) is equal to one, then both schedulers behave equivalently, they always choose the same input. Consequently, we test whether \(\hat{p}_{E_i}\) is close to one. We test the null hypothesis \(H_0: p \le 1-\epsilon _\mathrm {conv}\) against \(H_1: p > 1-\epsilon _\mathrm {conv}\) with a confidence level of \(1-\alpha _\mathrm {conv}\). The hypothesis \(H_1\) denotes that the compared schedulers choose the same inputs in most of the cases. Let \(\textsc {similarSched}(\alpha _\mathrm {conv},\epsilon _\mathrm {conv}, i)\) be the result of this test in round i, which is \( true \) if \(H_0\) is rejected and \( false \) otherwise.

Finally, we can formulate the complete convergence check \(\textsc {conv}(\alpha _\mathrm {conv},\epsilon _\mathrm {conv}, i)\). It returns \( true \) in round i if \(r_\mathrm {conv}\) consecutive calls of \(\textsc {similarSched}\) returned \( true \), i.e. \(\textsc {conv}(\alpha _\mathrm {conv},\epsilon _\mathrm {conv}, i) = \bigwedge ^i_{j=i-r_\mathrm {conf}+1} \textsc {similarSched}(\alpha _\mathrm {conv},\epsilon _\mathrm {conv}, j)\).

Note that \({p_\mathrm {rand}}_{i}\) implicitly affects the convergence check. We collect samples of \(E_i\) in Line 13 of Algorithm 1, thus large \({p_\mathrm {rand}}_{i}\), cause Line 13 to be executed infrequently. As a result, sample sizes of \(E_i\) are small. This influence on the convergence check is beneficial because schedulers are more likely to improve if \({p_\mathrm {rand}}_{i}\) is large, as new parts of the system may be explored via frequent random steps.

While the check introduces further parameters, it may simplify the application of the approach in scenarios where we have little knowledge about the system at hand. In such cases, it may be difficult to find a reasonable choice for the number of rounds \( maxRounds \). With this heuristic, it is possible to choose \( maxRounds \) conservatively, but stop early once convergence is detected. However, it may also impair results, if convergence is detected too early.

Generally, Mao et al. [36] showed convergence in the large sample limit for IOAlergia. However, the sampling mechanism needs to ensure that sufficiently many executions of all inputs in all states are observed. This is also discussed in [35], which states that IOAlergia requires a fair schedulers, one that chooses each input infinitely often. The uniformly randomised \(s_\mathrm {unif}\) satisfies this requirement. As a result, we have convergence in the limit, if we perform only a single round of inference, in which we sample with \(s_\mathrm {unif}\).

Property-directed sampling favours certain inputs with increasing number of rounds, but it also selects random inputs with probability \({p_\mathrm {rand}}_i\) in round i. If we ensure that \({p_\mathrm {rand}}_i\) is always non-zero, we will select all inputs infinitely often in an infinite number of rounds. Therefore, the inferred models will converge to the true model (up to bisimulation equivalence) and the inferred schedulers will converge to the optimal scheduler.

Another way to approach convergence is to follow a hybrid approach, by collecting traces via property-directed sampling and via uniform sampling in parallel. Uniform sampling ensures that all inputs are executed sufficiently often, which entails convergence. Property-directed sampling explores parts of the system, identified to be relevant, which increases the confidence in the correct inference of those parts. As a result, intermediate schedulers are more likely to perform well.

Hence, we have convergence in the limit under certain assumptions. In practice, i.e. when learning from limited data, uniform schedulers are likely to be insufficient, if events occur only after long interaction scenarios. If events occur rarely in the sampled system traces, then it is unlikely that the part modelling those events is accurately learned. Active learning, as described by Chen and Nielsen [13], addressed this issue by guiding sampling so as to reduce the uncertainty in the learned model. Our approach similarly guides sampling, but with the aim at reducing uncertainty along traces, which are likely to satisfy a reachability property.

As noted above, we have seen that the inferred schedulers usually converge to a scheduler, which may not be globally optimal, though. We also performed experiments with the outlined hybrid approach to avoid getting trapped in local maxima, by collecting half the system traces through uniform sampling. While it showed favourable performance in a few cases, the incremental approach generally produced better results with the same number of samples. Therefore, we will not discuss experiments with the hybrid approach.

Apart from convergence, it may not always be necessary to find a (near-) optimal scheduler. A requirement may state that the probability of reaching an erroneous state must be smaller than some p. Once we found and evaluated a scheduler \(s_\mathrm {h}\) such that the estimation \(\hat{p}_{\mathcal {M},s_\mathrm {h}} \ge p\), we basically show with some confidence that the requirement is violated. Such a requirement could be the basis of another stopping criterion. If in round i, a sufficiently large number of the sampled traces \(\mathcal {S}_i\) reaches an erroneous state, we may decide to evaluate the corresponding scheduler \({s_\mathrm {h}}_{i-1}\). We could then stop if \(\hat{p}_{\mathcal {M},{s_\mathrm {h}}_{i-1}} \ge p\) and continue otherwise.

Application and choice of parameters We will now briefly discuss the choice of parameters taking our findings into account. A summary of all parameters along with a concise description is given by Table 1.

The product \(n_\mathrm {s} = n_\mathrm {batch} \cdot maxRounds \) defines the overall maximum number of samples for inference, thus it could be chosen as large as the testing/simulation budget permits. Increasing \( maxRounds \) while fixing \(n_\mathrm {s}\) increases the time required for learning and model checking. Intuitively, it improves accuracy as well, as sampling is more frequently adjusted towards the considered property. For the systems examined in Sect. 5, values in the range between 50 and 200 led to reasonable accuracy while incurring acceptable runtime overhead. Runtime overhead is the time spent learning and model checking, as opposed to the time spent doing actual testing, i.e. (property-directed) sampling. The convergence check takes three parameters as input for which we identified well-suited default parameters. To ensure high confidence for the statistical test, we set \(\alpha _\mathrm {conv} = 0.01\). Since schedulers should choose the same input in most cases, \(\epsilon _\mathrm {conv}\) should be small, but greater than zero to allow for some variation. In our experiments, we set it to \(\epsilon _\mathrm {conv} = 0.01\) and we set \(r_\mathrm {conv} = 6\). More conservative choices would be possible at the expense of performing additional rounds.

The value of \(p_\mathrm {start}\) should generally be larger than 0.5, while \(c_\mathrm {change}\) should be close to 1. This ensures broad exploration in the beginning and more directed exploration afterwards. Finally, the choice of \(p_\mathrm {quit}\) depends on the simulation budget and the number of inputs. If there is a large number of inputs, it may be highly improbable to reach certain states within a small number test steps via random testing. Consequently, we should allow for the execution of long tests, in order to reach states requiring complex combinations of inputs. Domain knowledge may also aid in choosing this parameter. If we, e.g., expect a long initialisation phase, \(p_\mathrm {quit}\) should be low to ascertain that we reach states following the initialisation.

We evaluated our approach on five case studies from the area of automata learning, control policy synthesis, and probabilistic model-checking. For the first case study, we created our own model of the slot machine described by Mao et al. [36] in the context of learning MDPs. Two case studies consider models of network protocols enhanced with stochastic failures. For that, we transformed deterministic Mealy-machine models as detailed below. The model used in the fourth case study is inspired by the gridworld example, for which Fu and Topcu synthesised control strategies [23]. Finally, we generate schedulers for a consensus protocol [6] which serves as a benchmark in probabilistic model-checking. We discussed the experiments involving the slot machine and the network protocol models before [3]. New additions in this extended version are experiments with the gridworld example, the consensus protocol, and experiments with the convergence check. Note that due to changes of the implementation, measurement result may differ from those in [3].

Adding stochastic failures Deterministic Mealy-machines serve as the basis for two case studies. These Mealy machines are results from previous learning experiments [20, 49] and model communication protocols. Basically, we simulate stochastic failures by adding outputs represented by the label \( crash \). These occur with a predefined probability instead of the correct output. Upon such a failure, the system is reset. We implemented this by transforming the Mealy machines as follows:This simulates stochastic failures of outputs belonging to a set \( Crashes \). Instead of producing the correct outputs, we output \( crash \) and reach state \(q_\mathrm {cr}\) with a certain probability. With the same probability we stay in this state and otherwise we reset the system to \(q_0\) after the crash.

Measurement setup and criteria We have complete information about all models. This allows us to compare our results to optimal values. Nevertheless, for the evaluation we treat the systems as black boxes. The state spaces of the models without step-counter variables for bounded reachability are of sizes 471 (slot machine), 63 (MQTT), 157 (TCP), 35 (gridworld), and 272 (consensus protocol), respectively. For each of these systems, we identified an output relevant to the application domain and applied the presented technique to reach states emitting this output with varying numbers of steps. The slot machine grants prizes and we generated strategies to observe the rarest prize. Using the steps discussed above, we seeded stochastic failures into the MQTT and TCP models, which we tried to reach. The gridworld we used in the evaluation contains a dedicated goal location that served as a as reachability objective. In case of the consensus protocol, we generated strategies to finish the protocol, i.e. reach consensus, with high probability.

For a black-box MDP \(\mathcal {M}\) and a reachability property \(\phi \), we compare four approaches to find schedulers s for \(\mathbb {P}_{\mathcal {M},s}(\phi )\):Furthermore, let \(s_\mathrm {opt} = {{\,\mathrm{\arg \!\max }\,}}_s \mathbb {P}_{\mathcal {M},s}(\phi )\) be the optimal scheduler. This is the optimal scheduler obtained for the generating model \(\mathcal {M}\). As the most important measure of quality, we compare estimates of \(\mathbb {P}_{\mathcal {M},s}(\phi )\) to the maximal probability \(\mathbb {P}_{\mathcal {M},s_\mathrm {opt}}(\phi )\). We consider a scheduler s to be near optimal, if the estimate \(\hat{p}_{\mathcal {M},s}\) of \(\mathbb {P}_{\mathcal {M},s}(\phi )\) derived via SMC is approximately equal to \(\mathbb {P}_{\mathcal {M},s_\mathrm {opt}}(\phi )\), i.e. \(|\hat{p}_{\mathcal {M},s} - \mathbb {P}_{\mathcal {M},s_\mathrm {opt}}(\phi )| \le \epsilon \), for an \(\epsilon > 0\). In the following, we use \(\epsilon = \epsilon _\mathrm {eval}\) for deciding near optimality, where \(\epsilon _\mathrm {eval}\) is the error bound of the applied Chernoff bound (2).

We balance the number of test steps for the incremental and the monolithic approach by executing the same number of tests. As a result, the simulation costs for executing tests is approximately the same. Since the incremental approach requires model learning and model checking in each round, it will also require more computation time than the monolithic approach. While our main focus is on evaluating with respect to the achieved probability estimation, we will briefly discuss computation cost at the end of the section.

We also briefly discuss estimations based on model checking of inferred models \(\mathcal {M}_\mathrm {h}\), i.e. \(\max _{s} \mathbb {P}_{\mathcal {M}_\mathrm {h},s}(\phi )\) calculated by Prism [29]. These estimations have also been discussed by Mao et al. [36]. They noted that estimations may differ significantly from optimal values in some cases, but generally represent good approximations.

Implementation and settings We base the evaluation on our Java implementation of the described technique which can be found at [43]. All experiments were performed with a Lenovo Thinkpad T450 with 16 GB RAM and an Intel Core i7-5600U CPU operating at 2.6 GHz and running Xubuntu Linux 18.04. The systems were modelled with Prism [29]. Prism served three purposes:

Simulation, as well as sampling, is controlled by probabilistic choices. To ensure reproducibility, we used fixed seeds for pseudo-random number generators controlling the choices. All experiments were run with 20 different seeds and we discuss statistics derived from 20 such runs. For the evaluation of schedulers, we applied a Chernoff bound with \(\epsilon _\mathrm {eval}=0.01\) and \(\delta _\mathrm {eval}=0.01\). In contrast to the conference version of this paper [3], we used a fixed significance level for the compatibility check of IOAlergia, by setting \(\epsilon _\mathrm {\textsc {Alergia}{}} = 0.5\), a value also used by Mao et al. [36]. They noted that IOAlergia is generally robust with respect to the choice of this value, but we found that our approach benefits from a larger \(\epsilon _\mathrm {\textsc {Alergia}{}}\), which causes fewer state merges and consequently larger models. Put differently, our approach benefits from more conservative state merging. As noted in Sect. 4, we aim at ensuring broad exploration in the beginning and property-directed exploration in later rounds. Therefore, we set \(p_\mathrm {start}=0.75\) and \(c_\mathrm {change} = 0.95\) unless otherwise noted. We set the convergence-check parameters in all experiments as suggested in Sect. 4: \(\alpha _\mathrm {conv} = 0.01\), \(\epsilon _\mathrm {conv} = 0.01\), and \(r_\mathrm {conv} = 6\). Table 2 summarises parameter settings that apply in general.

We presented an approach to infer near-optimal schedulers for reachability objectives of MDPs. To our knowledge, it is the first such approach to be applicable in a purely black-box setting, where only the input interface is known. This is accomplished by incrementally refining the knowledge about the system, via model inference and based on that property-directed exploration of the system. Section 5 presents promising results, showing that near-optimality can be achieved.

Therefore, we plan to investigate this approach further and extend it. As a first step, we are currently evaluating the method on more case studies. In order to be able to examine more complex systems, we are planning to work on compositional verification. That is, we are investigating how to benefit from decomposition, as opposed to treating composed systems as large monolithic systems. We are also studying the applicability in different testing scenarios. In a testing context, e.g., Nachmanson et al. [38] discussed strategies for bounded reachability games, but with a given model.

Furthermore, non-functional properties like execution time could be considered. For that, we need to devise a model-inference technique which considers both non-deterministic choice of inputs and (continuous) time. Current approaches for probabilistic timed systems do not account for non-determinism of this form [36, 52]. If we had such a technique, we could, e.g., use Prism with the digital clocks engine [29] or Uppaal Stratego [15, 16] to infer schedulers. Another possible extension would be to consider more general properties than reachability. This would require replacing Prism’s scheduler generation in our approach. In conclusion, we believe that our results are encouraging and that there are many promising directions for future research.