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

• Antragsteller: Professor Dr. Bernd Finkbeiner; Professor Dr. Ernst-Rüdiger Olderog
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2018 bis 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 392735815

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.

• DFG-Verfahren: Sachbeihilfen