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.
翻译：超异性是标志性过渡系统的正确性条件,这些系统比传统痕量特性更显眼,特别与安全有关。最近,Attiya 和 Enea 研究了一种强有力的观测改进概念,它保存了所有超异性。它们分析了远方模拟与仅带有有限痕迹的环境下的强烈观测改进之间的对应关系。我们在有有限和无限痕迹的环境下研究了这种对应关系。特别是,我们表明远方模拟不维护这一环境中的超活性特性。我们以进步条件延长了远方模拟验证义务,并证明这种进步前方模拟确实意味着强烈的观测改进。
相关内容
微信扫码咨询专知VIP会员