Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2408.13840 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929474059108352 |
|---|---|
| author | Bodirsky, Manuel Kozik, Marcin Madelaine, Florent Martin, Barnaby Wrona, Michal |
| author_facet | Bodirsky, Manuel Kozik, Marcin Madelaine, Florent Martin, Barnaby Wrona, Michal |
| contents | We give a new, direct proof of the tetrachotomy classification for the model-checking problem of positive equality-free logic parameterised by the model. The four complexity classes are Logspace, NP-complete, co-NP-complete and Pspace-complete. The previous proof of this result relied on notions from universal algebra and core-like structures called U-X-cores. This new proof uses only relations, and works for infinite structures also in the distinction between Logspace and NP-hard under Turing reductions.
For finite domains, the membership in NP and co-NP follows from a simple argument, which breaks down already over an infinite set with a binary relation. We develop some interesting new algorithms to solve NP and co-NP membership for a variety of infinite structures. We begin with those first-order definable in (Q;=), the so-called equality languages, then move to those first-order definable in (Q;<), the so-called temporal languages. However, it is first-order expansions of the Random Graph (V,E) that provide the most interesting examples. In all of these cases, the derived classification is a tetrachotomy between Logspace, NP-complete, co-NP-complete and Pspace-complete. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_13840 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Model-checking positive equality free logic on a fixed structure (direttissima) Bodirsky, Manuel Kozik, Marcin Madelaine, Florent Martin, Barnaby Wrona, Michal Logic in Computer Science We give a new, direct proof of the tetrachotomy classification for the model-checking problem of positive equality-free logic parameterised by the model. The four complexity classes are Logspace, NP-complete, co-NP-complete and Pspace-complete. The previous proof of this result relied on notions from universal algebra and core-like structures called U-X-cores. This new proof uses only relations, and works for infinite structures also in the distinction between Logspace and NP-hard under Turing reductions. For finite domains, the membership in NP and co-NP follows from a simple argument, which breaks down already over an infinite set with a binary relation. We develop some interesting new algorithms to solve NP and co-NP membership for a variety of infinite structures. We begin with those first-order definable in (Q;=), the so-called equality languages, then move to those first-order definable in (Q;<), the so-called temporal languages. However, it is first-order expansions of the Random Graph (V,E) that provide the most interesting examples. In all of these cases, the derived classification is a tetrachotomy between Logspace, NP-complete, co-NP-complete and Pspace-complete. |
| title | Model-checking positive equality free logic on a fixed structure (direttissima) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2408.13840 |