A Cartesian-Closed Category For Higher-Order Model Checking

In previous work we have described the construction of an abstract lattice from a given Bfichi automaton. The abstract lattice is finite and has the following key properties. (i) There is a Galois insertion between it and the 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 w-iterations (but not in general greatest fixpoints) can be computed on the level of the abstract lattice.This allows one to decide whether finite and infinite traces of first-order recursive boolean programs are accepted by the automaton and can further be used to derive a type-and-effect system for infinitary properties.In this paper, we show how to derive from the abstract lattice a cartesian-closed category with fixpoint operator in such a way that the interpretation of a higher-order recursive program yields precisely the abstraction of its set of finite and infinite traces and thus provides a new algorithm for the higher-order model checking problem for trace properties.All previous algorithms for higher-order model checking [2], [16] work inherently on arbitrary tree properties and no apparent simplification appears when instantiating them with trace properties. The algorithm presented here, while necessarily having the same asymptotic complexity, is considerably simpler since it merely involves the interpretation of the program in a cartesian-closed category.The construction of the cartesian closed category from a lattice is new as well and may be of independent interest.