- Restrictions on Access:
- Unclassified, Unlimited, Publicly available.
- Compositional proof systems not only enable the stepwise development of concurrent processes but also provide a basis to alleviate the state explosion problem associated with model checking. An assume-guarantee style of specification and reasoning has long been advocated to achieve compositionality. However, this style of reasoning is often non-trivial, typically requiring human input to determine appropriate assumptions. In this paper, we present novel assume- guarantee rules in the setting of finite labelled transition systems with blocking communication. We show how these rules can be applied in an iterative and fully automated fashion within a framework based on learning.
- NASA Technical Reports Server (NTRS) Collection.
- Document ID: 20030107507.
SAVBS 2003; 2003; Unknown.
- Copyright, Distribution as joint owner in the copyright.
View MARC record | catkey: 15966203