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

Research output: Contribution to journalArticle

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

Fingerprint

Abstract Interpretation
Transition Systems
Semantics
Denotational Semantics
Fixpoint
Hierarchy
Design
Galois Connection
Transformer
Predicate
Termination
Correctness
Correspondence
Trace
Partial

ASJC Scopus subject areas

  • Computational Theory and Mathematics

Cite this

Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. / Cousot, Patrick.

In: Theoretical Computer Science, Vol. 277, No. 1-2, 28.04.2002, p. 47-103.

Research output: Contribution to journalArticle

@article{42475f1dd1814448b33eaaf575431246,
title = "Constructive design of a hierarchy of semantics of a transition system by abstract interpretation",
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.",
author = "Patrick Cousot",
year = "2002",
month = "4",
day = "28",
doi = "10.1016/S0304-3975(00)00313-3",
language = "English (US)",
volume = "277",
pages = "47--103",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "1-2",

}

TY - JOUR

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

AU - Cousot, Patrick

PY - 2002/4/28

Y1 - 2002/4/28

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0037188218&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0037188218&partnerID=8YFLogxK

U2 - 10.1016/S0304-3975(00)00313-3

DO - 10.1016/S0304-3975(00)00313-3

M3 - Article

VL - 277

SP - 47

EP - 103

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 1-2

ER -