Gast ::
000444982 001__ 444982 000444982 005__ 20231024090509.0 000444982 0247_ $$2URN$$aurn:nbn:de:hbz:82-opus-51699 000444982 0247_ $$2HSB$$a999910363695 000444982 0247_ $$2OPUS$$a5169 000444982 0247_ $$2Laufende Nummer$$a33588 000444982 037__ $$aRWTH-CONV-145293 000444982 041__ $$aEnglish 000444982 082__ $$a004 000444982 0847_ $$2msc$$a68Q45 * 68Q32 * 05C57 * 68Q60 000444982 1001_ $$0P:(DE-82)023531$$aNeider, Daniel$$b0$$eAuthor 000444982 245__ $$aApplications of automata learning in verification and synthesis$$cvorgelegt von Hermann Daniel Neider$$honline, print 000444982 246_3 $$aAnwendungen von Verfahren zum Lernen endlicher Automaten in Verifikation und Synthese$$yGerman 000444982 260__ $$aAachen$$bPublikationsserver der RWTH Aachen University$$c2014 000444982 300__ $$aXV, 267 S. : graph. Darst. 000444982 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd 000444982 3367_ $$02$$2EndNote$$aThesis 000444982 3367_ $$2DRIVER$$adoctoralThesis 000444982 3367_ $$2BibTeX$$aPHDTHESIS 000444982 3367_ $$2DataCite$$aOutput Types/Dissertation 000444982 3367_ $$2ORCID$$aDISSERTATION 000444982 502__ $$aAachen, Techn. Hochsch., Diss., 2014$$gFak01$$o2014-04-25 000444982 520__ $$aThe 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.$$leng 000444982 5203_ $$aDas 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.$$lger 000444982 591__ $$aGermany 000444982 653_7 $$aInformatik 000444982 653_7 $$2ger$$aLernen endlicher Autmaten 000444982 653_7 $$2ger$$aRegular Model Checking 000444982 653_7 $$2ger$$aInvarianten 000444982 653_7 $$2ger$$aErreichbarkeitsspiele 000444982 653_7 $$2ger$$aSicherheitsspiele 000444982 653_7 $$2eng$$aautomata learning 000444982 653_7 $$2eng$$ainvariants 000444982 653_7 $$2eng$$areachability games 000444982 653_7 $$2eng$$asafety games 000444982 650_7 $$2SWD$$aTheoretische Informatik 000444982 650_7 $$2SWD$$aSynthese 000444982 650_7 $$2SWD$$aVerifikation 000444982 650_7 $$2SWD$$aMaschinelles Lernen 000444982 650_7 $$2SWD$$aAutomatentheorie 000444982 650_7 $$2SWD$$aInvariante 000444982 7001_ $$0P:(DE-82)IDM01355$$aLöding, Christof$$b2$$eThesis advisor$$urwth 000444982 7001_ $$0P:(DE-82)IDM06019$$aThomas, Wolfgang$$b1$$eThesis advisor 000444982 7001_ $$0P:(DE-82)023349$$aLeucker, Martin$$b3$$eThesis advisor 000444982 8564_ $$uhttps://publications.rwth-aachen.de/record/444982/files/5169.pdf 000444982 909CO $$ooai:publications.rwth-aachen.de:444982$$pdnbdelivery$$pVDB$$pdriver$$purn$$popen_access$$popenaire 000444982 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess 000444982 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x0 000444982 9201_ $$0I:(DE-82)122110_20140620$$k122110$$lLehrstuhl für Informatik 7 (Logik und Theorie diskreter Systeme)$$x1 000444982 961__ $$c2014-12-04$$x2014-10-13$$z2012-02-20 000444982 970__ $$aHT018386878 000444982 980__ $$aphd 000444982 980__ $$aI:(DE-82)120000_20140620 000444982 980__ $$aI:(DE-82)122110_20140620 000444982 980__ $$aVDB 000444982 980__ $$aUNRESTRICTED 000444982 980__ $$aConvertedRecord 000444982 9801_ $$aFullTexts