Document Open Access Logo

Brief Announcement: On Strong Observational Refinement and Forward Simulation

Authors John Derrick , Simon Doherty, Brijesh Dongol , Gerhard Schellhorn, Heike Wehrheim

PDF

File

Thumbnail PDF
PDF
LIPIcs.DISC.2021.55.pdf
  • Filesize: 0.53 MB
  • 4 pages

Document Identifiers

Related Versions

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

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

Author Details

John Derrick
  • University of Sheffield, UK
Simon Doherty
  • University of Sheffield, UK
Brijesh Dongol
  • University of Surrey, UK
Gerhard Schellhorn
  • Universität Augsburg, Germany
Heike Wehrheim
  • Universität Oldenburg, Germany

Funding

  • Derrick, John: EPSRC Grant EP/R032351/1.
  • Dongol, Brijesh: EPSRC grants EP/V038915/1, EP/R032556/1, EP/R025134/2 and VeTSS.
  • Wehrheim, Heike: DFG Grant SFB 901.

References

  1. 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.
  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.
  3. 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.
  4. 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.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact