Abstract interpretation from Büchi automata
Martin O. Hofmann, Wei Chen · 2014
We describe the construction of an abstract lattice from a given Buchi automata. The abstract lattice is finite and has the following key properties. (i) There is a Galois connection between it and the (infinite) lattice of languages of finite and infinite words over a given alphabet. (ii) The abstraction is faithful with respect to acceptance by the automaton. (iii) Least fixpoints and ω-iterations (but not in general greatest fixpoints) can be computed on the level of the abstract lattice.