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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Complexity of Model Checking Second-Order Hyperproperties on Finite Structures

  • Bernd Finkbeiner,
  • Hadar Frenkel,
  • Tim Rohde

摘要

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.