MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2021

1. Author,Editor - 3. with BibTeX cite keys

MPI-I-2003-2-001

Compositional circular assume-guarantee rules cannot be sound and complete

Maier, Patrick

January 2003, 22 pages.

.
Status: available - back from printing

Circular assume-guarantee reasoning is used for the compositional verification of concurrent systems. Its soundness has been studied in depth, perhaps because circularity makes it anything but obvious. In this paper, we investigate completeness. We show that compositional circular assume-guarantee rules cannot be both sound and complete.

  • MPI-I-2003-2-001.ps
  • Attachement: MPI-I-2003-2-001.ps (314 KBytes)

URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2003-2-001

Hide details for BibTeXBibTeX
@TECHREPORT{Maier2003,
  AUTHOR = {Maier, Patrick},
  TITLE = {Compositional circular assume-guarantee rules cannot be sound and complete},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-2003-2-001},
  MONTH = {January},
  YEAR = {2003},
  ISSN = {0946-011X},
}