Bartosz Bednarczyk ; Stéphane Demri - Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?

lmcs:7409 - Logical Methods in Computer Science, July 28, 2022, Volume 18, Issue 3 - https://doi.org/10.46298/lmcs-18(3:5)2022
Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?

Authors: Bartosz Bednarczyk ; Stéphane Demri

    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.


    Volume: Volume 18, Issue 3
    Published on: July 28, 2022
    Accepted on: May 20, 2022
    Submitted on: April 28, 2021
    Keywords: Computer Science - Logic in Computer Science

    Share

    Consultation statistics

    This page has been seen 649 times.
    This article's PDF has been downloaded 418 times.