{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T15:19:14Z","timestamp":1772205554188,"version":"3.50.1"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2010,9,17]],"date-time":"2010-09-17T00:00:00Z","timestamp":1284681600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Auton Agent Multi-Agent Syst"],"published-print":{"date-parts":[[2012,5]]},"DOI":"10.1007\/s10458-010-9152-3","type":"journal-article","created":{"date-parts":[[2010,9,16]],"date-time":"2010-09-16T12:20:02Z","timestamp":1284639602000},"page":"345-373","source":"Crossref","is-referenced-by-count":32,"title":["Towards verifying contract regulated service composition"],"prefix":"10.1007","volume":"24","author":[{"given":"Alessio","family":"Lomuscio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongyang","family":"Qu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Monika","family":"Solanki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,9,17]]},"reference":[{"key":"9152_CR1","unstructured":"Lomuscio, A., Qu, H., & Solanki, M. (2008). Towards verifying compliance in agent-based web service compositions. In Proceedings of the seventh international joint conference on autonomous agents and multi-agent systems (AAMAS-08) (pp. 265\u2013272). New York: ACM Press."},{"key":"9152_CR2","unstructured":"\u00c5gotnes, T., Hoek, W. V., Rodr\u00edguez-Aguilar, J. A., Sierra, C., & Wooldridge, M. (2007). On the logic of normative systems. In M. M. Veloso (Ed.), IJCAI (pp. 1175\u20131180)."},{"issue":"5","key":"9152_CR3","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R. Alur","year":"2002","unstructured":"Alur R., Henzinger T. A., Kupferman O. (2002) Alternating-time temporal logic. Journal of the ACM 49(5): 672\u2013713","journal-title":"Journal of the ACM"},{"key":"9152_CR4","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1093\/mind\/LXVII.265.100","volume":"58","author":"A. R. Anderson","year":"1958","unstructured":"Anderson A. R. (1958) A reduction of deontic logic to alethic modal logic. Mind 58: 100\u2013103","journal-title":"Mind"},{"key":"9152_CR5","unstructured":"Baldoni, M., Baroglio, C., Martelli, A., & Patti, V. (2005). Verification of protocol conformance and agent interoperability. In CLIMA VI. LNCS (Vol. 3900, pp. 265\u2013283). NY: Springer."},{"issue":"6","key":"9152_CR6","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1049\/iet-sen:20070027","volume":"1","author":"L. Baresi","year":"2007","unstructured":"Baresi L., Bianculli D., Ghezzi C., Guinea S., Spoletini P. (2007) Validation of web service compositions. IET Software 1(6): 219\u2013232","journal-title":"IET Software"},{"key":"9152_CR7","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W., & Weise, C. (1998). New generation of Uppaal. In Proceedings of the international workshop on software tools for technology transfer. Aalborg, Denmark."},{"key":"9152_CR8","unstructured":"Bordini, R., Fisher, M., Pardavila, C., Visser, W., & Wooldridge, M. (2003). Model checking multi-agent programs with CASP. In CAV\u201903. Volume of LNCS 2725 (pp. 110\u2013113). NY: Springer."},{"key":"9152_CR9","unstructured":"Cimatti, A., Clarke, E. M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., et\u00a0al. (2002). NuSMV2: An open-source tool for symbolic model checking. In Proceedings of the 14th international conference on computer aided verification (CAV\u201902). LNCS (Vol. 2404, pp. 359\u2013364). NY: Springer."},{"key":"9152_CR10","volume-title":"Model checking","author":"E. M. Clarke","year":"1999","unstructured":"Clarke E. M., Grumberg O., Peled D. A. (1999) Model checking. The MIT Press, Cambridge, MA"},{"issue":"2","key":"9152_CR11","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1016\/j.jal.2007.06.007","volume":"6","author":"R. Craven","year":"2008","unstructured":"Craven R., Sergot M. J. (2008) Agent strands in the action language nc+. Journal of Applied Logic 6(2): 172\u2013191","journal-title":"Journal of Applied Logic"},{"key":"9152_CR12","unstructured":"Booth, D., Haas, H., McCabe, F., Newcomer, E., Champion, M., Ferris, C., et\u00a0al. (2004). Web service architecture. W3c working group note 11 february 2004. http:\/\/www.w3.org\/TR\/ws-arch\/ ."},{"key":"9152_CR13","unstructured":"Dembi\u0144ski, P., Janowska, A., Janowski, P., Penczek, W., P\u00f3lrola, A., Szreter, M., et\u00a0al. (2003). VerICS: A tool for verifying Timed Automata and Estelle specifications. In Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of systems (TACAS\u201903). LNCS (Vol. 2619, pp. 278\u2013283). NY: Springer."},{"key":"9152_CR14","unstructured":"Desai, N., Narendra, N. C., & Singh, M. P. (2008). Checking correctness of business contracts via commitments. In AAMAS \u201908: Proceedings of the 7th international joint conference on autonomous agents and multiagent systems (pp. 787\u2013794). Richland, SC: International Foundation for Autonomous Agents and Multiagent Systems."},{"key":"9152_CR15","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about Knowledge","author":"R. Fagin","year":"1995","unstructured":"Fagin R., Halpern J. Y., Moses Y., Vardi M. Y. (1995) Reasoning about Knowledge. MIT Press, Cambridge"},{"key":"9152_CR16","unstructured":"Foster, H., Uchitel, S., Magee, J., & Kramer, J. (2003). Model-based verification of web service compositions. In Proceedings of the 10th IEEE international conference on automated software engineering. London: IEEE Press."},{"key":"9152_CR17","unstructured":"Fu, X., Bultan, T., & Su, J. (2004). Analysis of interacting BPEL web services. In 13th international conference on World Wide Web (pp. 621\u2013630). NY: ACM Press. http:\/\/doi.acm.org\/10.1145\/988672.988756 ."},{"issue":"1\u20132","key":"9152_CR18","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/j.artint.2002.12.001","volume":"153","author":"E. Giunchiglia","year":"2004","unstructured":"Giunchiglia E., Lee J., Lifschitz V., McCain N., Turner H. (2004) Nonmonotonic causal theories. Artificial Intelligence 153(1\u20132): 49\u2013104","journal-title":"Artificial Intelligence"},{"key":"9152_CR19","unstructured":"Henzinger, T. A., Jhala, R., Majumdar, R., & Sutre, G. (2003). Software verification with blast. In Proceedings of the tenth international workshop on model checking of software (SPIN). LNCS (Vol. 2648, pp. 235\u2013239). NY: Springer. http:\/\/www.gigascale.org\/pubs\/399.html ."},{"key":"9152_CR20","volume-title":"SPIN model checker, the: Primer and reference manual","author":"G. J. Holzmann","year":"2003","unstructured":"Holzmann G. J. (2003) SPIN model checker, the: Primer and reference manual. Addison Wesley Professional, Canada"},{"key":"9152_CR21","doi-asserted-by":"crossref","unstructured":"Huang, H., Tsai, W., Paul, R., & Chen, Y. (2005). Automated model checking and testing for composite web services. In Proceedings of ISORC\u201905 (pp. 300\u2013307). IEEE Computer Society. http:\/\/dx.doi.org\/10.1109\/ISORC.2005.16 .","DOI":"10.1109\/ISORC.2005.16"},{"key":"9152_CR22","unstructured":"Hull, R., Benedikt, M., Christophides, V., & Su, J. (2003). E-services: A look behind the curtain. In Proceedings of the twenty-second ACM SIGMOD-SIGACT-SIGART symposium on principles of database systems (pp. 1\u201314). NY: ACM Press. http:\/\/doi.acm.org\/10.1145\/773153.773154 ."},{"key":"9152_CR23","unstructured":"Jones, A. J. I., & Sergot, M. J. (1993). On the characterisation of law and computer systems: The normative systems perspective. In Deontic logic in computer science: Normative system specification (Chap. 12). UK: Wiley."},{"key":"9152_CR24","first-page":"36","volume-title":"Deontic logic: Introductory and systematic readings","author":"S. Kanger","year":"1971","unstructured":"Kanger S. (1971) New foundations for ethical theory. In: Hilpinen R. (eds) Deontic logic: Introductory and systematic readings. Reidel Publishing Company, Dordrecht, pp 36\u201358"},{"key":"9152_CR25","unstructured":"Kazhamiakin, R., Pistore, M., & Santuari, L. (2006). Analysis of communication models in web service compositions. In WWW (pp. 267\u2013276). NY: ACM Press."},{"issue":"1","key":"9152_CR26","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/BF03037383","volume":"4","author":"R. Kowalski","year":"1986","unstructured":"Kowalski R., Sergot M. (1986) A logic-based calculus of events. New Generation Computing 4(1): 67\u201395","journal-title":"New Generation Computing"},{"key":"9152_CR27","unstructured":"Lamanna, D. D., Skene, J., & Emmerich, W. (2003). Slang: A language for defining service level agreements. In FTDCS (pp. 100\u2013106). San Juan, Puerto Rico: IEEE Computer Society Press."},{"key":"9152_CR28","unstructured":"Lazovik, A., Aiello, M., & Papazoglou, M. (2004). Associating assertions with business processes and monitoring their execution. In ICSOC \u201904: Proceedings of the 2nd international conference on service oriented computing (pp. 94\u2013104). NY: ACM Press. http:\/\/doi.acm.org\/10.1145\/1035167.1035182 ."},{"key":"9152_CR29","unstructured":"Lomuscio, A., Qu, H., & Raimondi, F. (2009). Mcmas 0.9 beta. http:\/\/www.lai.doc.ic.ac.uk\/mcmas ."},{"key":"9152_CR30","unstructured":"Lomuscio, A., Qu, H., & Raimondi, F. (2009). MCMAS: A model checker for the verification of multi-agent systems. In Proceedings of CAV 2009. LNCS (Vol. 5643, pp. 682\u2013688). NY: Springer."},{"issue":"1","key":"9152_CR31","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1023\/A:1026176900459","volume":"75","author":"A. Lomuscio","year":"2003","unstructured":"Lomuscio A., Sergot M. (2003) Deontic interpreted systems. Studia Logica 75(1): 63\u201392","journal-title":"Studia Logica"},{"issue":"1","key":"9152_CR32","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/j.jal.2004.01.005","volume":"2","author":"A. Lomuscio","year":"2004","unstructured":"Lomuscio A., Sergot M. (2004) A formalisation of violation, error recovery, and enforcement in the bit transmission problem. Journal of Applied Logic 2(1): 93\u2013116","journal-title":"Journal of Applied Logic"},{"key":"9152_CR33","unstructured":"Lomuscio, A., & Wo\u017ana, B. (2006). A complete and decidable axiomatisation for deontic interpreted systems. In Proceedings of the 8th international workshop on deontic logic in computer science (DEON\u201906) (Vol. 4048, pp. 238\u2013254). NY: Springer."},{"key":"9152_CR34","doi-asserted-by":"crossref","unstructured":"Lomusico, A., Qu, H., & Solanki, M. (2008). Towards verifying contract regulated service composition. In Proceedings of IEEE international conference on web services (ICWS 2008) (pp. 254\u2013261). IEEE Computer Society.","DOI":"10.1109\/ICWS.2008.115"},{"key":"9152_CR35","volume-title":"Deontic logic in computer science: Normative system specification","year":"1993","unstructured":"Meyer, J. J. C., Wieringa, R. J. (eds) (1993) Deontic logic in computer science: Normative system specification. John Wiley, UK"},{"key":"9152_CR36","doi-asserted-by":"crossref","unstructured":"Mongiello, M., & Castelluccia, D. (2006). Modelling and verification of bpel business processes. In the 4th workshop on model-based development of computer-based systems and 3rd international workshop on model-based methodologies for pervasive and embedded software (pp. 144\u2013148). IEEE Computer Society.","DOI":"10.1109\/MBD-MOMPES.2006.22"},{"key":"9152_CR37","unstructured":"Morgan, G., Parkin, S., Molina-Jimenez, C., & Skene, J. (2006). Monitoring middleware for service level agreements in heterogeneous environments. Challenges of Expanding Internet: E-Commerce, E-Business, and E-Government."},{"key":"9152_CR38","unstructured":"OASIS Web service Business Process Execution Language (WSBPEL) TC. (2007). Web service business process execution language. Version 2.0."},{"key":"9152_CR39","unstructured":"OASIS Web Services Transaction (WS-TX) TC. (2009). Web services coordination (ws-coordination). Version 1.2."},{"issue":"2\u20133","key":"9152_CR40","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1016\/j.scico.2007.03.002","volume":"67","author":"C. Ouyang","year":"2007","unstructured":"Ouyang C., Verbeek E., van der Aalst W. M. P., Breutel S., Dumas M., ter Hofstede A. H. M. (2007) Formal semantics and analysis of control flow in ws-bpel. Science of Computer Programming 67(2\u20133): 162\u2013198","journal-title":"Science of Computer Programming"},{"key":"9152_CR41","unstructured":"Panagiotidi, S., Vazquez-Salceda, J., Alvarez-Napagao, S., Ortega-Martorell, S., Willmott, S., Confalonieri, R., et\u00a0al. (2008). Contracting agent language. In Symposium on behaviour regulation in multi-agent systems."},{"issue":"2","key":"9152_CR42","first-page":"167","volume":"55","author":"W. Penczek","year":"2003","unstructured":"Penczek W., Lomuscio A. (2003) Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55(2): 167\u2013185","journal-title":"Fundamenta Informaticae"},{"key":"9152_CR43","unstructured":"Pistore, M., Barbon, F., Bertoli, P., Shaparau, D., & Traverso, P. (2004). Planning and monitoring web service composition. In AIMSA (pp. 106\u2013115). NY: Springer."},{"key":"9152_CR44","unstructured":"Prisacariu, C., & Schneider, G. (2007). A formal language for electronic contracts. In Proceedings of FMOODSG07. LNCS (Vol. 4468, pp. 174\u2013189). NY: Springer."},{"issue":"1","key":"9152_CR45","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1016\/j.jlap.2006.05.007","volume":"70","author":"M. Mazzara","year":"2007","unstructured":"Mazzara M. (2007) A pi-calculus based semantics for ws-bpel. Journal of Logic and Algebraic Programming 70(1): 96\u2013118","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"9152_CR46","doi-asserted-by":"crossref","unstructured":"Robby, Dwyer, M. B., & Hatcliff, J. (2006). Bogor: A flexible framework for creating software model checkers. In TAIC PART, (pp. 3\u201322). IEEE Computer Society.","DOI":"10.1109\/TAIC-PART.2006.5"},{"key":"9152_CR47","unstructured":"Rouached, M., Perrin, O., & Godart, C. (2006). Towards formal verification of web service composition. In the 4th international conference on business process management (BPM06). LNCS (Vol. 4102, pp. 257\u2013273). NY: Springer."},{"key":"9152_CR48","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2004.11.011","volume":"126","author":"H. Schlingloff","year":"2005","unstructured":"Schlingloff H., Martens A., Schmidt K. (2005) Modeling and model checking web services. Electronic Notes in Theoretical Computer Science 126: 3\u201326","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"9152_CR49","unstructured":"Solaiman, E., Molina-Jim\u00e9nez, C., & Shrivastava, S. K. (2003). Model checking correctness properties of electronic contracts. In ICSOC (Vol. 2910, pp. 303\u2013318). NY: Springer."},{"key":"9152_CR50","unstructured":"Walton, C. D. (2004). Model\u2014checking multi-agent web services. In AAAI 2004: Spring symposium on semantic web services. Stanford, USA."},{"key":"9152_CR51","volume-title":"An introduction to multi-agent systems","author":"M. Wooldridge","year":"2002","unstructured":"Wooldridge M. (2002) An introduction to multi-agent systems. John Wiley, England"},{"issue":"2","key":"9152_CR52","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1142\/S0218213006002631","volume":"15","author":"M. Wooldridge","year":"2006","unstructured":"Wooldridge M., Huget M. P., Fisher M., Parsons S. (2006) Model checking for multiagent systems: The mable language and its applications. International Journal on Artificial Intelligence Tools 15(2): 195\u2013226","journal-title":"International Journal on Artificial Intelligence Tools"},{"key":"9152_CR53","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/j.entcs.2004.11.015","volume":"126","author":"B. Wozna","year":"2005","unstructured":"Wozna B., Lomuscio A., Penczek W. (2005) Bounded model checking for deontic interpreted systems. Electronic Notes in Theoretical Computer Science 126: 93\u2013114","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"9152_CR54","unstructured":"Fu, X., Bultan, T., & Su, J. (2003). Conversation protocols: A formalism for specification and verification of reactive electronic services. In CIAA. Volume of LNCS 2759 (pp. 188\u2013200). NY: Springer."}],"container-title":["Autonomous Agents and Multi-Agent Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10458-010-9152-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10458-010-9152-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10458-010-9152-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T21:44:14Z","timestamp":1740519854000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10458-010-9152-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9,17]]},"references-count":54,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,5]]}},"alternative-id":["9152"],"URL":"https:\/\/doi.org\/10.1007\/s10458-010-9152-3","relation":{},"ISSN":["1387-2532","1573-7454"],"issn-type":[{"value":"1387-2532","type":"print"},{"value":"1573-7454","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,9,17]]}}}