document: CTR-S : a logic for specifying contracts in semantic web services A requirements analysis in the emerging field of Semantic Web Services ( SWS ) ( see http:\/\/daml.org\/services\/swsl\/requirements\/ ) has identified four major areas of research : intelligent service discovery , automated contracting of services , process modeling , and service enactment . This paper deals with the intersection of two of these areas : process modeling as it pertains to automated contracting . Specifically , we propose a logic , called CTR-S , which captures the dynamic aspects of contracting for services . Since CTR-S is an extension of the classical first-order logic , it is well-suited to model the static aspects of contracting as well . A distinctive feature of contracting is that it involves two or more parties in a potentially adversarial situation . CTR-S is designed to model this adversarial situation through its novel model theory , which incorporates certain game-theoretic concepts . In addition to the model theory , we develop a proof theory for CTR-S and demonstrate the use of the logic formodeling and reasoning about Web service contracts .
doc_bio_tags: O O O O O O B O O B I O O O O O O O O O B I O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O B O