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

DOI10.1007/978-3-642-15025-8_13zbMATH Open1287.68107OpenAlexW1570464944WikidataQ59259582 ScholiaQ59259582MaRDI QIDQ3586006FDOQ3586006

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

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
• Model checking existential logic on partially ordered sets
• Model checking existential logic on partially ordered sets
• On the model-checking of monadic second-order formulas with edge set quantifications
• Model checking in the modal \(\mu \)-calculus and generic solutions

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)

Cites Work

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

Cited In (4)

• Title not available (Why is that?)
• Logical equivalences, homomorphism indistinguishability, and forbidden minors
• Automated Reasoning
• Existential second-order logic over strings

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)