Antichains for the Automata-Based Approach to Model-Checking

TL;DR

This paper introduces antichain algorithms for automata-based model checking, significantly improving efficiency in solving universality, language inclusion, and emptiness problems for nondeterministic and alternating Buechi automata.

Contribution

It presents novel antichain algorithms leveraging simulation pre-orders to efficiently evaluate fixed points in automata complementation, outperforming standard methods on challenging instances.

Findings

Algorithm outperforms standard methods on difficult automaton instances

Significant speedup in universality checking for nondeterministic Buechi automata

Effective evaluation of fixed points using simulation pre-orders

Abstract

We propose and evaluate antichain algorithms to solve the universality and language inclusion problems for nondeterministic Buechi automata, and the emptiness problem for alternating Buechi automata. To obtain those algorithms, we establish the existence of simulation pre-orders that can be exploited to efficiently evaluate fixed points on the automata defined during the complementation step (that we keep implicit in our approach). We evaluate the performance of the algorithm to check the universality of Buechi automata using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, our algorithm outperforms the standard ones by several orders of magnitude.