The Model Checking Problem for Prefix Classes of Second-Order Logic: A Survey

DOI10.1007/978-3-642-15025-8_13zbMath1287.68107OpenAlexW1570464944WikidataQ59259582 ScholiaQ59259582MaRDI QIDQ3586006

Thomas Schwentick, Thomas Eiter, Georg Gottlob

Publication date: 3 September 2010

Published in: Fields of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-15025-8_13

zbMATH Keywords

monadic second-order logicsurvey papermodel checkingsecond-order logicregular languagesfinite model theoryGurevich's classifiability theorem

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Model theory of finite structures (03C13)

Uses Software

• MONA
• XPath
• Lixto

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Descriptive characterizations of computational complexity
• The quantifier structure of sentences that characterize nondeterministic time complexity
• The polynomial-time hierarchy
• A descriptive characterisation of even linear languages
• Query automata over finite trees
• Logic, semigroups and automata on words
• Regular languages defined with generalized quantifiers
• Normal forms for second-order logic over finite structures, and classification of NP optimization problems
• Tree acceptors and some of their applications
• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
• Monadic datalog over finite structures of bounded treewidth
• Weak Second‐Order Arithmetic and Finite Automata
• Some computational aspects of circumscription
• Universal quantifiers and time complexity of random access machines
• On the presence of disjoint subgraphs of a specified type
• Decision Problems of Finite Automata Design and Related Arithmetics
• Existential second-order logic over strings
• Automated Reasoning
• STACS 2004
• Monadic datalog and the expressive power of languages for Web information extraction
• Existential second-order logic over graphs
• Generalized finite automata theory with an application to a decision problem of second-order logic
• A Linear-Time Algorithm for Finding Tree-Decompositions of Small Treewidth

This page was built for publication: The Model Checking Problem for Prefix Classes of Second-Order Logic: A Survey