(2021) Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity.
|
Text
LIPIcs-FSTTCS-2021-52.pdf - Accepted Version Available under License Creative Commons Attribution. Download (825kB) | Preview |
Abstract
We study the expressivity and complexity of model checking of linear temporal logic with team semantics (TeamLTL). TeamLTL, despite being a purely modal logic, is capable of defining hyper- properties, i.e., properties which relate multiple execution traces. TeamLTL has been introduced quite recently and only few results are known regarding its expressivity and its model checking problem. We relate the expressivity of TeamLTL to logics for hyperproperties obtained by extending LTL with trace and propositional quantifiers (HyperLTL and HyperQPTL). By doing so, we obtain a number of model checking results for TeamLTL and identify its undecidability frontier. In particular, we show decidability of model checking of the so-called left-flat fragment of any downward closed TeamLTL-extension. Moreover, we establish that the model checking problem of TeamLTL with Boolean disjunction and inclusion atoms is undecidable.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Bernd Finkbeiner (Reactive Systems Group, RSG) |
| Conference: | FST&TCS Foundations of Software Technology and Theoretical Computer Science |
| Depositing User: | Jana Hofmann |
| Date Deposited: | 06 May 2022 09:12 |
| Last Modified: | 06 May 2022 09:12 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3665 |
Actions
Actions (login required)
 |
View Item |