Details
Originalsprache | Englisch |
---|---|
Titel des Sammelwerks | LICS 22 |
Untertitel | Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science |
Erscheinungsort | New York |
Herausgeber (Verlag) | Association for Computing Machinery (ACM) |
Seiten | 44:1-44:13 |
Seitenumfang | 13 |
ISBN (elektronisch) | 978-1-4503-9351-5 |
Publikationsstatus | Veröffentlicht - Aug. 2022 |
Abstract
In this paper, we study a novel approach to asynchronous hyperproperties by reconsidering the foundations of temporal team semantics. We consider three logics: TeamLTL, TeamCTL and TeamCTL*, which are obtained by adding quantifcation over so-called time evaluation functions controlling the asynchronous progress of traces. We then relate synchronous TeamLTL to our new logics and show how it can be embedded into them. We show that the model checking problem for TeamCTL with Boolean disjunctions is highly undecidable by encoding recurrent computations of non-deterministic 2-counter machines. Finally, we present a translation from TeamCTL* to Alternating Asynchronous Büchi Automata and obtain decidability results for the path checking problem as well as restricted variants of the model checking and satisfability problems.
ASJC Scopus Sachgebiete
- Informatik (insg.)
- Software
- Mathematik (insg.)
- Allgemeine Mathematik
Zitieren
- Standard
- Harvard
- Apa
- Vancouver
- BibTex
- RIS
LICS 22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. New York: Association for Computing Machinery (ACM), 2022. S. 44:1-44:13 3533360.
Publikation: Beitrag in Buch/Bericht/Sammelwerk/Konferenzband › Aufsatz in Konferenzband › Forschung › Peer-Review
}
TY - GEN
T1 - Temporal Team Semantics Revisited
AU - Gutsfeld, Jens Oliver
AU - Meier, Arne
AU - Ohrem, Christoph
AU - Virtema, Jonni
N1 - Funding Information: The frst two authors were partially funded by the DFG grant MU 1508/3-1. The third author was partially funded by the DFG grant ME 4279/1-2. The fourth author was partially funded by the DFG grant VI 1045/1-1.
PY - 2022/8
Y1 - 2022/8
N2 - In this paper, we study a novel approach to asynchronous hyperproperties by reconsidering the foundations of temporal team semantics. We consider three logics: TeamLTL, TeamCTL and TeamCTL*, which are obtained by adding quantifcation over so-called time evaluation functions controlling the asynchronous progress of traces. We then relate synchronous TeamLTL to our new logics and show how it can be embedded into them. We show that the model checking problem for TeamCTL with Boolean disjunctions is highly undecidable by encoding recurrent computations of non-deterministic 2-counter machines. Finally, we present a translation from TeamCTL* to Alternating Asynchronous Büchi Automata and obtain decidability results for the path checking problem as well as restricted variants of the model checking and satisfability problems.
AB - In this paper, we study a novel approach to asynchronous hyperproperties by reconsidering the foundations of temporal team semantics. We consider three logics: TeamLTL, TeamCTL and TeamCTL*, which are obtained by adding quantifcation over so-called time evaluation functions controlling the asynchronous progress of traces. We then relate synchronous TeamLTL to our new logics and show how it can be embedded into them. We show that the model checking problem for TeamCTL with Boolean disjunctions is highly undecidable by encoding recurrent computations of non-deterministic 2-counter machines. Finally, we present a translation from TeamCTL* to Alternating Asynchronous Büchi Automata and obtain decidability results for the path checking problem as well as restricted variants of the model checking and satisfability problems.
KW - Asynchronicity
KW - Automata Theory
KW - Hyperproperties
KW - Model Checking
KW - Team Semantics
KW - Temporal Logic
UR - http://www.scopus.com/inward/record.url?scp=85136992511&partnerID=8YFLogxK
U2 - 10.1145/3531130.3533360
DO - 10.1145/3531130.3533360
M3 - Conference contribution
SP - 44:1-44:13
BT - LICS 22
PB - Association for Computing Machinery (ACM)
CY - New York
ER -