Proving Non-Inclusion of B\"uchi Automata based on Monte Carlo Sampling

TL;DR

This paper introduces IMC^2, a Monte Carlo sampling-based algorithm for efficiently proving non-inclusion of B"uchi automata, enabling practical verification by balancing proof and counterexample search.

Contribution

The paper presents IMC^2, a novel Monte Carlo method for non-inclusion proof in B"uchi automata, combining probabilistic sampling with formal guarantees.

Findings

IMC^2 effectively finds counterexamples faster than traditional methods.

The algorithm provides probabilistic guarantees on non-inclusion proofs.

Experimental results demonstrate IMC^2's speed and reliability.

Abstract

The search for a proof of correctness and the search for counterexamples (bugs) are complementary aspects of verification. In order to maximize the practical use of verification tools it is better to pursue them at the same time. While this is well-understood in the termination analysis of programs, this is not the case for the language inclusion analysis of B\"uchi automata, where research mainly focused on improving algorithms for proving language inclusion, with the search for counterexamples left to the expensive complementation operation. In this paper, we present $\mathsf{IMC}^2$, a specific algorithm for proving B\"uchi automata non-inclusion $\mathcal{L}(\mathcal{A}) \not\subseteq \mathcal{L}(\mathcal{B})$, based on Grosu and Smolka's algorithm $\mathsf{MC}^2$ developed for Monte Carlo model checking against LTL formulas. The algorithm we propose takes $M = \lceil \ln \delta / \ln (1-\epsilon) \rceil$ random lasso-shaped samples from $\mathcal{A}$ to decide whether to reject the hypothesis $\mathcal{L}(\mathcal{A}) \not\subseteq \mathcal{L}(\mathcal{B})$, for given error probability $\epsilon$ and confidence level $1 - \delta$. With such a number of samples, $\mathsf{IMC}^2$ ensures that the probability of witnessing $\mathcal{L}(\mathcal{A}) \not\subseteq \mathcal{L}(\mathcal{B})$ via further sampling is less than $\delta$, under the assumption that the probability of finding a lasso counterexample is larger than $\epsilon$. Extensive experimental evaluation shows that $\mathsf{IMC}^2$ is a fast and reliable way to find counterexamples to B\"uchi automata inclusion.