UnivIS
Informationssystem der Friedrich-Alexander-Universität Erlangen-Nürnberg © Config eG 
Modellbasierter Entwurf und Analyse kooperierender autonomer Agenten

Dieses Vorhaben befasst sich mit der Entwicklung und Erprobung neuer Ansätze zur Spezifikation und Verifikation sicheren kooperativen Verhaltens autonomer Agenten, etwa Roboter oder autonom fahrender Autos. Nachdem in früheren Vorhaben allgemeine Fragestellungen untersucht wurden, nämlich

• Überdeckungskriterien für das gesamte kooperative Verhalten und zugehörige Testfallgenerierung zur Erzielung dieser Kriterien (s. R3-COP) sowie
• Bewertung der Zuverlässigkeit kooperativen Verhaltens und zugehörige Testfallgenerierung zur Durchführung statistischen Testens (s. R5-COP)

wendet sich dieses weitere Vorhaben an die Untersuchung besonderer Ausprägungen des potentiellen kooperativen Verhaltens, etwa um

• das Auftreten vorgegebener sicherheitskritischer Szenarien nach Möglichkeit von vornherein auszuschließen,
• die Möglichkeit eines solchen Auftretens durch dedizierte Testfälle vor dem Betrieb aufzuspüren und durch angemessene Korrektur künftig zu eliminieren,
• die rechtzeitige Erkennung potentiell kritischer Zustände im Betrieb zu unterstützen und passende Reaktionen auf vordefinierten Rückfallebenen automatisch einzuleiten.

Teilprojekt 1: Verifikation bzw. Falsifikation sicherheitsrelevanter Eigenschaften kooperativen Verhaltens

In diesem Teilprojekt werden modellbasierte Ansätze zur Erkennung von Verletzungen von Kooperations- bzw. Koexistenzeigenschaften untersucht. Hierzu wurde folgendes beispielhafte Agentensystem betrachtet, das aus 2 Robotern besteht, die Transportmissionen autonom übernehmen; hierbei ist jede Transportmission definiert durch

• eine zu transportierende Menge nicht weiter spezifizierten Materials und
• eine Missionspriorität.

Die Transportmission gilt genau dann als erfolgreich abgeschlossen, wenn das zu transportierende Material an der einzig vorhandenen Entladestation entladen wurde. Selbstverständlich dürfen Entladevorgänge nicht zur Überladung der Entladestation führen. Zur Gewährleistung dieser sicherheitsrelevanten Eigenschaft hat jeder Roboter vor Auslösung der Entladung zu überprüfen,

• ob die eigene Entladung zu einer Überladung der Station führen kann und
• ob ein auf einem angrenzenden Parksegment stehender Roboter mit einer höher priorisierten Mission ebenfalls die Möglichkeit der Entladung überprüft.

Dann und nur dann, wenn beide Bedingungen nicht erfüllt werden, wird die Entladung initiiert.

Um obige Kriterien zu evaluieren erfährt jeder Roboter

• über entsprechende Sensoren die aktuelle Kapazität der Entladestation und
• über ein Display die Priorität der Mission eines benachbarten Roboters.

Die auf die Kooperation der beiden Roboter begrenzte Anwendung soll anschließend auf die Koexistenz von 3 Robotern erweitert werden. Es war deshalb zu analysieren, inwieweit bei unveränderter Verhaltensspezifikation diese Erweiterung zu einer Verletzung der betrachteten Sicherheitseigenschaft führen kann. Hierzu wurde der im abgeschlossenen Projekt „Modellbasierte Verifikation relevanter Eigenschaften komplexer Softwaresysteme mittels heuristischer Testverfahren“ entwickelte Ansatz zur Falsifikation universeller temporallogischer CTL-Formeln eingesetzt. Dieser Ansatz erforderte zunächst die Modellierung des Gesamtverhaltens durch eine erweiterte endliche Zustandsmaschine, die als Kreuzprodukt von 4 einzelnen erweiterten Zustandsmaschinen (jeweils eine für jeden der 3 Roboter sowie eine vierte für die Entladestation) konstruiert wurde. Auf dieser Basis konnte der entwickelte Ansatz Eingangsdaten finden, die zu einem betrieblichen Szenario führen, in dem die Sicherheitseigenschaft verletzt wird. Somit konnte nachgewiesen werden, dass die Erweiterung des Agentensystems eine Anpassung der ursprünglichen Verhaltensspezifikation erforderlich macht.

Teilprojekt 2: Selbstreflektierende Anpassung der Autonomiegrade kooperierender Agenten

Im Vergleich zu traditionellen zentralisierten Systemen stellen kooperierende autonome Agenten-Systeme bekanntlich zusätzliche Herausforderungen: zum einen können sich Aktionen eines Agenten auf Nachfolgeentscheidungen weiterer Agenten auswirken; zum anderen sind die Agenten meist nicht in der Lage, die Aktionen der anderen Agenten vorauszusagen. Eine systematische, optimale und sicherheitsgerichtete Entscheidungsfindung mag daher u. U. (etwa infolge nur unvollständig verfügbarer Informationen) nicht möglich sein, wodurch das Auftreten kritischer Situationen nicht im Voraus ausgeschlossen werden kann.

Im Rahmen dieses Forschungsprojektes wird untersucht, inwieweit kritische Situationen sich dadurch vermeiden bzw. reduzieren lassen, dass die einzelnen Agenten zeitweise einen Teil ihrer Autonomie an eine zentrale Instanz abgeben. Diese zentrale Instanz überwacht die Aktionen der einzelnen Agenten; darauf basierend, muss sie in der Lage sein, das potentielle Auftreten einer kritischen Situation zu erkennen und als Gegenmaßnahme in die Autonomie der Agenten einzugreifen, indem sie diesen die als nächstes auszuführende Aktion vorgibt (um somit die kritische Situation zu vermeiden).

In einem ersten Schritt wurde untersucht, wie die internen Zustände des Agentensystems in Abhängigkeit vom Bedarf einer angemessenen Intervention seitens der zentralen Instanz, sowie von der Art der geforderten Intervention klassifiziert werden können.

Projektleitung:
Prof. Dr. rer. nat. habil. Francesca Saglietti

Beteiligte:
Xiaochen Wu, M.Sc., Dr.-Ing. Marc Spisländer

Laufzeit: 1.1.2018 - 31.12.2018

UnivIS ist ein Produkt der Config eG, Buckenhof