A Set-Theoretic Framework for Assume-Guarantee Reasoning

Patrick Maier

doi:10.1007/3-540-48224-5_67

A Set-Theoretic Framework for Assume-Guarantee Reasoning

Patrick Maier

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

9 Citations (Scopus)

Abstract

We present a circular assume-guarantee rule in an abstract setting (of sets over a partially-ordered domain). The rule has a mathematically concise side condition. Now, in order to prove an assume-guarantee rule in a concrete setting, all we need to do is to instantiate the abstract setting and check the side condition; i.e., we need not redo the notorious circularity argument again. We use this framework to prove a new assume-guarantee rule for Kripke structures. That rule generalizes existing assume-guarantee rules for other settings such as Reactive Modules or Mealy machines.

Original language	English
Title of host publication	Automata, Languages and Programming
Subtitle of host publication	28th International Colloquium, ICALP 2001; Crete, Greece, July 8–12, 2001; Proceedings
Publisher	Springer
Pages	821-834
Number of pages	14
DOIs	https://doi.org/10.1007/3-540-48224-5_67
Publication status	Published - 2001
Event	28th International Colloquium on Automata, Languages and Programming - Crete, Greece Duration: 8 Jul 2001 → 12 Jul 2001

Conference

Conference	28th International Colloquium on Automata, Languages and Programming
Abbreviated title	ICALP 2001
Country/Territory	Greece
City	Crete
Period	8/07/01 → 12/07/01

Keywords

compositional verification
assume-guarantee reasoning
Kripke structures
trace semantics

Access to Document

10.1007/3-540-48224-5_67

Cite this

@inproceedings{7f2efb47bc5a4267b9afd4fd44be8f28,

title = "A Set-Theoretic Framework for Assume-Guarantee Reasoning",

abstract = "We present a circular assume-guarantee rule in an abstract setting (of sets over a partially-ordered domain). The rule has a mathematically concise side condition. Now, in order to prove an assume-guarantee rule in a concrete setting, all we need to do is to instantiate the abstract setting and check the side condition; i.e., we need not redo the notorious circularity argument again. We use this framework to prove a new assume-guarantee rule for Kripke structures. That rule generalizes existing assume-guarantee rules for other settings such as Reactive Modules or Mealy machines.",

keywords = "compositional verification, assume-guarantee reasoning, Kripke structures, trace semantics",

author = "Patrick Maier",

year = "2001",

doi = "10.1007/3-540-48224-5_67",

language = "English",

pages = "821--834",

booktitle = "Automata, Languages and Programming",

publisher = "Springer",

note = "28th International Colloquium on Automata, Languages and Programming, ICALP 2001 ; Conference date: 08-07-2001 Through 12-07-2001",

}

TY - GEN

T1 - A Set-Theoretic Framework for Assume-Guarantee Reasoning

AU - Maier, Patrick

PY - 2001

Y1 - 2001

N2 - We present a circular assume-guarantee rule in an abstract setting (of sets over a partially-ordered domain). The rule has a mathematically concise side condition. Now, in order to prove an assume-guarantee rule in a concrete setting, all we need to do is to instantiate the abstract setting and check the side condition; i.e., we need not redo the notorious circularity argument again. We use this framework to prove a new assume-guarantee rule for Kripke structures. That rule generalizes existing assume-guarantee rules for other settings such as Reactive Modules or Mealy machines.

AB - We present a circular assume-guarantee rule in an abstract setting (of sets over a partially-ordered domain). The rule has a mathematically concise side condition. Now, in order to prove an assume-guarantee rule in a concrete setting, all we need to do is to instantiate the abstract setting and check the side condition; i.e., we need not redo the notorious circularity argument again. We use this framework to prove a new assume-guarantee rule for Kripke structures. That rule generalizes existing assume-guarantee rules for other settings such as Reactive Modules or Mealy machines.

KW - compositional verification

KW - assume-guarantee reasoning

KW - Kripke structures

KW - trace semantics

U2 - 10.1007/3-540-48224-5_67

DO - 10.1007/3-540-48224-5_67

M3 - Conference contribution

SP - 821

EP - 834

BT - Automata, Languages and Programming

PB - Springer

T2 - 28th International Colloquium on Automata, Languages and Programming

Y2 - 8 July 2001 through 12 July 2001

ER -

A Set-Theoretic Framework for Assume-Guarantee Reasoning

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this