Loading [MathJax]/extensions/tex2jax.js

Temporal Team Semantics Revisited

Publikation: Beitrag in Buch/Bericht/Sammelwerk/KonferenzbandAufsatz in KonferenzbandForschungPeer-Review

Autorschaft

  • Jens Oliver Gutsfeld
  • Arne Meier
  • Christoph Ohrem
  • Jonni Virtema

Externe Organisationen

  • Westfälische Wilhelms-Universität Münster (WWU)

Details

OriginalspracheEnglisch
Titel des SammelwerksLICS 22
UntertitelProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
ErscheinungsortNew York
Herausgeber (Verlag)Association for Computing Machinery (ACM)
Seiten44:1-44:13
Seitenumfang13
ISBN (elektronisch)978-1-4503-9351-5
PublikationsstatusVerö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

Zitieren

Temporal Team Semantics Revisited. / Gutsfeld, Jens Oliver; Meier, Arne; Ohrem, Christoph et al.
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/KonferenzbandAufsatz in KonferenzbandForschungPeer-Review

Gutsfeld, JO, Meier, A, Ohrem, C & Virtema, J 2022, Temporal Team Semantics Revisited. in LICS 22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science., 3533360, Association for Computing Machinery (ACM), New York, S. 44:1-44:13. https://doi.org/10.1145/3531130.3533360
Gutsfeld, J. O., Meier, A., Ohrem, C., & Virtema, J. (2022). Temporal Team Semantics Revisited. In LICS 22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (S. 44:1-44:13). Artikel 3533360 Association for Computing Machinery (ACM). https://doi.org/10.1145/3531130.3533360
Gutsfeld JO, Meier A, Ohrem C, Virtema J. Temporal Team Semantics Revisited. in 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 Epub 2022 Aug 4. doi: 10.1145/3531130.3533360
Gutsfeld, Jens Oliver ; Meier, Arne ; Ohrem, Christoph et al. / Temporal Team Semantics Revisited. 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
Download
@inproceedings{395ca069bd144c61ac8635739228de20,
title = "Temporal Team Semantics Revisited",
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{\"u}chi Automata and obtain decidability results for the path checking problem as well as restricted variants of the model checking and satisfability problems.",
keywords = "Asynchronicity, Automata Theory, Hyperproperties, Model Checking, Team Semantics, Temporal Logic",
author = "Gutsfeld, {Jens Oliver} and Arne Meier and Christoph Ohrem and Jonni Virtema",
note = "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. ",
year = "2022",
month = aug,
doi = "10.1145/3531130.3533360",
language = "English",
pages = "44:1--44:13",
booktitle = "LICS 22",
publisher = "Association for Computing Machinery (ACM)",
address = "United States",

}

Download

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 -

Von denselben Autoren