A cartesian-closed category for higher-order model checking

• Published in: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
• Main Authors: Hofmann, Martin, Ledent, Jeremy
• Other Authors: Institut für Informatik München/Munich (LMU), Ludwig Maximilian University Munich = Ludwig Maximilians Universität München (LMU), Laboratoire d'informatique de l'École polytechnique Palaiseau (LIX), École polytechnique (X), Institut Polytechnique de Paris (IP Paris)-Institut Polytechnique de Paris (IP Paris)-Centre National de la Recherche Scientifique (CNRS)
• Format: Conference Object
• Language: English
• Published: HAL CCSD 2017
• Subjects: [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]; Iceland
• Online Access: https://hal.science/hal-04470696; https://hal.science/hal-04470696/document; https://hal.science/hal-04470696/file/buchi_ho.pdf; https://doi.org/10.1109/lics.2017.8005120

International audience In previous work we have described the construction of an abstract lattice from a given B üchi 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 ω-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.