For safety-critical applications, model checking tools can verify safety criteria of systems and synthesize correct-by-design controllers. Instead of representing these controllers with huge lookup tables or hard-to-understand binary decision diagrams, recent work tried to find succinct and explainable representations with decision trees. To describe complex systems with small trees, recent efforts used more expressive algebraic predicates in the decision nodes. However, until now, there has not been a way of automatically generating those. In this thesis, we propose two solutions: The first one generates predicates from given domain knowledge. The second one learns polynomial expressions from the controller data using support vector machines. We implement the second approach into the open-source tool dtcontrol and evaluate it on 28 case studies. For many cases, we see a significant size reduction and for 10 case studies, we even reach the minimum decision tree size.     «

For safety-critical applications, model checking tools can verify safety criteria of systems and synthesize correct-by-design controllers. Instead of representing these controllers with huge lookup tables or hard-to-understand binary decision diagrams, recent work tried to find succinct and explainable representations with decision trees. To describe complex systems with small trees, recent efforts used more expressive algebraic predicates in the decision nodes. However, until now, there has not...     »

Für sicherheitsrelevante Anm Sicherheitspezifikationen zu verifizieren und beweisbar korrekte Controller zu synthetisieren. Anstatt diese Controller mit riesigen Lookup-Tabellen oder schwer verständlichen binären Entscheidungsdiagrammen darzustellen, wurden in jüngsten Forschungsarbeiten Entscheidungsbäumen benutzt, um prägnante und erklärbare Darstellungen zu finden. Um komplexe Systeme mit kleinen Bäumen zu beschreiben, werden in neueren Arbeiten aussagekräftigere algebraische Prädikate in den Entscheidungsknoten verwendet. Bislang gab es jedoch keine Möglichkeit, diese automatisch zu generieren. In dieser Arbeit schlagen wir zwei Lösungen vor: Die erste generiert Prädikate aus gegebenem Expertenwissen. Die zweite lernt polynomielle Ausdrücke aus den Daten des Controllers mit Hilfe von Support Vector Machines. Wir integrieren den zweiten Ansatz in die Open-Source-Anwendung dtcontrol und evaluieren ihn anhand 28 Fallstudien. Für viele Fälle sehen wir eine signifikante Größenreduktion und für 10 Fallstudien erreichen wir sogar die minimale Entscheidungsbaumgröße.     «

Für sicherheitsrelevante Anm Sicherheitspezifikationen zu verifizieren und beweisbar korrekte Controller zu synthetisieren. Anstatt diese Controller mit riesigen Lookup-Tabellen oder schwer verständlichen binären Entscheidungsdiagrammen darzustellen, wurden in jüngsten Forschungsarbeiten Entscheidungsbäumen benutzt, um prägnante und erklärbare Darstellungen zu finden. Um komplexe Systeme mit kleinen Bäumen zu beschreiben, werden in neueren Arbeiten aussagekräftigere algebraische Prädikate in den...     »