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完全问题。最后，我们给出了同时考虑模型规模和公式规模的初步分析结果。