LIPIcs.DISC.2021.55.pdf
- Filesize: 0.53 MB
- 4 pages
Document
Brief Announcement: On Strong Observational Refinement and Forward Simulation
Authors
John Derrick 
,
Brijesh Dongol ,
Heike Wehrheim
-
Part of:
Volume:
35th International Symposium on Distributed Computing (DISC 2021)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Symposium on Distributed Computing (DISC) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-10-04
File
Document Identifiers
Author Details
Cite As Get BibTex
John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. Brief Announcement: On Strong Observational Refinement and Forward Simulation. In 35th International Symposium on Distributed Computing (DISC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 209, pp. 55:1-55:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.DISC.2021.55
Abstract
Hyperproperties are correctness conditions for labelled transition systems that are more expressive than traditional trace properties, with particular relevance to security. Recently, Attiya and Enea studied a notion of strong observational refinement that preserves all hyperproperties. They analyse the correspondence between forward simulation and strong observational refinement in a setting with finite traces only. We study this correspondence in a setting with both finite and infinite traces. In particular, we show that forward simulation does not preserve hyperliveness properties in this setting. We extend the forward simulation proof obligation with a progress condition, and prove that this progressive forward simulation does imply strong observational refinement.
Subject Classification
ACM Subject Classification
- Security and privacy → Formal methods and theory of security
- Computing methodologies → Concurrent computing methodologies
Keywords
- Strong Observational Refinement
- Hyperproperties
- Forward Simulation
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- H. Attiya and C. Enea. Putting strong linearizability in context: Preserving hyperproperties in programs that use concurrent objects. In J. Suomela, editor, DISC, volume 146 of LIPIcs, pages 2:1-2:17. Schloss Dagstuhl, 2019. URL: https://doi.org/10.4230/LIPIcs.DISC.2019.2.
- M. R. Clarkson and F. B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
- J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, and H. Wehrheim. On strong observational refinement and forward simulation, 2021. URL: http://arxiv.org/abs/2107.14509.
- V. Luchangco, M. Moir, and N. Shavit. Nonblocking k-compare-single-swap. In SPAA, pages 314-323. ACM, 2003. URL: https://doi.org/10.1145/777412.777468.