Applications of automata learning in verification and synthesis

Neider, Daniel; Thomas, Wolfgang; Löding, Christof; Leucker, Martin

doi:999910363695

Applications of automata learning in verification and synthesis = Anwendungen von Verfahren zum Lernen endlicher Automaten in Verifikation und Synthese

Neider, Daniel (Author)

2014

Verantwortlichkeitsangabevorgelegt von Hermann Daniel Neider

ImpressumAachen : Publikationsserver der RWTH Aachen University 2014

UmfangXV, 267 S. : graph. Darst.

Aachen, Techn. Hochsch., Diss., 2014

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Thomas, Wolfgang (Thesis advisor) ; Löding, Christof (Thesis advisor)^RWTH* ; Leucker, Martin (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2014-04-25

Online
URN: urn:nbn:de:hbz:82-opus-51699
URL: https://publications.rwth-aachen.de/record/444982/files/5169.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Theoretische Informatik (Genormte SW) ; Synthese (Genormte SW) ; Verifikation (Genormte SW) ; Maschinelles Lernen (Genormte SW) ; Automatentheorie (Genormte SW) ; Invariante (Genormte SW) ; Informatik (frei) ; Lernen endlicher Autmaten (frei) ; Regular Model Checking (frei) ; Invarianten (frei) ; Erreichbarkeitsspiele (frei) ; Sicherheitsspiele (frei) ; automata learning (frei) ; invariants (frei) ; reachability games (frei) ; safety games (frei)

Thematische Einordnung (Klassifikation)
DDC: 004
msc: 68Q45 * 68Q32 * 05C57 * 68Q60

Kurzfassung
Das Ziel dieser Dissertation ist es, das Lernen endlicher Automaten in vier ausgesuchten Szenarien anzuwenden: Regular Model Checking, quantifizierte Invarianten linearer Datenstrukturen, automatische Erreichbarkeitsspiele sowie beschriftete Sicherheitsspiele. Regular Model Checking ist eine spezielle Art des Model Checkings, in der das zu verifizierende Programm in Form von endlichen Automaten gegeben ist. Wir entwickeln verschiedene (Semi-)Algorithmen für Regular Model Checking: einen white-box Algorithmus, der das gesamte Programm als Eingabe benötigt; semi-black-box Algorithmen, die Teile des Programms als Eingabe benötigen und fehlende Informationen von einem Lehrer lernen; schließlich black-box Algorithmen, die alle Informationen von einem Lehrer erhalten. Im Falle der black-box Algorithmen nutzen wir ein neues Konzept, genannt ICE-learning, welches ein generischer Ansatz zum Lernen von Invarianten ist. Quantifizierte Invarianten linearer Datenstrukturen treten in der Floyd-Hoare-Verifikation von Programmen auf, die beispielsweise Arrays und Listen verwalten. Um solche Invarianten zu lernen, führen wir das Konzept von quantified data automata ein und entwickeln ein aktives Lernverfahren für solche Automaten. Basierend auf einer endlichen Stichprobe von Programmkonfigurationen, die bei der Ausführung des zu prüfenden Programms auftreten, lernen wir einen quantified data automaton und übersetzen diesen in eine Logikformel. Eine solche Übersetzung benötigt möglicherweise einen zusätzlichen Abstraktionsschritt, der sicherstellt, dass die resultierende Formel zu einer entscheidbaren Logik gehört. Automatische Erreichbarkeitsspiele sind klassische Erreichbarkeitsspiele, die über automatischen Spielgraphen gespielt werden; solche Graphen werden durch asynchrone Transducer definiert und umfassen alle endlichen Graphen, Pushdown-Graphen sowie Konfigurationsgraphen von Turingmaschinen. Wir betrachten zunächst automatische Erreichbarkeitsspiele über endlichen Spielgraphen und beschreiben einen symbolischen Fixpunkt-Algorithmus zum Lernen von Attraktoren, der Mengen von Knoten des zugrundeliegenden Graphen durch endliche Automaten repräsentiert. Da ein solcher Fixpunkt-Algorithmus für Spiele über unendlichen Spielgraphen im Allgemeinen nicht terminiert, entwickeln wir einen lernbasierten (Semi-)Algorithmus, der den Attraktor nicht iterativ berechnet, sondern diesen von einem Lehrer lernt (sofern die Problemstellung dies erlaubt). Zuletzt betrachten wir beschriftete Sicherheitsspiele, die über endlichen, deterministisch kantenbeschrifteten Spielgraphen gespielt werden. In diesem Zusammenhang betrachten wir das Problem, Gewinnstrategien zu synthetisieren, die, wenn sie als Software oder Controller implementiert werden, in einer „kleinen“ Implementierung resultieren. Dazu modellieren wir Strategien als Strategieautomaten und nutzen eine Eigenschaft aktiver Lernalgorithmen aus: Typischerweise erzeugen solche Algorithmen Hypothesen mit wachsender Zustandszahl. Die zugrundeliegende Idee ist es, gewinnende Partien zu lernen und das Lernen zu stoppen, sobald der Lerner einen Strategieautomaten produziert, der eine Gewinnstrategie repräsentiert. Dieser Ansatz garantiert, dass der resultierende Strategieautomat höchstens so groß wie der zugrundeliegende Spielgraph ist. Um diesen Ansatz weiter zu verbessern, entwickeln wir domänenspizifische Optimierungen von Angluins sowie Kearns und Vaziranis Lernalgorithmen.

The objective of this thesis is to explore automata learning, which is an umbrella term for techniques that derive finite automata from external information sources, in the areas of verification and synthesis. We consider four application scenarios that turn out to be particularly well-suited: Regular Model Checking, quantified invariants of linear data structures, automatic reachability games, and labeled safety games. The former two scenarios stem from the area of verification whereas the latter two stem from the area of synthesis (more precisely, from the area of infinite-duration two-player games over graphs, as popularized by McNaughton). Regular Model Checking is a special kind of Model Checking in which the program to verify is modeled in terms of finite automata. We develop various (semi-)algorithms for computing invariants in Regular Model Checking: a white-box algorithm, which takes the whole program as input; two semi-black-box algorithms, which have access to a part of the program and learn missing information from a teacher; finally, two black-box algorithms, which obtain all information about the program from a teacher. For the black-box algorithms, we employ a novel paradigm, called ICE-learning, which is a generic learning setting for learning invariants. Quantified invariants of linear data structures occur in Floyd-Hoare-style verification of programs manipulating arrays and lists. To learn such invariants, we introduce the notion of quantified data automata and develop an active learning algorithm for these automata. Based on a finite sample of configurations that manifest on executions of the program in question, we learn a quantified data automaton and translate it into a logic formula expressing the invariant. The latter potentially requires an additional abstraction step to ensure that the resulting formula falls into a decidable logic. Automatic reachability games are classical reachability games played over automatic graphs; automatic graphs are defined by means of asynchronous transducers and subsume various types of graphs, such as finite graphs, pushdown graphs, and configuration graphs of Turing machines. We first consider automatic reachability games over finite graphs and present a symbolic fixed-point algorithm for computing attractors that uses deterministic finite automata to represent sets of vertices. Since such a fixed-point algorithm is not guaranteed to terminate on games over infinite graphs, we subsequently develop a learning-based (semi-)algorithm that learns the attractor (if possible) from a teacher rather than computing it iteratively. Finally, we consider labeled safety games, which are safety games played over finite graphs whose edges are deterministically labeled with actions. The problem we are interested in is to compute a winning strategy that, when implemented as as a circuit or a piece of code, results in a small implementation. To this end, we model strategies as so-called strategy automata and exploit a common property of active learning algorithms, namely that such algorithms produce conjectures of increasing size. The idea is to start learning the set of all winning plays and stop the learning prematurely as soon as the learner conjectures a winning strategy automaton. This procedure guarantees that the resulting strategy automaton is at most as large as the underlying game graph. To improve the performance of our algorithm further, we develop domain-specific optimizations of Angluin's as well as Kearns and Vazirani's active learning algorithms.

Fulltext:
PDF