On Strong Observational Refinement and Forward Simulation
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
@article{arxiv.2107.14509,
title = {On Strong Observational Refinement and Forward Simulation},
author = {John Derrick and Simon Doherty and Brijesh Dongol and Gerhard Schellhorn and Heike Wehrheim},
journal= {arXiv preprint arXiv:2107.14509},
year = {2021}
}
Comments
Full version of the paper to appear in DISC 2021