A theory of normed simulations
<|reference_start|>A theory of normed simulations: 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.<|reference_end|>
@article{griffioen2000a,
    title={A theory of normed simulations},
    author={W.O.D. Griffioen and F.W. Vaandrager},
    journal={ACM Trans. Comput. Log. 5(4): 577-610 (2004)},
    year={2000},
    doi={10.1145/1024922.1024923},
    number={CSI-R0013},
    archivePrefix={arXiv},
    eprint={cs/0007030},
    primaryClass={cs.LO}
}