CTR-S: a logic for specifying contracts in semantic web services

ABSTRACT

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.

REFERENCES

• 1: Rajeev Alur , Thomas A. Henzinger , Orna Kupferman, Alternating-time Temporal Logic, Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS '97), p.100, October 19-22, 1997
• 2: P. C. Attie, M. P. Singh, E. A. Emerson, A. P. Sheth, and M. Rusinkiewicz. Scheduling workflows by enforcing intertask dependencies. Distributed Systems Engineering Journal, 3(4):222--238, December 1996.
• 3: F. Bacchus and F. Kabanza. Planning for temporally extended goals. In Proceedings of the Thirteenth National Conference on Artificial Intelligence (AAAI -96), pages 1215--1222, Portland, Oregon, USA, 1996. AAAI Press / The MIT Press.
• 4: Anthony J. Bonner, Workflow, transactions and datalog, Proceedings of the eighteenth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, p.294-305, May 31-June 03, 1999, Philadelphia, Pennsylvania, United States [doi>10.1145/303976.304005]
• 5: A. J. Bonner and M. Kifer. Concurrency and communication in transaction logic. In Joint Intl. Conference and Symposium on Logic Programming, pages 142--156, Bonn, Germany, September 1996. MIT Press.
• 6: Anthony J. Bonner , Michael Kifer, A logic for programming database transactions, Logics for databases and information systems, Kluwer Academic Publishers, Norwell, MA, 1998
• 7: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 8: Hasan Davulcu , Michael Kifer , C. R. Ramakrishnan , I. V. Ramakrishnan, Logic based modeling and analysis of workflows, Proceedings of the seventeenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, p.25-33, June 01-04, 1998, Seattle, Washington, United States [doi>10.1145/275487.275491]
• 9: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 10: Ronald Fagin , Joseph Y. Halpern , Moshe Y. Vardi , Yoram Moses, Reasoning about knowledge, MIT Press, Cambridge, MA, 1995
• 11: Benjamin N. Grosof , Terrence C. Poon, SweetDeal: representing agent contracts with exceptions using XML rules, ontologies, and process descriptions, Proceedings of the 12th international conference on World Wide Web, May 20-24, 2003, Budapest, Hungary [doi>10.1145/775152.775200]
• 12: R. Gunthor. Extended transaction processing based on dependency rules. In Proceedings of the RIDE-IMS Workshop , 1993.
• 13: J. Hintikka. Logic, Language Games, and Information. Oxford Univ. Press, Clarendon, Oxford, 1973.
• 14: Michael Kifer , Georg Lausen , James Wu, Logical foundations of object-oriented and frame-based languages, Journal of the ACM (JACM), v.42 n.4, p.741-843, July 1995 [doi>10.1145/210332.210335]
• 15: F. Leymann. Web services flow language (wsfl 1.0). Technical report, IBM, 2001. http://www-4.ibm.com/software/solutions/webservices/pdf/WSFL.pdf.
• 16: R. McNaughton. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 65:149--184, 1993.
• 17: S. Mukherjee, H. Davulcu, M. Kifer, G. Yang, and P. Senkul. Survey of logic based approaches to workflow modeling. In J. Chomicki, R. van der Meyden, and G. Saake Springer, editors, Logics for Emerging Applications of Databases , LNCS. Springer-Verlag, October 2003.
• 18: M. Osborne and A. Rubinstein. A Course in Game Theory. The MIT Press, 1998.
• 19: Rohit Parikh, The logic of games and its applications, Selected papers of the international conference on "foundations of computation theory" on Topics in the theory of computation, p.111-139, December 1985, Borgholm, Sweden
• 20: Daniel M. Reeves , Michael P. Wellman , Benjamin N. Grosof, Automated negotiation from declarative contract descriptions, Proceedings of the fifth international conference on Autonomous agents, p.51-58, May 2001, Montreal, Quebec, Canada [doi>10.1145/375735.375867]
• 21: Craig Schlenoff , Michael Gruninger , Mihai Ciocoiu , Jintae Lee, The essence of the process specification language, Transactions of the Society for Computer Simulation International, v.16 n.4, p.204-216, Dec.1.1999
• 22: Munindar P. Singh, Semantical Considerations on Workflows: An Algebra for Intertask Dependencies, Proceedings of the Fifth International Workshop on Database Programming Languages, p.5, September 06-08, 1995
• 23: Munindar P. Singh, Synthesizing Distributed Constrained Events from Transactional Workflow, Proceedings of the Twelfth International Conference on Data Engineering, p.616-623, February 26-March 01, 1996

INDEX TERMS

Primary Classification:
  H. Information Systems
  H.4 INFORMATION SYSTEMS APPLICATIONS
      H.4.m Miscellaneous

Additional Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.3 Languages and Systems

General Terms:
Algorithms, Languages, Verification

Keywords:
contracts, services composition, web services