Modeling and verifying choreographed multi-agent-based web service compositions regulated by commitment protocols
Modeling multi-agent based web services using commitment protocols formalized as guarded automata with certain variables. Defining formal semantics for conditional commitments and associated actions for agent communication. Introducing a formal specification language of commitment protocols. Developing a symbolic model checking algorithm for the verification of web services composition. Computing the space complexity of the developed algorithm.
verification commitment protocols conditional commitments symbolic model checking multi-agent systems agent-based web services