Spiel-basierte Synthese für die industrielle Automatisierung

• Antragsteller: Dr. Chih-Hong Cheng; Dr. Michael Luttenberger
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2014 bis 2019
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 253384115

• Erstellungsjahr: 2019

Zusammenfassung der Projektergebnisse

Zentrale Fragestellungen waren die Entwicklung von effizienten Lösungsverfahren für die Synthese von Controllern aus gegebenen, praxisnahen quantitativen und qualitativen Spezifikationen basierend auf der Übersetzung dieser in ein Mehrpersonenspiel. Im ursprünglichen Antrag zusammen mit Herrn Cheng waren die genannte Problemstellungen speziell auf die Weiterentwicklung des von Herrn Cheng entwickelten Softwarewerkzeugs MGSyn für die Synthese von Controllern im Bereich der industriellen Automatisierung ausgerichtet. Da mit dem Weggang Herrn Chengs die treibende Kraft hinter MGSyn verloren gegangen war, wurden die im Projektantrag genannten Fragestellungen losgelöst von MGSyn untersucht. Die hierzu erlangten Ergebnisse lassen sich wie folgt kurz zusammenfassen (gegliedert nach den Arbeitspaketen aus dem Antrag): • Optimierung der Synthese-Algorithmen bzw. Löser für die zugrundeliegenden Spielen durch (a) statische Analyse zur Optimierung der formalen Spezifikation und (b) Parallelisierung der Löser: Für die Gruppe von Prof. Majid Zamani wurde der bereits vorhandene GPU-basierten Löser für Paritätsspiele auf quantitative Spiele mit Mean-Payoff und Discounted-Payoff erweitert. Dieser wurde in OpenCL implementiert, so dass er sowohl von GPUs als auch Mehrkern-CPUs Gebrauch machen kann. Er ist Teil eines Softwarewerkzeugs zur Optimierung von Controllern fuür hybride Systeme, welches in Kooperation mit der Gruppe von Prof. Zamani entwickelt wurde. Für das LTL-Synthese-Problem wurde das Softwarewerkzeug Strix entwickelt, welches einen innovativen Ansatz benutzt, um möglichst wenig der eigentlichen Übersetzung der LTL-Formel in ein Paritätsspiel durchzuführen. Strix selbst wurde von Anfang an so entwickelt, dass es von Mehrkern-Prozessoren sowohl im Übersetzungsschritt von LTL in das Spiel als auch bei der Lösung des Spiels Gebrauch machen kann. Sowohl bei der Übersetzung der LTL-Spezifikation in das Spiel als auch bei der Übersetzung der Gewinnstrategie in den eigentlichen Controller werden Techniken verwendet, um die Spezifikation zu vereinfachen und das Spiel und den Controller möglichst klein zu halten. • Sammlung von Benchmarks: Durch die Kooperation mit der Gruppe von Herr Zamani hat sich eine Sammlung von quantitativen Spielen ergeben, die direkt aus der Diskretisierung konkreter physikalischer Systeme, wie z.B. Klimaanlagen, stammen. Zur Evaluation von Strix wurde auf die Benchmarksammelung der Syntcomp zurückgegriffen. • Quantitative Spezifikationen, nichtdeterministische Strategien und stochastische Umgebungen: Wie bereits erwähnt, wurde der vorhandene GPU-basierte Löser für Paritätsspiele auf Spiele mit Mean-Payoff und Discounted-Payoff erweitert. Hierbei wurde aus der zu Grunde liegende Algorithmus basierend auf nichtdeterministischen Strategien entsprechend erweitert. Diese spielten ebenfalls im Fall von Strix eine wichtige Rolle: Der Nichtdeterminismus bietet bei der Übersetzung der Gewinnstrategie in den eigentlichen Controller (z.B. als Mealy-Automat oder als Schaltkreis) einen weiteren Freiheitsgrad zur Minimierung der Repräsentation, da die konkrete Aktion des Controllers so gewählt werden kann, dass die Übergangsrelation möglichst einfach darzustellen ist. • Synthese von verteilten Controllern: Zu diesem Arbeitspaket wurde auf Grund der Kürzung des Projekts keine Arbeit geleistet. • Fallstudie und Analyse der entwickelten Softwarewerkzeuge: Beide Softwarewerkzeuge wurden mit Hilfe der gesammelten Benchmarks evaluiert und die Resultate veröffentlicht. Der Löser für Spiele mit Mean-Payoff und Discounted-Payoff erlaubt auf Grund seiner Effizienz eine innovative Suche nach einem bezüglich des eigentlichen physikalischen Systems möglichst effizienten Controllers, selbst bei Diskretisierungen mit mehreren Millionen Zuständen. Strix hat überaus erfolgreich bei der Syntcomp 2018 in der Kategorie LTL-Synthese teilgenommen und dort in allen sechs Teilkategorien den ersten Platz belegt.

Projektbezogene Publikationen (Auswahl)

• “Solving Mean-Payoff Games on the GPU”. In: Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings. 2016, pp. 262–267
  Philipp J. Meyer and Michael Luttenberger
  
• “Quantitative Implementation Strategies for Safety Controllers”. In: CoRR abs/1712.05278 (2017)
  Philipp J. Meyer et al.
  
• “Strix: Explicit Reactive Synthesis Strikes Back!” In: Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. 2018, pp. 578–586
  Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger
  
• “Practical Synthesis of Reactive Systems from LTL Specifications via Parity Games”. In: CoRR abs/1903.12576 (2019)
  Michael Luttenberger, Philipp J. Meyer, and Salomon Sickert