Modeling and verifying choreographed multi-agent-based web service compositions regulated by commitment protocols

Highlights：

• 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.