Title:Tensorial logic with colours and higher-order model checking

Abstract:We revisit the type-theoretic account of higher-order model-checking by Kobayashi and Ong in the light of linear logic and of its relational semantics. We start from the well-known fact that every higher-order recursion scheme (HORS) on a given signature may be seen after Church encoding as a lambda Y-term of a given second-order type. We then observe that the type of this encoding is dual to the one of alternating tree automata A on the same signature. This duality simply reflects the fact that a tree automaton is eventually designed to interact with a tree. Guided by this fundamental intuition, we show how to express inside the relational semantics of linear logic the set of states accepted by an alternating tree automaton A on the infinite tree generated by a HORS G of the same signature. We establish that it coincides with the composite <G|A> of their relational interpretations. We then extend this result to the more difficult case of alternating parity tree automata (APT). A meticulous analysis of the Kobayashi-Ong type system leads us to the interesting discovery that the colors of APT behave exactly as a parametric version of the exponential modality of linear logic. This leads us to an infinitary and colored extension of tensorial logic and of its relational semantics. We obtain the following structure theorem, which clarifies the semantic nature of higher-order model-checking: every HORS G and APT A on the same signature can be interpreted in the coloured relational semantics in such a way that the interaction <G|A> of their interpretations computes the set of accepting states of A on the infinite tree generated by G. To conclude, we briefly explain how this connection with linear logic and its relational semantics enables us to recover in a clean and conceptual way the original decidability result of MSO on infinite trees generated by HORS.