Practical verification of decision-making in agent-based autonomous systems

TLDR

Hybrid automata have traditionally been used to implement and verify hybrid systems, but their scalability deteriorates with complex discrete decision‑making, prompting a common practice of separating logical decision‑making into discrete components while verification methods have not kept pace. The authors aim to develop a verification methodology that analyzes the decision‑making component of agent‑based hybrid systems using a model‑checking technique that can be composed with continuous system analysis. They propose a model‑checking technique for agent‑based logical components that can be combined with a separate analysis of the continuous part of the hybrid system. The technique enables program model checkers to verify the actual implementation of decision‑making in hybrid autonomous systems.

Abstract

We present a verification methodology for analysing the decision-making component in agent-based hybrid systems. Traditionally hybrid automata have been used to both implement and verify such systems, but hybrid automata based modelling, programming and verification techniques scale poorly as the complexity of discrete decision-making increases making them unattractive in situations where complex logical reasoning is required. In the programming of complex systems it has, therefore, become common to separate out logical decision-making into a separate, discrete, component. However, verification techniques have failed to keep pace with this development. We are exploring agent-based logical components and have developed a model checking technique for such components which can then be composed with a separate analysis of the continuous part of the hybrid system. Among other things this allows program model checkers to be used to verify the actual implementation of the decision-making in hybrid autonomous systems.