Temporal verification of simulation and refinement

Abstract

The paper presents temporal logic methods for proving simulation and refinement relations between programs. After introducing the notions of fai~ transition systems and the specification language of temporal logic, we present proof rules for verifying properties of programs. We then define the relations of simulation and refinement between programs and relate them to inclusion relations between computations and observations of the compared systems. We then show that these semantic definitions can be formalized in temporal logic by the use of the temporal and observational semantics formulas. This representation expresses simulation and refinement as implications between a pair of such formulas. We provide proof rules, based on the rules for verifying program properties. The proof rules are illustrated on several simple examples. Towards the end, we recognize the usefulness of having a stuttering robust version of temporal logic. The second part of the paper presents a proposed temporal logic, called TLR, which is insensitive to stuttering. This logic is interpreted over sequences of sampling points, alternating between persistent and transient sample points. This logic possesses an idempotent next-time operator, which gives some insight into its stuttering robustness. We present a decision procedure and a complete axiomatic system for the propositional version of TLt~. It is shown that, if all system variables are taken to be left-continuous, then most of the rules of regular temporal logic are still sound for TLI%. Finally, we present a stronger proof rule for refinement, and illustrate its use to prove refinement of two programs that cannot be done within the regular temporal logic framework.