Deduktiver Entwurf, Analyse und Verifikation von Multiagenten-Systemen für den 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. Im Rahmen des Projekts wird ein Verfahren entwickelt, 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 Softwaretechnik (UML) eingesetzt werden. Damit ist in einem weiteren Schritt die Analyse und Verifikation von Multiagenten-Systemen durchführbar, indem Temporallogiken und Methoden aus dem Model Checking für den hier vorgesehenen Zweck (weiter) entwickelt werden.