REMASTER: Formale Modellierung der Umgebung in MAS

Multiagentensysteme (MAS) bestehen aus mehreren interagierenden Entitäten, die gemeinsame oder individuelle Ziele verfolgen. Agenten können hierbei Software-Module, Menschen oder Roboter sein. Daher finden sich MAS in allen Bereichen unserer heutigen technologisierten Gesellschaft, wie zum Beispiel unbemannten Fahrzeugen, Cloud Computing oder peer-to-peer Netzwerken. Zusätzlich können auch biologische Systeme auf natürlich Weise durch MAS beschrieben werden. Agenten agieren üblicherweise in einer Umgebung, wie zum Beispiel physikalischen (Roboter in einer Fabrik) oder virtuellen Räumen (Computernetzwerke). Nachdem der Schwerpunkt anfangs eher auf dem experimentellen Design von Systemen mit einem oder mehreren Agenten gelegen hat, hat sich das Feld weiterentwickelt zu einem rigorosen und theoretischen Design basierend auf fortgeschrittenen computationalen Modellen. Um die Korrektheit von MAS zu analysieren, hat die MAS Forschung begonnen Formale Methoden einzusetzen - mathematische Werkzeuge basierend auf Logik und ähnlichen mathematischen Formalismen, welche extrem erfolgreich eingesetzt wurden um alle möglichen Verhaltensweisen eines Systemmodells zu untersuchen (z.B. für moderne Mikroprozessoren) was mit Standardtechniken wie Testen nicht möglich wäre. In klassischen Formalen Methoden, kann ein Programm entweder korrekt sein oder nicht. In der Praxis kann man ein Programm gegenüber einem anderen bevorzugen kann, obwohl beide korrekt sind: ein Programm ist schneller, effizienter, oder robuster. Das Beurteilen solcher quantitativen Kriterien ist Gegenstand aktueller Forschung im Bereich der Formalen Methoden. Der Einsatz ähnlicher quantitativer Kriterien für MAS ist äußerst vielversprechend. Insbesondere, sollten MAS bezüglich ihrer Umgebungen robust sein: MAS sollen Ungenauigkeiten in der Umgebung tolerieren sowie sich auf Änderungen in der Umgebung einstellen können. Wir veranschaulichen diese Anforderung am Beispiel der selbstfahrenden Fahrzeuge von google. Diese Fahrzeuge benützen "Super-Karten", welche die Straßenumgebung in 3D, vollständig und digital, enthalten, mit einer Genauigkeit von wenigen Zentimetern. Diese Karten liefern genaue Informationen über die Position von Bordsteinen und Ampelanlagen auf der Straße, wiederum präzise in 3D. Allerdings können diese Fahrzeuge nicht mit Veränderungen umgehen, wie beispielsweise temporären Ampelanlagen, da die Software in ihrem Basismodus eine vollständig bekannte und statische Umgebung voraussetzt. Demgegenüber ist ein menschlicher Fahrer in der Lage sich auf unbekannte und veränderte Umgebungen einzustellen. Bislang gibt es nur sehr wenige Forschungsarbeiten, die Formale Methoden einsetzen um MAS, die robust in Bezug auf ihre Umgebung sind, zu analysieren oder synthetisieren (d.h. das System automatisch aus der Spezifikation generieren). Ziel dieses Projektes ist es diese Lücke zu schließen und Formale Methoden zu entwickeln, die es erlauben die Korrektheit von MAS bezüglich nur teilweise bekannter und dynamischer Umgebungen zu beurteilen, um damit der Anforderung an dem automatischen und gründlichen Design korrekter und zuverlässiger MAS gerecht zu werden.

Ein zentrales Thema in der künstlichen Intelligenz (KI) dreht sich um das Konzept des Agenten, womit man jede Entität bezeichnet, die mit anderen Agenten und/oder der Umwelt via Sensoren und Aktoren interagieren kann und von der Notwendigkeit oder dem Wunsch geleitet wird, ein bestimmtes Ziel zu erreichen oder eine bestimmte Aufgabe zu erfüllen. Ein System, das aus einer Gruppe solcher Agenten besteht, nennt man ein Multi-Agentensystem (MAS). Beispiele hierfür sind Software-Agenten im Internet, fahrerlose Autos, Menschen oder Software-Programme, die Kartenspiele mit mehreren Spielern spielen, und Roboter die neue und gefährliche gefährliche Umgebungen erkunden. In all diesen Beispielen sind die Agenten in einer Umgebung verortet und werden von dieser Umgebung unterstützt, die erst die Bedingungen für die Existenz und die Arbeit der Agenten schafft. Wichtige Aspekte einer Umgebung sind beispielsweise die physische Umgebung, die die Agenten physisch verortet (z. B. physische Straßen, Netzwerkverbindungen); eine Kommunikationsumgebung, die die Kommunikation der Agenten ermöglicht (z. B. Regeln, Mittel und Protokolle); oder eine soziale Umgebung, die die Organisationsstruktur in Form von Rollen, Gruppen usw. widerspiegelt. Der immer stärkere Einsatz von KI-Agenten in unserer Gesellschaft und die damit verbundenen Schwierigkeiten, solche Agenten so zu gestalten, dass sie in den komplexen Umgebungen, in denen sie eingesetzt werden, sicher und korrekt arbeiten, hat in letzter Zeit zu der Erkenntnis geführt, wie wichtig es ist Werkzeuge und Techniken formaler Methoden einzusetzen für den Entwurf und die Analyse von künstlichen Agenten und ihrer Interaktionen mit ihrer Umgebung. Formale Methoden stellen Methoden bereit, welche hauptsächlich auf Logik und Automaten basieren, um automatisch zu bestimmen, ob ein mathematisches Modell eines Systems eine Spezifikation erfüllt die in mathematischer Logik ausgedrückt werden kann (Modellprüfung), oder, alternativ, automatisch ein System zu konstruieren, das eine gegebene Spezifikation erfüllt (Synthese). Die zentralen Ergebnisse dieses Projekts waren die Entwicklung neuer Formaler Methoden zur Analyse von Agenten, die in komplexen Umgebungen agieren: zum Beispiel neuartige Algorithmen zur Modellprüfung von MAS, die in Umgebungen mit unbekannter physikalischer Infrastruktur Infrastruktur operieren, und eine neue Spezifikationslogik namens Probabilistic Strategy Logic für die Analyse von MAS, die in stochastischen Umgebungen operieren. Außerdem wurden Kernfragen - wie man die Umgebung am besten modellieren sollte - neu betrachtet, und wichtige Erkenntnisse und neue Synthesealgorithmen wurden erzielt. Außerdem wurde eine neue vielversprechende Forschungsrichtung, die Best-Effort-Synthese, initiiert (und grundlegende Ergebnisse hierzu erzielt). Die grundlegende Frage hierbei ist, was ein Agent tun sollte, wenn er nicht sicherstellen kann, dass er sein Ziel erreicht, unabhängig davon, wie sich die Umwelt verhält.