Towards verifying compliance in agent-based web service compositions

We explore the problem of specification and verification of compliance in agent based Web service compositions. We use the formalism of temporal-epistemic logic suitably extended to deal with compliance/violations of contracts. We illustrate these concepts using a motivating example where the behaviours of participating agents are governed by contracts. The composition is specified in OWL-S and mapped to our chosen formalism. Finally we use an existing symbolic model checker to verify the example specification whose state space is approximately 221 and discuss experimental results. Categories and Subject Descriptors D.2.4 [Software/Program Verification]: Model checking; H.3.5 [Online Information Services]: Web-based services General Terms Verification Keywords Web services, Model checking, compliance, epistemic logic.

• Type: Conference
• Year: 2008
• Where: ATAL
• Authors: Alessio Lomuscio, Hongyang Qu, Monika Solanki
• Keywords: ATAL 2008, Intelligent Agents, Model Checking, Terms Verification Keywords, Web Services