Multi-agent systems: Modeling andVerification using Hybrid Automata

Hybrid automata are used as standard means for the specification andanalysis of dynamical systems. Several researches have approached them to formallyspecify reactive Multi-agent systems situated in a physical environment,where the agents react continuously to their environment. The specified systems,in turn, are formally checked with the help of existing hybrid automata verificationtools. However, when dealing with multi-agent systems, two problems maybe raised. The first problem is a state space problem raised due to the compositionprocess, where the agents have to be parallel composed into an agent capturing allpossible behaviors of the multi-agent system prior to the verification phase. Thesecond problem concerns the expressiveness of verification tools when modelingand verifying certain behaviors. Therefore, this paper tackles these problemsby showing how multi-agent systems, specified as hybrid automata, can be modeledand verified using constraint logic programming(CLP). In particular, a CLPframework is presented to show how the composition of multi-agent behaviorscan be captured dynamically during the verification phase. This can relieve thestate space complexity that may occur as a result of the composition process.Additionally, the expressiveness of the CLP model flexibly allows not only tomodel multi-agent systems, but also to check various properties by means of thereachability analysis. Experiments are promising to show the feasibility of ourapproach.[...]