A theory of normed simulations

TL;DR

This paper introduces normed simulations, a simplified and decidable class of simulation relations that facilitate mechanized refinement proofs and establish a complete proof method for behavior inclusion under certain conditions.

Contribution

It defines normed simulations, proves their decidability under certain conditions, and shows they form a complete proof method for behavior inclusion with finite nondeterminism.

Findings

Normed simulations restrict each lower-level step to at most one higher-level step.

Decidability of normed simulation relations is established under certain logical conditions.

Normed simulations, combined with their properties, provide a complete proof method for behavior inclusion.

Abstract

In existing simulation proof techniques, a single step in a lower-level specification may be simulated by an extended execution fragment in a higher-level one. As a result, it is cumbersome to mechanize these techniques using general purpose theorem provers. Moreover, it is undecidable whether a given relation is a simulation, even if tautology checking is decidable for the underlying specification logic. This paper introduces various types of normed simulations. In a normed simulation, each step in a lower-level specification can be simulated by at most one step in the higher-level one, for any related pair of states. In earlier work we demonstrated that normed simulations are quite useful as a vehicle for the formalization of refinement proofs via theorem provers. Here we show that normed simulations also have pleasant theoretical properties: (1) under some reasonable assumptions, it is decidable whether a given relation is a normed forward simulation, provided tautology checking is decidable for the underlying logic; (2) at the semantic level, normed forward and backward simulations together form a complete proof method for establishing behavior inclusion, provided that the higher-level specification has finite invisible nondeterminism.