CISPA
Browse
- No file added yet -

Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity

Download (806.11 kB)
conference contribution
posted on 2023-11-29, 18:18 authored by Jonni Virtema, Jana Hofmann, Bernd FinkbeinerBernd Finkbeiner, Juha Kontinen, Fan Yang
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.

History

Preferred Citation

Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen and Fan Yang. Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity. In: Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)

Legacy Posted Date

2022-05-06

Open Access Type

  • Hybrid

BibTeX

@inproceedings{cispa_all_3665, title = "Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity", author = "Virtema, Jonni and Hofmann, Jana and Finkbeiner, Bernd and Kontinen, Juha and Yang, Fan", booktitle="{Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)}", year="2021", }

Usage metrics

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC