https://www.mdu.se/

Driverless vehicles are becoming more and more popular in the area of construction equipment as they promise to ensure safety and industrial productivity by iteratively and automatically completing repetitive tasks. These vehicles are always travelling and working in an environment full of uncertainties, such as unforeseen static obstacles. In this thesis, our goal is to develop a method for correctness-guaranteed mission-plan synthesis for autonomous vehicles that meet specified requirements and apply the path-finding algorithm, i.e., Theta*, and a model-checking technique to ensure the correctness of the mission plan. The proposed approach is implemented in a tool called TAMAA (Timed-Automata-Based Planner for Multiple Autonomous Agents), which facilitates the use of formal modelling and verification techniques for mission-plan synthesis by a means of a user-friendly GUI. The tool is evaluated in various scenarios to demonstrate that it is able to synthesize mission plans that satisfy different kinds of requirements.