Inquisitive Team Semantics of LTL
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913841450844160 |
|---|---|
| author | Bozzelli, Laura Litak, Tadeusz Mittelmann, Munyque Murano, Aniello |
| author_facet | Bozzelli, Laura Litak, Tadeusz Mittelmann, Munyque Murano, Aniello |
| contents | In this paper, we introduce a novel team semantics of LTL inspired by inquisitive logic. The main features of the resulting logic, we call InqLTL, are the intuitionistic interpretation of implication and the Boolean semantics of disjunction. We show that InqLTL with Boolean negation is highly undecidable and strictly less expressive than TeamLTL with Boolean negation. On the positive side, we identify a meaningful fragment of InqLTL with a decidable model-checking problem which can express relevant classes of hyperproperties. To the best of our knowledge, this fragment represents
the first hyper logic with a decidable model-checking problem which allows unrestricted use of temporal modalities and
universal second-order quantification over traces. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_10700 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Inquisitive Team Semantics of LTL Bozzelli, Laura Litak, Tadeusz Mittelmann, Munyque Murano, Aniello Logic in Computer Science Formal Languages and Automata Theory F.4.1 In this paper, we introduce a novel team semantics of LTL inspired by inquisitive logic. The main features of the resulting logic, we call InqLTL, are the intuitionistic interpretation of implication and the Boolean semantics of disjunction. We show that InqLTL with Boolean negation is highly undecidable and strictly less expressive than TeamLTL with Boolean negation. On the positive side, we identify a meaningful fragment of InqLTL with a decidable model-checking problem which can express relevant classes of hyperproperties. To the best of our knowledge, this fragment represents the first hyper logic with a decidable model-checking problem which allows unrestricted use of temporal modalities and universal second-order quantification over traces. |
| title | Inquisitive Team Semantics of LTL |
| topic | Logic in Computer Science Formal Languages and Automata Theory F.4.1 |
| url | https://arxiv.org/abs/2505.10700 |