Pushing the Barriers in Controller Synthesis for Cyber-Physical Systems

  • Controller design for continuous dynamical systems is a core algorithmic problem in the design of cyber-physical systems (CPS). When the CPS application is safety critical, additionally we require the controller to have strong correctness guarantees. One approach for this design problem is to use simpler discrete abstraction of the original continuous system, on which known reactive synthesis methods can be used to design the controller. This approach is known as the abstraction-based controller design (ABCD) paradigm. In this thesis, we build ABCD procedures which are faster and more modular compared to the state-of-the-art, and can handle problems which were beyond the scope of the existing techniques. Usually, existing ABCD approaches use state space discretization for computing the abstractions, for which the procedures do not scale well for larger systems. Our first contribution is a multi-layered ABCD algorithm, where we combine coarse abstractions and lazily computed fine abstractions to improve scalability. So far, we only address reach-avoid and safety specifications, for which our prototype tool (called Mascot) showed up to an order of magnitude speedup on standard benchmark examples. Second, we consider the problem of modular design of sound local controllers for a network of local discrete abstractions communicating via discrete/boolean variables and having local specifications. We propose a sound algorithm, where the systems negotiate a pair of local assume-guarantee contracts, in order to synchronize on a set of non-conflicting and correct behaviors. As a by-product, we also obtain a set of local controllers for the systems which ensure simultaneous satisfaction of the local specifications. We show the effectiveness of the our algorithm using a prototype tool (called Agnes) on a set of discrete benchmark examples. Our third contribution is a novel ABCD algorithm for a more expressive model of nonlinear dynamical systems with stochastic disturbances and ω-regular specifications. This part has two subparts, which are of significant merits on their own rights. First, we present an abstraction algorithm for nonlinear stochastic systems using 2.5-player games (turn-based stochastic graph games). We show that an almost sure winning strategy in this abstract 2.5-player game gives us a sound controller for the original system for satisfying the specification with probability one. Second, we present symbolic algorithms for a seemingly different class of 2-player games with certain environmental fairness assumptions, which can also be used to efficiently compute winning strategies in the aforementioned abstract 2.5-player game. Using our prototype tool (Mascot-SDS), we show that our algorithm significantly outperforms the state-of-the-art implementation on standard benchmark examples from the literature.
  • Ein zentrales algorithmisches Problem beim Entwurf sicherheitskritischer cyber-physikalischer Systeme (CPS) ist die vollautomatische Synthese von garantiert korrekter Regelsoftware für Systemkomponenten mit kontinuierlicher Dynamik und diskreten Spezifikationen. Ein vielversprechender Ansatz um dieses Problem zu lösen ist der sogenannte abstraktionsbasierte Reglerentwurf (engl. Abstraction-Based Control Design (ABCD)). In ABCD wird die kontinuierliche Systemdynamik zunächst durch diskrete Abstraktionen approximiert. Auf Basis dieser Abstraktionen wird dann mit Hilfe von Algorithmen aus der (diskreten) reaktiven Synthese ein korrekter Regler für die gegebene diskrete Spezifikation synthetisiert, welcher dann in einen Regler für das Orginalproblem verfeinert werden kann. In dieser Arbeit befassen wir uns im Wesentlichen mit zwei Unzulänglichkeiten von ABCD. Zum einen nehmen wir uns der Herausforderungen bei der Skalierbarkeit von ABCD-Techniken an. Zum anderen erweitern wir ABCD auf ausdrucksstärkere Modelle, welche immer noch eine Synthese bezüglich ω-regulärer Spezifikationen zulassen. Insbe- sondere schlagen wir eine neue ABCD-Technik für kontinuierliche nichtlineare dynamische Systeme mit stochastischen Störungen vor. Unser Beitrag zu Skalierbarkeit und Expressivität von ABCD ist in drei Hauptteile gegliedert. Unser erster Beitrag ist ein mehrschichtiger ABCD-Algorithmus für verbesserte Skalierbarkeit. Viele bestehende Ansätze verwenden eine Diskretisierung des Zustandsraums zur Berechnung der Abstraktion, was einen schwerwiegenden rechnerischen Engpass darstellt. In unserem mehrschichtigen Ansatz kombinieren wir grobe Abstraktionen und lokal berechnete feine Abstraktionen, um die Skalierbarkeit zu verbessern. Bislang haben wir diese Methode nur für eingeschränkten Spezifikationsklassen entwickelt, welche in einem Prototyp (genannt Mascot) implementiert sind. Im Vergleich zu anderen ABCD-Algorithmen ist Mascot bei der Reglerberechnung für standardisierte Benchmark-Beispiele bis zu eine Größenordnung schneller. Der zweite Beitrag dient ebenfalls der besseren Skalierbarkeit, und schlägt einen Algorithmus für das (diskrete) verteilte reaktive Syntheseproblem vor. Dieser Algorithmus kann für den skalierbaren und modularen Entwurf lokaler Regler in einem Netzwerk lokaler diskreter Abstraktionen, die über diskrete/boolesche Variablen kommunizieren und lokale Spezifikationen haben, verwendet werden. Wir schlagen einen Algorithmus vor, bei dem die abstrakten Systeme lokal und dezentral Verträge untereinander aushandeln, und sich damit auf eine Reihe von konfliktfreien und korrekten Verhaltensweisen einigen. Wir zeigen die Anwendbarkeit unseres Algorithmus anhand eines Prototyps (genannt Agnes) an einer Reihe von diskreten Benchmark-Beispielen. Der dritte Beitrag ist, wie bereits erwähnt, ein neuartiger ABCD-Algorithmus für nichtlinearer dynamischer Systeme mit stochastischen Störungen und ω-regulären Spezifikationen. Dieser Teil hat zwei Unterabschnitte, die für sich genommen von großem Wert sind. Zuerst stellen wir einen Abstraktionsalgorithmus für nichtlineare stochastische Systeme unter Verwendung von 2.5-Spieler-Spielen (rundenbasierte stochastische Graphenspiele) vor. Wir zeigen, dass eine Gewinnstrategie in diesem abstrakten 2.5-Spieler-Spiel in einen korrekten Regler für das Orginalsystem verfeinert werden kann. Danach entwickeln wir symbolische Algorithmen für eine scheinbar andere Klasse von 2-Spieler-Spielen mit bestimmten Fairness-Annahmen. Diese Algorithmen können allerdings auch zur effizienten Berechnung von Gewinnstrategien in dem oben erwähnten abstrakten 2.5-Spiel verwendet werden. Mit Hilfe unseres Prototyps (Mascot-SDS) zeigen wir, dass die Kombination beider Algorithmen den Stand der Technik deutlich übertrifft.

Download full text files

Export metadata

Metadaten
Author:Kaushik MallikORCiD
URN:urn:nbn:de:hbz:386-kluedo-68668
DOI:https://doi.org/10.26204/KLUEDO/6866
Advisor:Rupak Majumdar
Document Type:Doctoral Thesis
Language of publication:English
Date of Publication (online):2022/06/30
Date of first Publication:2022/06/30
Publishing Institution:Technische Universität Kaiserslautern
Granting Institution:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2022/06/24
Date of the Publication (Server):2022/07/01
Tag:Abstraction-Based Controller Design; Correct-by-Design Controller Synthesis; Cyber-Physical Systems
Page Number:XII, 221
Faculties / Organisational entities:Kaiserslautern - Fachbereich Informatik
CCS-Classification (computer science):D. Software / D.0 GENERAL
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Creative Commons 4.0 - Namensnennung, nicht kommerziell, keine Bearbeitung (CC BY-NC-ND 4.0)