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

DOI10.1007/978-3-642-15025-8_13MaRDI QIDQ3586006zbMATH OpenOpenAlexWikidataFDO

Authors Thomas Eiter, Georg Gottlob, Thomas Schwentick

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

survey paperfinite model theorymodel checkingmonadic second-order logicregular languagessecond-order logicGurevich's classifiability theorem

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1688350
• Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic
• First-order and monadic second-order model-checking on ordered structures
• The Complexity of Model Checking for Intuitionistic Logics and Their Modal Companions
• The Complexity of Model Checking Higher-Order Fixpoint Logic
• Mathematical Foundations of Computer Science 2005
• On the model-checking of monadic second-order formulas with edge set quantifications
• Model checking in the modal -calculus and generic solutions

Cites work

• scientific article; zbMATH DE number 4028925 (Why is no real title available?)
• scientific article; zbMATH DE number 3474957 (Why is no real title available?)
• scientific article; zbMATH DE number 1223631 (Why is no real title available?)
• scientific article; zbMATH DE number 1254648 (Why is no real title available?)
• scientific article; zbMATH DE number 618821 (Why is no real title available?)
• scientific article; zbMATH DE number 709536 (Why is no real title available?)
• scientific article; zbMATH DE number 1142314 (Why is no real title available?)
• scientific article; zbMATH DE number 2079028 (Why is no real title available?)
• scientific article; zbMATH DE number 2087211 (Why is no real title available?)
• scientific article; zbMATH DE number 1884381 (Why is no real title available?)
• scientific article; zbMATH DE number 803291 (Why is no real title available?)
• scientific article; zbMATH DE number 3368555 (Why is no real title available?)
• scientific article; zbMATH DE number 965572 (Why is no real title available?)
• A Linear-Time Algorithm for Finding Tree-Decompositions of Small Treewidth
• A descriptive characterisation of even linear languages
• Automated Reasoning
• Decision Problems of Finite Automata Design and Related Arithmetics
• Descriptive characterizations of computational complexity
• Existential second-order logic over graphs: charting the tractability frontier
• Existential second-order logic over strings
• Generalized finite automata theory with an application to a decision problem of second-order logic
• Logic, semigroups and automata on words
• Monadic Datalog and the expressive power of languages for web information extraction
• Monadic Datalog over finite structures of bounded treewidth
• Normal forms for second-order logic over finite structures, and classification of NP optimization problems
• On the presence of disjoint subgraphs of a specified type
• Query automata over finite trees
• Regular languages defined with generalized quantifiers
• STACS 2004
• Some computational aspects of circumscription
• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
• The polynomial-time hierarchy
• The quantifier structure of sentences that characterize nondeterministic time complexity
• Tree acceptors and some of their applications
• Universal quantifiers and time complexity of random access machines
• Weak Second‐Order Arithmetic and Finite Automata

Cited in

(4)

• Logical equivalences, homomorphism indistinguishability, and forbidden minors
• Existential second-order logic over strings
• Automated Reasoning
• scientific article; zbMATH DE number 2087211 (Why is no real title available?)

Describes a project that uses

Uses Software

• MONA
• XPath
• Lixto

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3586006)