Controllers are central objects in many model checking and synthesis processes. They can not only be used for implementation, but also have the potential to reveal insights about the system and validate the correctness of or highlight errors in the underlying model. To leverage this potential, succinct and easily explainable data structures for controller representation are required. Recent work has shown that decision trees are particularly well-suited to this task, providing much more concise and understandable representations than lookup tables or binary decision diagrams. This thesis presents an overview of decision tree learning for controller representation and proposes a variety of algorithmic improvements that make the resulting trees more efficient and explainable. These techniques have been implemented in the latest version of the tool dtControl, which enables the easy conversion of controllers from many verification tools to decision trees. We furthermore introduce a thoroughly redesigned software architecture for dtControl, allowing for much more flexibility and extensibility. We demonstrate the effectiveness of our methods on a variety of case studies, where we can in almost all cases reduce controller sizes by at least 96% compared to a lookup table representation.     «

Controllers are central objects in many model checking and synthesis processes. They can not only be used for implementation, but also have the potential to reveal insights about the system and validate the correctness of or highlight errors in the underlying model. To leverage this potential, succinct and easily explainable data structures for controller representation are required. Recent work has shown that decision trees are particularly well-suited to this task, providing much more concise...     »

Controller sind wesentliche Bestandteile vieler Modellprüfungs- und Syntheseverfahren. Sie werden einerseits zur Implementierung verwendet und erlauben andererseits Einblicke in das System zu gewinnen, sowie die Korrektheit beziehungsweise potenzielle Fehler des zugrundeliegenden Modells aufzuzeigen. Um dieses Potenzial nutzen zu können, werden kompakte und leicht verständliche Datenstrukturen für die Repräsentation von Controllern benötigt. Jüngste Forschungsergebnisse haben gezeigt, dass Entscheidungsbäume besonders gut für diese Aufgabe geeignet sind und sehr viel kleinere und eklärbarere Repräsentationen ergeben als Lookup-Tabellen oder binäre Entscheidungsdiagramme. Diese Bachelorarbeit gibt einen Überblick über Entscheidungsbaum-Lernen zur Repräsentation von Controllern und präsentiert verschiedene algorithmische Verbesserungen, die zu effizienteren und verständlicheren Bäumen führen. Diese Verfahren wurden in der neuesten Version des Programms dtControl implementiert, welches es ermöglicht, Controller von vielen Verifikationstools in Entscheidungsbäume umzuwandeln. Darüber hinaus wurde die Softwarearchitektur des Programms von Grund auf neu konzipiert, um mehr Flexibilität und Erweiterbarkeit zu ermöglichen. Die Effektivität unserer Methoden wird anhand einer Vielzahl von Fallstudien nachgewiesen, in denen unsere Algorithmen fast immer eine Größenreduktion von mindestens 96% gegenüber Lookup-Tabellen erreichen.     «

Controller sind wesentliche Bestandteile vieler Modellprüfungs- und Syntheseverfahren. Sie werden einerseits zur Implementierung verwendet und erlauben andererseits Einblicke in das System zu gewinnen, sowie die Korrektheit beziehungsweise potenzielle Fehler des zugrundeliegenden Modells aufzuzeigen. Um dieses Potenzial nutzen zu können, werden kompakte und leicht verständliche Datenstrukturen für die Repräsentation von Controllern benötigt. Jüngste Forschungsergebnisse haben gezeigt, dass Entsc...     »