On Strong Observational Refinement and Forward Simulation

TL;DR

This paper investigates the relationship between forward simulation and strong observational refinement in systems with both finite and infinite traces, revealing limitations and proposing an extended proof obligation to ensure hyperproperty preservation.

Contribution

It extends the analysis of strong observational refinement to infinite traces and introduces a progressive forward simulation condition that guarantees refinement.

Findings

Forward simulation does not preserve hyperliveness in infinite traces.

Adding a progress condition to forward simulation ensures strong observational refinement.

The extended proof obligation captures infinite trace behaviors more accurately.

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.