Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?
Adding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability but CTL with propositional quantification under the tree semantics (tQCTL) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of tQCTL a...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2022-07-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/7409/pdf |
| _version_ | 1797268523948441600 |
|---|---|
| author | Bartosz Bednarczyk Stéphane Demri |
| author_facet | Bartosz Bednarczyk Stéphane Demri |
| author_sort | Bartosz Bednarczyk |
| collection | DOAJ |
| description | Adding propositional quantification to the modal logics K, T or S4 is known
to lead to undecidability but CTL with propositional quantification under the
tree semantics (tQCTL) admits a non-elementary Tower-complete satisfiability
problem. We investigate the complexity of strict fragments of tQCTL as well as
of the modal logic K with propositional quantification under the tree
semantics. More specifically, we show that tQCTL restricted to the temporal
operator EX is already Tower-hard, which is unexpected as EX can only enforce
local properties. When tQCTL restricted to EX is interpreted on N-bounded trees
for some N >= 2, we prove that the satisfiability problem is AExpPol-complete;
AExpPol-hardness is established by reduction from a recently introduced tiling
problem, instrumental for studying the model-checking problem for interval
temporal logics. As consequences of our proof method, we prove Tower-hardness
of tQCTL restricted to EF or to EXEF and of the well-known modal logics such as
K, KD, GL, K4 and S4 with propositional quantification under a semantics based
on classes of trees. |
| first_indexed | 2024-04-25T01:33:50Z |
| format | Article |
| id | doaj.art-cff7fc40bfd748a49de92c46013f4a80 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:50Z |
| publishDate | 2022-07-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-cff7fc40bfd748a49de92c46013f4a802024-03-08T10:39:29ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742022-07-01Volume 18, Issue 310.46298/lmcs-18(3:5)20227409Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?Bartosz Bednarczykhttps://orcid.org/0000-0002-8267-7554Stéphane DemriAdding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability but CTL with propositional quantification under the tree semantics (tQCTL) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of tQCTL as well as of the modal logic K with propositional quantification under the tree semantics. More specifically, we show that tQCTL restricted to the temporal operator EX is already Tower-hard, which is unexpected as EX can only enforce local properties. When tQCTL restricted to EX is interpreted on N-bounded trees for some N >= 2, we prove that the satisfiability problem is AExpPol-complete; AExpPol-hardness is established by reduction from a recently introduced tiling problem, instrumental for studying the model-checking problem for interval temporal logics. As consequences of our proof method, we prove Tower-hardness of tQCTL restricted to EF or to EXEF and of the well-known modal logics such as K, KD, GL, K4 and S4 with propositional quantification under a semantics based on classes of trees.https://lmcs.episciences.org/7409/pdfcomputer science - logic in computer science |
| spellingShingle | Bartosz Bednarczyk Stéphane Demri Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard? Logical Methods in Computer Science computer science - logic in computer science |
| title | Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard? |
| title_full | Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard? |
| title_fullStr | Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard? |
| title_full_unstemmed | Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard? |
| title_short | Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard? |
| title_sort | why does propositional quantification make modal and temporal logics on trees robustly hard |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/7409/pdf |
| work_keys_str_mv | AT bartoszbednarczyk whydoespropositionalquantificationmakemodalandtemporallogicsontreesrobustlyhard AT stephanedemri whydoespropositionalquantificationmakemodalandtemporallogicsontreesrobustlyhard |