Details
| Original language | English |
|---|---|
| Title of host publication | 43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018 |
| Editors | Igor Potapov, James Worrell, Paul Spirakis |
| Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
| ISBN (print) | 9783959770866 |
| Publication status | Published - 27 Aug 2018 |
| Event | 43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018 - Liverpool, United Kingdom (UK) Duration: 27 Aug 2018 → 31 Aug 2018 |
Publication series
| Name | Leibniz International Proceedings in Informatics, LIPIcs |
|---|---|
| Volume | 117 |
| ISSN (Print) | 1868-8969 |
Abstract
We develop team semantics for Linear Temporal Logic (LTL) to express hyperproperties, which have recently been identified as a key concept in the verification of information flow properties. Conceptually, we consider an asynchronous and a synchronous variant of team semantics. We study basic properties of this new logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of these basic logics react on adding other atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL under team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties.
Keywords
- Hyperproperties, LTL, Model checking, Satisfiability, Team semantics
ASJC Scopus subject areas
- Computer Science(all)
- Software
Cite this
- Standard
- Harvard
- Apa
- Vancouver
- BibTeX
- RIS
43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018. ed. / Igor Potapov; James Worrell; Paul Spirakis. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2018. 10 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 117).
Research output: Chapter in book/report/conference proceeding › Conference contribution › Research › peer review
}
TY - GEN
T1 - Team semantics for the specification and verification of hyperproperties
AU - Krebs, Andreas
AU - Meier, Arne
AU - Virtema, Jonni
AU - Zimmermann, Martin
N1 - Funding information: Funded by the German Research Foundation DFG, project ME 4279/1-2. 2 Funded by the German Research Foundation DFG, project “TriCS” (ZI 1516/1-1).
PY - 2018/8/27
Y1 - 2018/8/27
N2 - We develop team semantics for Linear Temporal Logic (LTL) to express hyperproperties, which have recently been identified as a key concept in the verification of information flow properties. Conceptually, we consider an asynchronous and a synchronous variant of team semantics. We study basic properties of this new logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of these basic logics react on adding other atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL under team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties.
AB - We develop team semantics for Linear Temporal Logic (LTL) to express hyperproperties, which have recently been identified as a key concept in the verification of information flow properties. Conceptually, we consider an asynchronous and a synchronous variant of team semantics. We study basic properties of this new logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of these basic logics react on adding other atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL under team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties.
KW - Hyperproperties
KW - LTL
KW - Model checking
KW - Satisfiability
KW - Team semantics
UR - http://www.scopus.com/inward/record.url?scp=85053217639&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.MFCS.2018.10
DO - 10.4230/LIPIcs.MFCS.2018.10
M3 - Conference contribution
AN - SCOPUS:85053217639
SN - 9783959770866
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018
A2 - Potapov, Igor
A2 - Worrell, James
A2 - Spirakis, Paul
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 43rd International Symposium on Mathematical Foundations of Computer Science, MFCS 2018
Y2 - 27 August 2018 through 31 August 2018
ER -