Prophecies all the Way: Game-based Model-Checking for HyperQPTL beyond ${\forall }^{\ast }{\exists }^{\ast }$

Sarah Winter, Martin Zimmermann

Model-checking HyperLTL, a temporal logic expressing properties of sets of traces with applications to information-flow based security and privacy, has a decidable, but TOWER-compl…