Two-automaton emptiness check in Spot

From LRDE

Abstract

Spot is library that handles -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 to know if intersects . When it is implemented as , the computation of the product throttles the amout of acceptance sets A and B can use. We propose a new function which does the emptiness check of 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.