In higher-order model-checking (HOMC), functional programs are represented as higher-order recursion schemes (HORS), a kind of grammar with parameters which can be functions. These grammars generate infinite trees, over which we want to check formulas of monadic second-order logic (MSO). This problem is decidable, as proved first by Ong in 2006, and then by many others including Kobayashi and Ong (2009) whose approach use intersection types. It turns out that linear logic is a powerful and enlightening tool to reason about HOMC, as shown by Grellois and Melliès in the last years.

In general, the complexity of the HOMC problem is n-EXPTIME, where n is the order of the HORS of interest. In this talk, we explain that we can refine this complexity measure: motivated by linear logic, we introduce *linear* HORS and a linear-nonlinear model of automaton checking fragments of MSO. We then show that HOMC is in fact n-EXPTIME complete for n the *linear* order of the linear HORS generating the tree of interest. We believe that this explains why HOMC, in spite of its huge theoretical complexity, has been successfully used in practice by Kobayashi's team.

This linear framework allows to reprove in a much simpler way three existing results extending the usual HOMC problem, and notably to deal with call-by-value programs in a smooth way (the usual HOMC approach considering call-by-name).

This is joint work with Pierre Clairambault and Andrzej Murawski.