The model checking problem for prefix classes of second-order logic: a survey

In this paper, we survey results related to the model checking problem for second-order logic over classes of finite structures, including word structures (strings), graphs, and trees, with a focus on prefix classes, that is, where all quantifiers (both first- and second-order ones) are at the beginning of formulas. A complete picture of the prefix classes defining regular and non-regular languages over strings is known, which nearly completely coincides with the tractability frontier; some complexity issues remain to be settled, though. Over graphs and arbitrary relational structures, the tractability frontier is completely delineated for the existential second-order fragment, while it is less explored for trees. Besides surveying some of the results, we mention some open issues for research.