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

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) adm…