Constructive design of a hierarchy of semantics of a transition system by abstract interpretation

Research output: Contribution to journalArticlepeer-review

Abstract

We construct a hierarchy of semantics by successive abstract interpretations. Starting from the maximal trace semantics of a transition system, we derive the big-step semantics, termination and nontermination semantics, Plotkin's natural, Smyth's demoniac and Hoare's angelic relational semantics and equivalent nondeterministic denotational semantics (with alternative powerdomains to the Egli-Milner and Smyth constructions), D. Scott's deterministic denotational semantics, the generalized and Dijkstra's conservative/liberal predicate transformer semantics, the generalized/total and Hoare's partial correctness axiomatic semantics and the corresponding proof methods. All the semantics are presented in a uniform fixpoint form and the correspondences between these semantics are established through composable Galois connections, each semantics being formally calculated by abstract interpretation of a more concrete one using Kleene and/or Tarski fixpoint approximation transfer theorems.

Original languageEnglish (US)
Pages (from-to)47-103
Number of pages57
JournalTheoretical Computer Science
Volume277
Issue number1-2
DOIs
StatePublished - Apr 28 2002

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Constructive design of a hierarchy of semantics of a transition system by abstract interpretation'. Together they form a unique fingerprint.

Cite this