When dealing with finite state properties, it is usual to have some finite algebraic structures (e.g. finite monoids in the case of finite state automata on strings) that represent those properties. When dealing with logical properties of programs that are computed by finite state automaton, the question of what is an "adequate" finite algebraic structure arises. Having such a structure would entail a sort of modularity in program verification, but it also gives some strong understanding of how the properties can be checked.

In the context of higher-order verification, programs are models as lambda-terms and it is natural to think about denotational domains as a possible candidate. Finitary Scott domains only capture very simple properties of the Bohm trees generated by higher-order programs. This talk will illustrate how to enrich Scott domains so that they can capture wider classes of finite state properties.

(joint work with Igor Walukiewicz)