Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-I-2003-2-001

Compositional circular assume-guarantee rules cannot be sound and complete

Maier, Patrick

MPI-I-2003-2-001. January 2003, 22 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
Acknowledgement:
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-2003-2-001.ps314 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document: http://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},
}