Abstract:
Correctness proofs of both abstractions of systems and refinements of
specifications rely upon binary relations that are expressed as simulations,
or as safety/liveness relations, or as Galois connections.
In this talk, we survey forms of binary correctness relations that one uses
to relate systems, and we study basic properties of such relations.
Also, properties of systems are often stated as
temporal logic formulas, and we present sublogics of temporal logic
for reasoning about abstractions and refinements.
The talk concludes with a presentation of Larsen's modal transition
systems, which provide a sound model format for reasoning about
abstractions and refinements with full (modal mu-calculus) temporal logic.