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. © 2010 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Eiter, T., Gottlob, G., & Schwentick, T. (2010). The model checking problem for prefix classes of second-order logic: A survey. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6300 LNCS, pp. 227–250). https://doi.org/10.1007/978-3-642-15025-8_13
Mendeley helps you to discover research relevant for your work.