Navigation

Skiplinks

Kontakt

Petri-Spiele: Ein semantischer und algorithmischer Ansatz für die effiziente Synthese von verteilten reaktiven Systemen

Projektbeschreibung

Projektleitung: E.-R. Olderog und B. Finkbeiner

Projektdauer: 01.08.2018 bis 31.07.2021

Finanzierung durch: DFG

Das Syntheseproblem für reaktive Systeme geht von einer Spezifikation eines reaktiven Systems
aus und fragt nach einer Implementierung, welche die Spezifikation für jedes mögliche Verhalten
der Umgebung erfüllt. Eine besonders interessante Version dieses Problems mit großem Potential
für praktische Anwendungen ist die Synthese von verteilten Systemen, die aus vielen nebenläufigen
Prozessen bestehen. Bislang sind die meisten Resultate für die Synthese von verteilten Systemen
jedoch negativ. In den beiden prominentesten Ansätzen (dem Modell von Pnueli und Rosner sowie
den asynchronen Automaten von Zielonka) hat verteilte Synthese eine extrem hohe Komplexität
(nicht-elementar) oder ist sogar unentscheidbar. Das Ziel dieses Projekts ist, einen neuen Ansatz für
die verteilte Synthese zu entwickeln, in dem das Syntheseproblem in akzeptabler Komplexität zu
lösen ist und der gleichzeitig ausdrucksstark genug ist, um die Synthese von realistischen verteilten
Systemen zu ermöglichen.


Der hier vorgeschlagene Ansatz basiert auf Petri-Spielen, einer spieltheoretischen Erweiterung
von Petri-Netzen. In Vorarbeiten haben wir gezeigt, dass die Syntheseprobleme von Herstellungs-
und Arbeitsablaufszenarien als Petri-Spiele modelliert werden können. Wir haben ebenfalls gezeigt,
dass unter bestimmten Voraussetzungen die gewinnende Strategie eines Petri-Spiels, welche einer
verteilten Implementierung entspricht, effizient bestimmt werden kann. Das Ziel dieses Projektes wird
erreicht, indem Petri-Spiele zu einem vollständigen Framework für die Synthese verteilter Systeme
erweitert werden. Die vorgeschlagene Arbeit zielt auf die semantischen Grundlagen von Petri-Spielen
und effiziente Algorithmen zur Lösung von Petri-Spielen ab. Die semantischen Erweiterungen
werden Petri-Spiele ausdrucksstärker, kompakter und dadurch für realistische verteilte Systeme
anwendbar machen. Die neuen Algorithmen werden die existierenden Algorithmen verallgemeinern
und dabei insbesondere die semantischen Erweiterungen umsetzen und gleichzeitig eine akzeptable
Komplexität beibehalten. Wir werden unseren Ansatz in zwei realistischen Anwendungsgebieten
evaluieren, die bislang für Synthese unerreichbar sind: intelligente Fabriken und automatische
Zugangskontrollsysteme in großen Gebäuden.

Insgesamt wird dieses Projekt den ersten praktischen Syntheseansatz für verteilte Systeme,
einschließlich der nötigen Spielmodelle, Algorithmen und Implementierungen, entwickeln. Wir
erwarten, dass unsere Realisierung von verteilter Synthese über das unmittelbare Forschungsgebiet
der Synthese hinaus Einfluss auf Gebiete wie Semantik, verteilte Systeme und autonome Systeme
haben wird.

Wissenschaftliche Mitarbeit: M. Gieseking und J. Hecking-Harbusch

Webmaster (Stand: 10.09.2018)