Complexity of Model Checking Second-Order Hyperproperties on Finite Structures
摘要
We study the model checking problem of Hyper \(^2\) LTL over finite structures. Hyper \(^2\) LTL is a second-order hyperlogic, that extends the well-studied logic HyperLTL by adding quantification over sets of traces, to express complex hyperproperties such as epistemic and asynchronous hyperproperties. While Hyper \(^2\) LTL is very expressive, its expressiveness comes with a price, and its general model checking problem is undecidable. This motivates us to study the model checking problem for Hyper \(^2\) LTL over finite structures – tree-shaped or acyclic graphs, which are particularly useful for monitoring purposes. We show that Hyper \(^2\) LTL model checking is decidable on finite structures:It is in PSPACE (in the size of the model) on tree-shaped models and in EXPSPACE on acyclic models. Additionally, we show that for an expressive fragment of Hyper \(^2\) LTL, namely the Fixpoint Hyper \(^2\) LTL \(_{fp}\) fragment, the model checking problem is much simpler and is P-complete on tree-shaped models and EXP-complete on acyclic models. Last, we present some preliminary results that take into account not only the size of the model, but also the formula size.