Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?

Bartosz BednarczykBartosz Bednarczyk, Stéphane DemriStéphane Demri

Bartosz Bednarczyk, Stéphane Demri
Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?
Logical Methods in Computer Science, Volume 18, Issue 3(5), July 2022

Details
Bibtex

KurzfassungAbstract
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.
Weitere Informationen unter:Further Information: Link
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@article{BD2022,
  author  = {Bartosz Bednarczyk and St{\'{e}}phane Demri},
  title   = {Why Does Propositional Quantification Make Modal and Temporal
             Logics on Trees Robustly Hard?},
  journal = {Logical Methods in Computer Science},
  volume  = {Volume 18, Issue 3},
  number  = {5},
  year    = {2022},
  month   = {July},
  doi     = {10.46298/lmcs-18(3:5)2022}
}