Brief Announcement: On Strong Observational Refinement and Forward Simulation

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

Thumbnail PDF


  • Filesize: 0.53 MB
  • 4 pages

Document Identifiers

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

Cite AsGet 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)


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
  • Strong Observational Refinement
  • Hyperproperties
  • Forward Simulation


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  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:
  2. M. R. Clarkson and F. B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157-1210, 2010. URL:
  3. J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, and H. Wehrheim. On strong observational refinement and forward simulation, 2021. URL:
  4. V. Luchangco, M. Moir, and N. Shavit. Nonblocking k-compare-single-swap. In SPAA, pages 314-323. ACM, 2003. URL: