Towards verifying compliance in agent-based web service compositions
Alessio R. Lomuscio, Hongyang Qu, Monika Solanki · 2008
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 2 21 and discuss experimental results. Categories and Subject Descriptors D.2.4 [Software/Program Verification]: Model checking; H.3.5 [Online Information Services]: Web-based