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.