Generalized model-checking problems for first-order logic

DOI10.1007/3-540-44693-1_2MaRDI QIDQ2762493zbMATH OpenFDO

Authors Martin Grohe

Publication date 9 January 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2010/20100012

Mathematics Subject Classification ID

Classical first-order logic (03B10) Descriptive complexity and finite models (68Q19) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

Descriptive complexity theory provides a convenient and intuitive way to model a large variety of computational problems. The basic problem studied in descriptive complexity is of the following form: Given a finite relational structure \(A\) and a sentence \(\phi\) of some logic \(L\), decide if \(\phi\) is satisfied by \(A\). We call this problem the \textit{model-checking problem} for \(L\). The model-checking problem and variants of it appear in different areas of computer science: The name model-checking is usually associated with automated verification. Here state spaces of finite state systems are modeled by Kripke structures and specifications are formulated in modal or temporal logics. Then checking whether the system has the specified property means checking whether the Kripke structure satisfies the specification, that is, model-checking. In recent years, this approach has very successfully been applied to the verification circuits and protocols. For the entire collection see [Zbl 0958.00036].

Recommendations

• The complexity of first-order and monadic second-order logic revisited
• First-Order Model Checking Problems Parameterized by the Model
• Model checking.
• On the complexity of the model checking problem
• scientific article; zbMATH DE number 2196601

Cited in

(17)

• Describing parameterized complexity classes
• Parameterized random complexity
• Tractability in constraint satisfaction problems: a survey
• Parameterized complexity: the main ideas and connections to practical computing
• The birth and early years of parameterized complexity
• A basic parameterized complexity primer
• The Model Checking Problem for Prefix Classes of Second-Order Logic: A Survey
• Model-Checking First-Order Logic: Automata and Locality
• First-order interpretations of bounded expansion classes
• Enumerating answers to first-order queries over databases of low degree
• scientific article; zbMATH DE number 7297863 (Why is no real title available?)
• Satisfiability Checking of Non-clausal Formulas Using General Matings
• First-Order Model-Checking in Random Graphs and Complex Networks
• On Diagrams and General Model Checkers
• Algorithmic uses of the Feferman-Vaught theorem
• Hard problems on random graphs
• Learning concepts definable in first-order logic with counting

This page was built for publication: Generalized model-checking problems for first-order logic

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