Deductive design, analysis and verification of multi-agent systems for RoboCup

点击翻译按钮获取中文摘要

Die Erstellung von Software für kooperierende Teams mobiler Roboter stellt hohe Anforderungen. Zum einen muss eine Reaktion des Systems in Echtzeit garantiert werden und zum anderen erhöht die Kooperation mehrerer Agenten miteinander die Komplexität. Formale Methoden zu Entwurf, Analyse und Verifikation von Multiagenten-Systemen existieren bisher kaum. Wir wollen ein Verfahren entwickeln, welches es erlaubt, Multiagenten-Systeme formal zu entwerfen und diesen Entwurf auch ausführbar zu machen. Hierzu sollen Techniken aus der Deduktion und Logikprogrammierung und Mittel der Unified Modelling Language (UML) eingesetzt werden. Damit ist in einem weiteren Schritt die Analyse und Verifikation von Multiagenten-Systemen durchführbar, indem Temporal- bzw. dynamische Logiken und Methoden aus dem Model Checking für den hier vorgesehenen Zweck (weiter) entwickelt werden. Insgesamt ist so ein Systementwurf möglich, der in Systeme mobiler Roboter integriert werden kann. Dies soll konkret für die RoboCup-Simulation sowie für echte Roboter vom Typ Sony Aibo Dog durchgeführt werden. Am Ende dieses Projekts steht ein System, das neben dem Entwurf und der Implementierung eines Multiagenten-Systems kooperierender mobiler Roboter auch dessen formale Analyse und Verifikation erlaubt.