Compositional higher-order model checking via ω -regular games over Böhm trees
Takeshi Tsukada, C.-H. Luke Ong · 2014
We introduce type-checking games, which are ω-regular games over Böhm trees, determined by a type of the Kobayashi-Ong intersection type system. These games are a higher-type extension of parity games over trees, determined by an alternating parity tree automaton. However, in contrast to these games over trees, the "game boards" of our type-checking games are composable, using the composition of Böhm trees. Moreover the winner (and winning strategies) of a composite game is completely determined by the respective winners (and winning strategies) of the component games.