Learning communicating and nondeterministic automata

Kern, Carsten; Katoen, Joost-Pieter

doi:29523

Learning communicating and nondeterministic automata = Lernen von kommunizierenden und nichtdeterministischen Automaten

Kern, Carsten (Author)

2009

Verantwortlichkeitsangabevorgelegt von Carsten Kern

ImpressumAachen : RWTH Aachen, Department of Computer Science 2009

Umfang230 S. : graph. Darst.

ReiheAachener Informatik-Berichte ; 2009,17

Zugl.: Aachen, Techn. Hochsch., Diss., 2009

Zsfassung in engl. und dt. Sprache

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2009-08-31

Online
URN: urn:nbn:de:hbz:82-opus-29439
URL: http://publications.rwth-aachen.de/record/51281/files/Kern_Carsten.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
CSP (Genormte SW) ; Maschinelles Lernen (Genormte SW) ; Inkrementelles Lernen (Genormte SW) ; Algorithmische Lerntheorie (Genormte SW) ; CASE <Informatik> (Genormte SW) ; Software Engineering (Genormte SW) ; Verteiltes System (Genormte SW) ; Informatik (frei) ; Verteilte Systeme (frei) ; Lernen verteilter Systeme (frei) ; Lernbibliothek (frei) ; Lernen von Halbordnungen (frei) ; distributed systems (frei) ; learning of distributed systems (frei) ; learning library (frei) ; partial order learning (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Die Ergebnisse dieser Arbeit sind zweigeteilt. Einerseits werden existierende induktive Lernverfahren grundlegend erweitert, und zwei neue Lernalgorithmen zur Inferenz nichtdeterministischer bzw. universeller Automaten vorgestellt. Andererseits werden bestimmte Lerntechniken eingesetzt und verbessert, um kommunizierende Automaten (in der Softwareentwicklung auch Designmodelle genannt) semi-automatisch zu inferieren. Es werden sowohl theoretische Resultate bezüglich der Durchführbarkeit der Ansätze als auch zwei Implementierungen vorgestellt, die jeweils unsere theoretische Arbeit untermaueren. Für das erste Ziel, nämlich einen sogenannten aktiven online Lernalgorithms für nichtdeterministische, endliche Automaten (NFA) zu entwerfen, wird in Analogie zu Angluins berühmtem Lernalgorithmus L* für determinisitische, endliche Automaten (DFA) eine Version eines Algorithmus entwickelt, der eine bestimmte Teilklasse nichtdeterministischer, endlicher Automaten inferieren kann. Die Automaten dieser Klasse werden residuelle, endliche Automaten (RFSA) genannt. Denis et al. haben gezeigt, dass es eine exponentielle Kluft zwischen der Größe minimaler DFA und äquivalenter kanonischer RFSA gibt. Auch in Fällen in denen der kanonische RFSA exponentiell größer ist als ein äquivalenter minimaler NFA, zeigen wir, dass unser neuer Lernalgorithmus NL* eine große Verbesserung im Vergleich zu dem schon existierenden Algorithmus L* darstellt, da der kanonische RFSA im schlimmsten Fall die gleiche Größe wie der äquivalente minimale DFA besitzt, im Regelfall jedoch wesentlich kleiner und leichter zu lernen ist. Im Gegensatz zu dem von Denis et al. vorgestellten Lernverfahren ist unser Algorithmus in der Lage kanonische RFSA zu lernen. Wie L* so wird auch unser Algorithmus NL* in vielen Bereichen Einsatz finden: z.B. in der Mustererkennung, in der maschinellen Linguistik und Biologie sowie in der Spracherkennung und formalen Verifikation. Unserer Meinung nach könnte NL* vor allem im Bereich der formalen Verifikation eine Hauptrolle spielen, in der die Größe der zu prüfenden Modelle von essentieller Bedeutung und Nichtdeterminismus nur von untergeordnetem Interesse ist. Das zweite Ziel dieser Arbeit lautet, einen Ansatz zur Inferenz verteilter Designmodelle (CFMs) basierend auf Anforderungen zu kreieren, die als Systemszenarios (Message Sequence Charts) spezifiziert sind. Die Hauptidee besteht darin, den Algorithmus von Angluin dahingehend zu erweitern, dass er mit gültigen und ungültigen Systemläufen umzugehen weiß und nach einigen Iterationen mit einem Zwischenmodell (einem DFA) aufwartet, das Eigenschaften aufweist, die es in über FIFO Kanäle kommunizierende Komponenten (oder Prozesse) verteilen lassen. Es werden theoretische Ergebnisse hergeleitet, die Aussagen darüber liefern, welche Klassen verteiler Automaten (CFMs) mit welchen Komplexitätsschranken lernbar sind. In diesem Zusammenhang wird außerdem eine Implementierung mit Namen Smyle vorgestellt, die die Durchführbarkeit des Lernens einiger in dieser Arbeit vorgestellter Klassen aufzeigt. Aufbauend auf diesem theoretischen Lernformalismus wird ein softwaretechnisches Lebenszyklusmodell, genannt der Smyle Modeling Approach, entwickelt, in das unsere Lernanwendung Smyle integriert wird. Zusätzlich wurde ein Projekt ins Leben gerufen, das aktuell die meisten der in dieser Arbeit vorgestellten Lernverfahren und deren Erweiterungen implementiert. Die entstandene Lernbibliothek trägt den Namen libalf. Wir hoffen, dass diese Bibliothek aufgrund ihres kontinuierlich ansteigenden Umfangs an Lernverfahren großen Anklang unter Wissenschaftlern finden wird, und dass sie der Startpunkt eines weitläufigen Projektes unterschiedlicher Universitäten wird, die diese Bibliothek nutzen und dazu beitragen, sie mit neuen Algorithmen an zu reichern.

The results of this dissertation are two-fold. On the one hand, inductive learning techniques are extended and two new inference algorithms for inferring nondeterministic, and universal, respectively, finite-state automata are presented. On the other hand, certain learning techniques are employed and enhanced to semi-automatically infer communicating automata (also called design models in the software development cycle). For both topics, theoretical results on the feasibility of the approaches, as well as an implementation are presented which, in both cases, support our theory. Concerning the first objective to derive a so-called active online learning algorithm for nondeterministic finite-state automata (NFA), we present, in analogy to Angluin's famous learning algorithm L* for deterministic finite-state automata (DFA), a version for inferring a certain subclass of NFA. The automata from this class are called residual finite-state automata (RFSA). It was shown by Denis et al. that there is an exponential gap between the size of minimal DFA and their corresponding minimal RFSA. Even if there are also cases where the canonical (i.e., minimal) RFSA is exponentially larger than a corresponding minimal NFA, we show that the new learning algorithm---called NL*---is a great improvement compared to L* as the inferred canonical RFSA has always at most the size of the corresponding minimal DFA but is usually even considerably smaller and more easy to learn. Unlike a learning procedure developed by Denis et al.---called DeLeTe2---our algorithm is capable of deriving canonical RFSA. Like L*, the new algorithm will be applicable in many fields including pattern recognition, computational linguistics and biology, speech recognition, and verification. From our point of view, NL* might especially play a mayor role in the area of formal verification where the size of the models that are processed is of enormous importance and nondeterminism not regarded an unpleasant property. The second objective of this thesis is to create a method for inferring distributed design models (CFMs) from a given set of requirements specified as scenarios (message sequence charts). The main idea is to extend the L* algorithm to cope with valid and invalid sets of system runs and, after some iterations, come up with an intermediate design model (a DFA) which exhibits features that make it distributable into communicating components (or processes) interacting via FIFO channels. Theoretical results on which classes of CFMs are learnable in which time-complexity bounds are presented. We also developed a tool implementation called Smyle, realizing important theoretical results evolving from this part of the thesis. Based on this learning formalism we also derive a software-engineering lifecycle model called the Smyle Modeling Approach in which we embedded our learning approach. Additionally, we launched a project for a new learning library called libalf which includes most of the learning algorithms (and their extensions) mentioned in this thesis. We hope that, due to its continuously increasing functionality, libalf will find broad acceptance among researchers, and that it will be the starting point for an extensive project of different research groups which will employ libalf, or augment the library with new algorithms.

Volltext:
PDF