# Two-automaton emptiness check in Spot

## Abstract

Spot is library that handles ${\displaystyle \omega }$-automata whose acceptance conditions are expressed with at most 32 acceptance sets. Since the acceptance condition of the product of two automata has to use the sum of their setswe cannot produce a product whose operands use more than 32 sets in total. A typical operation on automata is to compute ${\displaystyle L(A\times B)\neq \emptyset }$ to know if ${\displaystyle L(A)}$ intersects ${\displaystyle L(B)}$. When it is implemented as ${\displaystyle empty(product(A,B))}$, the computation of the product throttles the amout of acceptance sets A and B can use. We propose a new function ${\displaystyle empty(A,B)}$ which does the emptiness check of ${\displaystyle A\times B}$ without actually building an automaton and hence without any limit on the acceptance conditions. The ltlcross tool can now compare automata using a total of more than 32 acceptance sets.