Křetínský, Jan (Prof. Dr.); Guldstrand Larsen R, Kim (Prof.); Althoff, Matthias (Prof. Dr.)
Sprache:
en
Fachgebiet:
DAT Datenverarbeitung, Informatik
Stichworte:
Quantitative Verification, Model Checking, Controller Synthesis, Markov Decision Process, Controller Representation, Decision Tree
TU-Systematik:
DAT 500d
Kurzfassung:
Quantitative model checking and controller synthesis deal with the task of automatically synthesizing reliable controllers for safety-critical systems. We address the state-space explosion challenge and present two distinct algorithms based on partial exploration for discrete as well as continuous-time Markov decision processes. Further, we present the first results on representing controllers of probabilistic and hybrid systems concisely and explainably using decision trees.
Übersetzte Kurzfassung:
Quantitative Modellüberprüfung und Reglersynthese befassen sich mit der Aufgabe, zuverlässige Regler für sicherheitskritische Systeme automatisch zu synthetisieren. Wir befassen uns mit der Herausforderung der Zustandsraumexplosion und stellen zwei verschiedene Algorithmen vor, die auf der partiellen Erkundung von diskreten bzw. zeitkontinuierlichen Markov-Entscheidungsprozessen basieren. Darüber hinaus präsentieren wir die ersten Ergebnisse zur Darstellung von Reglern probabilistischer und hybrider Systeme knapp und erklärbar mithilfe von Entscheidungsbäumen.
«
Quantitative Modellüberprüfung und Reglersynthese befassen sich mit der Aufgabe, zuverlässige Regler für sicherheitskritische Systeme automatisch zu synthetisieren. Wir befassen uns mit der Herausforderung der Zustandsraumexplosion und stellen zwei verschiedene Algorithmen vor, die auf der partiellen Erkundung von diskreten bzw. zeitkontinuierlichen Markov-Entscheidungsprozessen basieren. Darüber hinaus präsentieren wir die ersten Ergebnisse zur Darstellung von Reglern probabilistischer und hybr...
»