A Graphical User Interface for the Hybrid Control of Multi-Robot Systems under Linear Temporal Logic

In recent years the model checking theory was applied successfullyfor robot motion and task planning by specifying the workspace asa weighted finite transition system and tasks as linear temporal logicformulas. The tasks contain hard and soft-specifications which are assignedto an agent in a multi-robot system. The tasks are assigned aslocal tasks to an agent and are independent from each other.In this work a Graphical User Interface is presented to define a finitetransition system and specify tasks for each agent as linear temporallogic formulas. Furthermore, the presented GUI allows the user tosynthesize the robot motion and task plan. While an agent executesits motion plan, changes in the weighted finite transition system canbe applied and the agent performs a replanning. A new frameworkfor online task adaption is provided, which allows the user to sendtemporary tasks to an agent while executing its motion plan. In theend of the thesis some case studies are shown to demonstrate the newapproaches in simulation and also the functionality of the GUI in anexperiment. In the experiment the agents are able to avoid other agentsand even avoid moving human beings in the workspace.Under de senaste åren tillämpades modellkontrollteori framgångsrikt fö r robotrö relse och uppdragsplanering genom att ange arbetsrum som ett viktat finita ö vergångssystem och uppdragen som linjära tidsbestämd logikformler. Uppdraget innehåller hårda och mjuka specifikationer som tilldelas en agent i ett flerrobotsystem. Uppdragen är tilldelade som lokala uppdragen till en agent och är oberoende av varandra.‌I detta arbete presenteras ett grafiskt användargränssnitt fö r ett definierat finita ö vergångssystem och specificerar uppdrag fö r varje agen som linjära tidsbestämd logikformler. Dessutom tillåter den presenterade användargränssnitt användaren att syntetisera robotrö relsen och uppdragplanering. Medan en agent utfö r sin rö relseplan, kan ändringar i det viktat finita ö vergångssystemet appliceras och agent planerar om sin rö relse. Ett nytt ramverk fö r online uppdrag anpassning är given, vilket gö r det mö jligt fö r användare att skicka tillfälliga uppdraget till agent under tillfällen då agenten utfö r sin rö relseplan. I slutet av rapporten, visas några fallstudier som visar de nya metoderna i simuleringen och även funktionaliteten hos användaravsnitt i ett experiment. Det visar sig att agenterna undvika andra medel och till och med und-vika människor under rö relse i arbetsytan