Why propositional quantification makes modal logics on trees robustly hard ?

Bartosz BednarczykBartosz Bednarczyk, Stéphane DemriStéphane Demri

ISBN: 978-1-7281-3608-0
Download
DOI Link

Bartosz Bednarczyk, Stéphane Demri
Why propositional quantification makes modal logics on trees robustly hard ?
Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019), 1--13, June 2019. IEEE

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 (QCTL t ) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of QCTL t as well as of the modal logic K with propositional quantification under the tree semantics. More specifically, we show that QCTL t restricted to the temporal operator EX is already Tower-hard, which is unexpected as EX can only enforce local properties. When QCTL t 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 QCTL t restricted to EF or to EXEF and of the well-known modal logics K, KD, GL, S4, K4 and D4, with propositional quantification under a semantics based on classes of trees.
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@inproceedings{DBLP:conf/lics/BednarczykD19,
  author    = {Bartosz Bednarczyk and
               St{ \'{e}}phane Demri},
  title     = {Why Propositional Quantification Makes Modal Logics on Trees Robustly
               Hard?},
  booktitle = {34th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}
               2019, Vancouver, BC, Canada, June 24-27, 2019},
  pages     = {1--13},
  year      = {2019},
  crossref  = {DBLP:conf/lics/2019},
  url       = {https://doi.org/10.1109/LICS.2019.8785656},
  doi       = {10.1109/LICS.2019.8785656},
  timestamp = {Wed, 25 Sep 2019 18:03:36 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/lics/BednarczykD19},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/lics/2019,
  title     = {34th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}
               2019, Vancouver, BC, Canada, June 24-27, 2019},
  publisher = [[:Vorlage:IEEE]],
  year      = {2019},
  url       = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=8765678},
  isbn      = {978-1-7281-3608-0},
  timestamp = {Sun, 11 Aug 2019 19:07:26 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/lics/2019},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}