NP Reasoning in the Monotone [Formula: see text]-Calculus

Satisfiability checking for monotone modal logic is known to be (only) NP-complete. We show that this remains true when the logic is extended with alternation-free fixpoint operators as well as the universal modality; the resulting logic – the alternation-free monotone [Formula: see text]-calculus w...

Descripción completa

Detalles Bibliográficos
Autores principales: Hausmann, Daniel, Schröder, Lutz
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324257/
http://dx.doi.org/10.1007/978-3-030-51074-9_28
_version_ 1783551903647399936
author Hausmann, Daniel
Schröder, Lutz
author_facet Hausmann, Daniel
Schröder, Lutz
author_sort Hausmann, Daniel
collection PubMed
description Satisfiability checking for monotone modal logic is known to be (only) NP-complete. We show that this remains true when the logic is extended with alternation-free fixpoint operators as well as the universal modality; the resulting logic – the alternation-free monotone [Formula: see text]-calculus with the universal modality – contains both concurrent propositional dynamic logic (CPDL) and the alternation-free fragment of game logic as fragments. We obtain our result from a characterization of satisfiability by means of Büchi games with polynomially many Eloise nodes.
format Online
Article
Text
id pubmed-7324257
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73242572020-06-30 NP Reasoning in the Monotone [Formula: see text]-Calculus Hausmann, Daniel Schröder, Lutz Automated Reasoning Article Satisfiability checking for monotone modal logic is known to be (only) NP-complete. We show that this remains true when the logic is extended with alternation-free fixpoint operators as well as the universal modality; the resulting logic – the alternation-free monotone [Formula: see text]-calculus with the universal modality – contains both concurrent propositional dynamic logic (CPDL) and the alternation-free fragment of game logic as fragments. We obtain our result from a characterization of satisfiability by means of Büchi games with polynomially many Eloise nodes. 2020-05-30 /pmc/articles/PMC7324257/ http://dx.doi.org/10.1007/978-3-030-51074-9_28 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Hausmann, Daniel
Schröder, Lutz
NP Reasoning in the Monotone [Formula: see text]-Calculus
title NP Reasoning in the Monotone [Formula: see text]-Calculus
title_full NP Reasoning in the Monotone [Formula: see text]-Calculus
title_fullStr NP Reasoning in the Monotone [Formula: see text]-Calculus
title_full_unstemmed NP Reasoning in the Monotone [Formula: see text]-Calculus
title_short NP Reasoning in the Monotone [Formula: see text]-Calculus
title_sort np reasoning in the monotone [formula: see text]-calculus
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324257/
http://dx.doi.org/10.1007/978-3-030-51074-9_28
work_keys_str_mv AT hausmanndaniel npreasoninginthemonotoneformulaseetextcalculus
AT schroderlutz npreasoninginthemonotoneformulaseetextcalculus

Ejemplares similares