Modelling and Verification of Multi-agent Hybrid Systems

Multi-agent hybrid systems are widely seen in applications such as highly autonomous vehicles, robotics and telecommunication networks, distributed real-time systems, distributed artificial intelligence, surveillance systems, industrial control systems, power systems and smartgrids, coordinated defence systems, and healthcare. Multi-agent hybrid systems are often safety-critical, where ensuring the operational correctness is absolutely necessary. Examples of safety-critical multi-agent hybrid systems are autonomous vehicles, systems in healthcare such as insulin infusion pumps, and so on. Due to this safety-critical nature, the formal verification of multi-agent hybrid systems becomes necessary to ensure their correctness and integrity. In this work, we study the mathematical modelling of such systems by hybrid automaton and by the parallel composition of hybrid automata. Subsequently, we study the usage of model-checking tools for multi-agent hybrid systems, particularly Verse and SpaceEx, for their simulation and verification. We then address two exercises in modelling of multi-agent hybrid systems. Firstly, we propose two hybrid models to achieve clock synchronization in swarm robotic systems via pulse coupling, verify whether a global synchronization is at all achieved, and compare it with existing models in literature. Secondly, we model Dijkstra's k-state solution to the self-stabilizing token ring problem as a multi-agent hybrid system and prove its convergence for a specific case using formal verification techniques. Then, we study the model checking via reachability analysis approach to formal verification of multi-agent hybrid systems, and propose a path-oriented reachability analysis algorithm within the framework of the Verse library.