Compositional circular assume-guarantee rules cannot be sound and complete

DOI10.1007/3-540-36576-1_22MaRDI QIDQ4417869zbMATH OpenFDO

Authors Patrick Maier

Publication date 30 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2620/26200343.htm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• On the completeness of compositional reasoning
• On the completeness of compositional reasoning methods
• Foundations for circular compositional reasoning
• Automated circular assume-guarantee reasoning
• Abstract patterns of compositional reasoning.

Cited in

(10)

• Automated circular assume-guarantee reasoning
• Conditions of contracts for separating responsibilities in heterogeneous systems
• On the completeness of compositional reasoning
• Debits and Credits in Petri Nets and Linear Logic
• On the completeness of compositional reasoning methods
• Compositional reasoning
• A set-theoretic framework for assume-guarantee reasoning
• Foundations for circular compositional reasoning
• Automated compositional proofs for real-time systems
• Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning

This page was built for publication: Compositional circular assume-guarantee rules cannot be sound and complete

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4417869)