Liveness-preserving simulation relations

Abstract

We present a simulation-based proof method for liveness properties. Our method is based on simulation relations that relate the liveness properties of an implementation to those of the specification. Even though reasoning about liveness is usually associated with reasoning over entire executions, variant functions, fairness etc., our method requires reasoning over individual states/transitions only. It thus presents a significant methodological advance over current methods.