Complexity results for modal logic with recursion via translations and tableaux
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2023
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913466138230784 |
|---|---|
| author | Aceto, Luca Achilleos, Antonis Anastasiadi, Elli Francalanza, Adrian Ingólfsdóttir, Anna |
| author_facet | Aceto, Luca Achilleos, Antonis Anastasiadi, Elli Francalanza, Adrian Ingólfsdóttir, Anna |
| contents | This paper studies the complexity of classical modal logics and of their extension with fixed-point operators, using translations to transfer results across logics. In particular, we show several complexity results for multi-agent logics via translations to and from the $μ$-calculus and modal logic, which allow us to transfer known upper and lower bounds. We also use these translations to introduce terminating and non-terminating tableau systems for the logics we study, based on Kozen's tableau for the $μ$-calculus and the one of Fitting and Massacci for modal logic. Finally, we describe these tableaux with $μ$-calculus formulas, thus reducing the satisfiability of each of these logics to the satisfiability of the $μ$-calculus, resulting in a general 2EXP upper bound for satisfiability testing. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2306_16881 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Complexity results for modal logic with recursion via translations and tableaux Aceto, Luca Achilleos, Antonis Anastasiadi, Elli Francalanza, Adrian Ingólfsdóttir, Anna Logic in Computer Science This paper studies the complexity of classical modal logics and of their extension with fixed-point operators, using translations to transfer results across logics. In particular, we show several complexity results for multi-agent logics via translations to and from the $μ$-calculus and modal logic, which allow us to transfer known upper and lower bounds. We also use these translations to introduce terminating and non-terminating tableau systems for the logics we study, based on Kozen's tableau for the $μ$-calculus and the one of Fitting and Massacci for modal logic. Finally, we describe these tableaux with $μ$-calculus formulas, thus reducing the satisfiability of each of these logics to the satisfiability of the $μ$-calculus, resulting in a general 2EXP upper bound for satisfiability testing. |
| title | Complexity results for modal logic with recursion via translations and tableaux |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2306.16881 |