Computer Science – Logic in Computer Science
Scientific paper
2000-07-19
Computer Science
Logic in Computer Science
31 pages, 10figures
Scientific paper
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.
Griffioen W. O. D.
Vaandrager F. W.
No associations
LandOfFree
A theory of normed simulations does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with A theory of normed simulations, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A theory of normed simulations will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-631059