TAMAA: UPPAAL-based mission planning for autonomous agents

Autonomous vehicles, such as construction machines, operate in hazardous environments, while being required to function at high productivity. To meet both safety and productivity, planning obstacle-avoiding routes in an efficient and effective manner is of primary importance, especially when relying on autonomous vehicles to safely perform their missions. This work explores the use of model checking for the automatic generation of mission plans for autonomous vehicles, which are guaranteed to meet certain functional and extra-functional requirements, e.g., timing ones. We propose a model of autonomous vehicles as agents in timed automata together with monitors for supervising their behavior in time, for instance battery level. We automate this approach by implementing it in a tool called TAMAA (Timed-Automata-based Planner for Multiple Autonomous Agents) and integrating it with a mission-management tool. We demonstrate the applicability of our approach on an industrial autonomous wheel loader use case.