Inquisitive Team Semantics of LTL
Abstract
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.
Keywords
Cite
@article{arxiv.2505.10700,
title = {Inquisitive Team Semantics of LTL},
author = {Laura Bozzelli and Tadeusz Litak and Munyque Mittelmann and Aniello Murano},
journal= {arXiv preprint arXiv:2505.10700},
year = {2025}
}