  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.
