# Probabilistic Black-Box Checking via Active MDP Learning

arXiv: https://arxiv.org/abs/2308.07930 · HTML: https://mlsanity.com/paper/2308.07930/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 40 references that are in the map.
- First posted on arXiv 15 Jul 2023.

## Builds on (most cited first, 6 of 6)

- [Verification of Markov Decision Processes using Learning Algorithms](https://mlsanity.com/paper/1402.2967/) (2014)
- [Falsification of Cyber-Physical Systems with Robustness-Guided Black-Box Checking](https://mlsanity.com/paper/2005.02126/) (2020)
- [L*-Based Learning of Markov Decision Processes (Extended Version)](https://mlsanity.com/paper/1906.12239/) (2019)
- [Smart Sampling for Lightweight Verification of Markov Decision Processes](https://mlsanity.com/paper/1409.2116/) (2014)
- [Scalable Verification of Markov Decision Processes](https://mlsanity.com/paper/1310.3609/) (2013)
- [Efficient Black-Box Checking via Model Checking with Strengthened Specifications](https://mlsanity.com/paper/2109.04656/) (2021)

## Built on by (most cited first, 1 of 1)

- [Extending AALpy with Passive Learning: A Generalized State-Merging Approach](https://mlsanity.com/paper/2506.06333/) (2025)

## Abstract (arXiv)

We introduce a novel methodology for testing stochastic black-box systems, frequently encountered in embedded systems. Our approach enhances the established black-box checking (BBC) technique to address stochastic behavior. Traditional BBC primarily involves iteratively identifying an input that breaches the system's specifications by executing the following three phases: the learning phase to construct an automaton approximating the black box's behavior, the synthesis phase to identify a candidate counterexample from the learned automaton, and the validation phase to validate the obtained candidate counterexample and the learned automaton against the original black-box system. Our method, ProbBBC, refines the conventional BBC approach by (1) employing an active Markov Decision Process (MDP) learning method during the learning phase, (2) incorporating probabilistic model checking in the synthesis phase, and (3) applying statistical hypothesis testing in the validation phase. ProbBBC uniquely integrates these techniques rather than merely substituting each method in the traditional BBC; for instance, the statistical hypothesis testing and the MDP learning procedure exchange information regarding the black-box system's observation with one another. The experiment results suggest that ProbBBC outperforms an existing method, especially for systems with limited observation.