Constructive design of a hierarchy of semantics of a transition system by abstract interpretation (Extended abstract)

Research output: Contribution to journalConference articlepeer-review

Abstract

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.

Original languageEnglish (US)
Pages (from-to)77-102
Number of pages26
JournalElectronic Notes in Theoretical Computer Science
Volume6
DOIs
StatePublished - 1997
EventMFPS XIII, Mathematical Foundations of Progamming Semantics, Thirteenth Annual Conference - Pittsburgh, PA, United States
Duration: Mar 23 1997Mar 26 1997

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 (Extended abstract)'. Together they form a unique fingerprint.

Cite this