Papers › Proving Non-Inclusion of Büchi Automata based on Monte Carlo Sampling
Proving Non-Inclusion of Büchi Automata based on Monte Carlo Sampling
Yong Li, Andrea Turrini, Xuechao Sun, Lijun Zhang
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 𝖨𝖬𝖢², a specific algorithm for proving B\"uchi automata non-inclusion ℒ(𝒜) ⊈ℒ(ℬ), based on Grosu and Smolka's algorithm 𝖬𝖢² developed for Monte Carlo model checking against LTL formulas. The algorithm we propose takes M = ⌈lnδ/ ln(1-ϵ) ⌉ random lasso-shaped samples from 𝒜 to decide whether to reject the hypothesis ℒ(𝒜) ⊈ℒ(ℬ), for given error probability ϵ and confidence level 1 - δ. With such a number of samples, 𝖨𝖬𝖢² ensures that the probability of witnessing ℒ(𝒜) ⊈ℒ(ℬ) via further sampling is less than δ, under the assumption that the probability of finding a lasso counterexample is larger than ϵ. Extensive experimental evaluation shows that 𝖨𝖬𝖢² is a fast and reliable way to find counterexamples to B\"uchi automata inclusion.
Code
Repository list and official/mentioned flags are the archive's, frozen 2025-07-28. Reachability, where shown, is from one Syntology probe window (2026-09-16 to 2026-09-18); repositories not probed show nothing. GitHub stars are not tracked.
Code Syntology ran Syntology
Not run by Syntology. Nothing on this page verifies that the listed code works.
Results from the paper archive 2025-07-28
No leaderboard rows for this paper in the archive.
Report a problem or propose a change · a person checks every report against the paper or source before anything changes; decisions are listed on /corrections