In recent years, hyperproperties (i.e., properties of sets of traces) have been identified as a crucial concept for capturing information-flow security policies and knowledge of agents in distributed systems. In the synchronous linear-time setting, a well-known approach for the specification of hyperproperties is based on set semantics of standard \(\textsf {LTL}\) . The resulting logic ( \(\textsf {TeamLTL}\) ) inherits the powerful split interpretation of disjunction from dependency logic. In this paper, we introduce a novel team semantics of \(\textsf {LTL}\) inspired by inquisitive logic, and whose main features are the intuitionistic interpretation of implication and the inquisitive semantics of disjunction. We investigate expressiveness, decidability, and complexity issues of the novel logic that we call \(\textsf {InqLTL}\) and its extension with strong negation. We show that \(\textsf {InqLTL}\) with strong negation is highly undecidable and strictly less expressive than \(\textsf {TeamLTL}\) with strong negation. On the positive side, we identify a meaningful fragment of \(\textsf {InqLTL}\) with a decidable model-checking problem which can express relevant classes of hyperproperties. To the best of our knowledge, this fragment represents the unique hyper logic with a decidable model-checking problem which allows unrestricted use of temporal modalities and universal second-order quantification over traces.

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

Inquisitive Team Semantics of LTL

  • Laura Bozzelli,
  • Tadeusz Litak,
  • Munyque Mittelmann,
  • Aniello Murano

摘要

In recent years, hyperproperties (i.e., properties of sets of traces) have been identified as a crucial concept for capturing information-flow security policies and knowledge of agents in distributed systems. In the synchronous linear-time setting, a well-known approach for the specification of hyperproperties is based on set semantics of standard \(\textsf {LTL}\) . The resulting logic ( \(\textsf {TeamLTL}\) ) inherits the powerful split interpretation of disjunction from dependency logic. In this paper, we introduce a novel team semantics of \(\textsf {LTL}\) inspired by inquisitive logic, and whose main features are the intuitionistic interpretation of implication and the inquisitive semantics of disjunction. We investigate expressiveness, decidability, and complexity issues of the novel logic that we call \(\textsf {InqLTL}\) and its extension with strong negation. We show that \(\textsf {InqLTL}\) with strong negation is highly undecidable and strictly less expressive than \(\textsf {TeamLTL}\) with strong negation. On the positive side, we identify a meaningful fragment of \(\textsf {InqLTL}\) with a decidable model-checking problem which can express relevant classes of hyperproperties. To the best of our knowledge, this fragment represents the unique hyper logic with a decidable model-checking problem which allows unrestricted use of temporal modalities and universal second-order quantification over traces.