We study the model checking problem of Hyper2LTL over finite structures. Hyper2LTL 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 Hyper2LTL 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 Hyper2LTL over finite structures -- tree-shaped or acyclic graphs, which are particularly useful for monitoring purposes. We show that Hyper2LTL 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 Hyper2LTL, namely the Fixpoint Hyper2LTLfp 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.

翻译：我们研究了Hyper2LTL在有限结构上的模型检测问题。Hyper2LTL是一种二阶超逻辑，它通过添加对迹集合的量化来扩展已被深入研究的HyperLTL逻辑，从而能够表达复杂的超性质，例如认知超性质和异步超性质。尽管Hyper2LTL具有很强的表达能力，但其表达能力的提升也带来了代价，其一般模型检测问题是不可判定的。这促使我们研究Hyper2LTL在有限结构——树形或无环图——上的模型检测问题，这些结构在监测应用中特别有用。我们证明了Hyper2LTL在有限结构上的模型检测是可判定的。在树形模型上，其复杂度为PSPACE（相对于模型大小）；在无环模型上，其复杂度为EXPSPACE。此外，我们证明对于Hyper2LTL的一个表达力丰富的片段，即不动点片段Hyper2LTLfp，其模型检测问题要简单得多：在树形模型上是P-完全的，在无环模型上是EXP-完全的。最后，我们给出了一些初步结果，这些结果不仅考虑了模型的大小，还考虑了公式的大小。