Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation (Extended Abstract)
Patrick M. Cousot · Electronic Notes in Theoretical Computer Science · 1997
We construct a hierarchy of semantics by successive abstract interpretations. Starting from a maximal trace semantics of a transition system, we derive a big-step semantics, termination and nontermination semantics, natural, demoniac and angelic relational semantics and equivalent nondeterministic denotational semantics, D. Scott's deterministic denotational semantics, generalized/conservative/liberal predicate transformer semantics, generalized/total/partial correctness axiomatic semantics and corresponding proof methods. All semantics are presented in uniform fixpoint form and the correspondence between these semantics are established through composable Galois connection.