Search

Model checkers like SPIN provide a way to gain certainty about the behavior of programs and protocols. To guarantee that the model checker itself is correct, the CAVA project developed a verified and executable LTL model checker using Isabelle/HOL. This thesis reports on various building blocks of CAVA by presenting the first formalized and executable Promela semantics, a framework for verifying depth-first search based algorithms, and an automata library. As a part thereof, this thesis will detail the development rationale and history of those building blocks., Modelchecker, wie z.B. SPIN, sind eine Möglichkeit, Gewissheit über das Verhalten von Programmen und Protokollen zu erlangen. Um nun sicherzustellen, dass der Modelchecker selber korrekt ist, wurde im Projekt CAVA ein verifizierter und ausführbarer Modelchecker mit Hilfe von Isabelle/HOL entwickelt. In dieser Dissertation stellen wir verschiedene Bausteine von CAVA vor: Die erste formalisierte und ausführbare Semantik von Promela, ein Framework um auf Tiefensuche basierende Algorithmen zu verifizieren, sowie eine Automatenbibliothek. Ein Augenmerk liegt dabei auf der Geschichte und den Hintergründen der jeweiligen Implementierung.

Algebraic systems of fixpoint equations $X = F(X)$ arise in various areas of computer science. In this thesis we study algorithms for solving algebraic systems based on Newton's method as proposed by (Esparza, Kiefer, Luttenberger, 2010). We first investigate the theoretical properties and algorithmics of Newton's method on semirings. Then we present FPsolve, an efficient and generic implementation of various methods for solving algebraic systems over semirings. Finally, we explore applications in database theory, formal languages, and natural language processing., Algebraische Systeme von Fixpunktgleichungen finden Anwendung in verschiedenen Bereichen der Informatik. In dieser Arbeit beschäftigen wir uns mit Algorithmen zur Lösung von algebraischen Systemen, welche auf dem Newtonverfahren basieren (nach Espraza/Kiefer/Luttenberger, 2010). Wir untersuchen die theoretischen und algorithmischen Eigenschaften des Newtonverfahrens auf Semiringen. Anschließend stellen wir FPsolve vor, eine effiziente und generische Implementierung verschiedener Methoden zur Lösung algebraischer Systeme. Abschließend erkunden wir diverse Anwendungen.

This thesis deals with verification of probabilistic systems both in the setting of discrete time as well as continuous time. Firstly, we design a novel method to translate formulae of linear temporal logic to automata and show how this speeds up verification of Markov decision processes. Secondly, we provide the first compositional verification method in the continuous-time setting. We design a specification formalism and assume-guarantee algorithms to approximate probabilities to reach a given state of an interactive Markov chain within a given time bound., Diese Arbeit beschäftigt sich mit Verifikation von probabilistischen Systemen sowohl in diskreter Zeit als auch in kontinuierlicher Zeit. Wir entwerfen eine neuartige Methode, um Formeln der linearen zeitlichen Logik in Automaten übersetzen, und zeigen, wie diese die Verifikation von Markov Entscheidungsprozessen beschleunigt. Wir entwerfen auch das erste kompositorische Verifikationsverfahren für kontinuierliche Zeit, namentlich ein assume-guarantee Algorithmus das die Wahrscheinlichkeiten, dass ein gegebene Zustand innerhalb gegebener Zeit erreicht ist annähert.

In this thesis we make two contributions to the general problem of automatically diagnosing and correcting bugs in software systems. In the first contribution, we use a catalogue of error prone program code together with search techniques to fix faulty Java Code. In the second contribution, we consider model based approaches for partially observable, distributed systems with alarms. For the alarm explanation, we present new approaches based on Petri net unfoldings., Diese Arbeit stellt zwei Beiträge für die automatische Diagnose und Korrektur von Softwaresystemen vor. Im ersten Beitrag nutzen wir einen Katalog von fehleranfälligen Quellcode zusammen mit Suchmethoden um Programmfehler in Java Code automatisch zu korrigieren. Im zweiten Beitrag präsentieren wir modellbasierte Ansätze für die Diagnose von partiell beobachtbaren, verteilten Systemen mit Alarmen. Für die Alarmerklärung stellen wir Verfahren vor, die auf Petrinetz-Entfaltungen basieren.

This thesis deals with reachability problems of probabilistic systems with large state spaces. To compute reachability probabilities of probabilistic programs we extend abstraction approaches such that they can use arbitrary abstract domains. We present a method for proving termination with probability one of probabilistic programs which uses termination provers for non-probabilistic programs. We also develop methods for the analysis of branching processes., Diese Arbeit beschäftigt sich mit Erreichbarkeitsproblemen für probabilistische Systeme mit großen Zustandsräumen. Um Erreichbarkeitswahrscheinlichkeiten von probabilistischen Programmen zu bestimmen, erweitern wir Abstraktionsansätze, so dass beliebige abstrakte Domänen benutzt werden können. Wir präsentieren eine Methode, um Terminierung von probabilistischen Programmen mit Wahrscheinlichkeit 1 zu beweisen, die Terminierungsbeweiser für nichtprobabilistische Programme nutzt. Außerdem entwickeln wir Verfahren für die Analyse von Verzweigungsprozessen.

We develop a framework, based on canonical permutations and firing sequences, for approaching classical computational problems (like reachability) for classes of Petri nets with arbitrary edge multiplicities. We apply this framework to conservative Petri nets, generalized communication-free Petri nets, and their inverse nets to obtain complexity results for these problems. Furthermore, we investigate generalized conflict-free, communication-free, and rings of Petri nets, as well as related grammars., Wir entwickeln ein auf kanonischen Permutationen und Schaltungsfolgen basierendes Rahmenkonzept für klassische Probleme (wie Erreichbarkeit) für Klassen von Petrinetzen mit allgemeinen Kantengewichten. Dieses wenden wir auf erhaltende Petrinetze, generalisierte kommunikationsfreie Petrinetze, sowie deren inverse Petrinetze an, um Komplexitätsschranken zu erhalten. Zudem untersuchen wir generalisierte konfliktfreie, kommunikationsfreie, und ringförmige Petrinetze, sowie mit diesen Klassen verwandte Grammatiken.

For many computational tasks, the performance bottleneck is caused by memory accesses instead of CPU time. To tackle this problem in a theoretical way, the I/O-model and the Parallel External Memory (PEM) model were introduced. The PEM model describes several parallel processors, each assigned to a private internal memory (cache) of limited capacity. Communication and the storage of input, output, and intermediate results is realised by a shared external memory (disk) which is organised in blocks. This thesis considers the parallel I/O complexity of several tasks that are based on sparse matrix computations over a semiring. We present upper and lower bounds for the multiplication of a sparse matrix with (i) several vectors, including bilinear forms, (ii) a dense matrix, (iii) another sparse matrix. The work is complemented by a consideration of the MapReduce framework in the PEM model., Bei viele Berechnungsaufgaben wird die Berechnungsdauer maßgeblich durch Speicherzugriffe bestimmt. Um diese theoretisch zu erfassen wurden das I/O-Model und das Parallel External Memory Model (PEM) erdacht. Im PEM Model werden mehrere parallel Prozessoren modelliert, welche je an einen privaten Cache (Internspeicher) mit limitierter Kapazität angebunden sind. Zusätzlich steht ein Shared-Memory-Speicher (Externspeicher) für Eingabe, Ausgabe und Kommunikation zur Verfügung. In dieser Dissertation werden mehrere Aufgaben untersucht, die auf dünnbesetzten Matrizen in einem Semiring basieren. Es werden obere und untere Schranken für die I/O Komplexität der Multiplikation einer dünnbesetzten Matrix mit (i) mehreren Vektoren, (ii) einer dichten Matrix und (iii) einer weiteren dünnbesetzten Matrix gezeigt. Zusätzlich wird die Arbeit mit einer Untersuchung des MapReduce frameworks komplementiert.

For many computational tasks, the performance bottleneck is caused by memory accesses instead of CPU time. To tackle this problem in a theoretical way, the I/O-model and the Parallel External Memory (PEM) model were introduced. The PEM model describes several parallel processors, each assigned to a private internal memory (cache) of limited capacity. Communication and the storage of input, output, and intermediate results is realised by a shared external memory (disk) which is organised in blocks. This thesis considers the parallel I/O complexity of several tasks that are based on sparse matrix computations over a semiring. We present upper and lower bounds for the multiplication of a sparse matrix with (i) several vectors, including bilinear forms, (ii) a dense matrix, (iii) another sparse matrix. The work is complemented by a consideration of the MapReduce framework in the PEM model., Bei viele Berechnungsaufgaben wird die Berechnungsdauer maßgeblich durch Speicherzugriffe bestimmt. Um diese theoretisch zu erfassen wurden das I/O-Model und das Parallel External Memory Model (PEM) erdacht. Im PEM Model werden mehrere parallel Prozessoren modelliert, welche je an einen privaten Cache (Internspeicher) mit limitierter Kapazität angebunden sind. Zusätzlich steht ein Shared-Memory-Speicher (Externspeicher) für Eingabe, Ausgabe und Kommunikation zur Verfügung. In dieser Dissertation werden mehrere Aufgaben untersucht, die auf dünnbesetzten Matrizen in einem Semiring basieren. Es werden obere und untere Schranken für die I/O Komplexität der Multiplikation einer dünnbesetzten Matrix mit (i) mehreren Vektoren, (ii) einer dichten Matrix und (iii) einer weiteren dünnbesetzten Matrix gezeigt. Zusätzlich wird die Arbeit mit einer Untersuchung des MapReduce frameworks komplementiert.

We show how side-effecting constraint systems provide a unified framework for realizing efficient interprocedural analyses of programs, where the amount of context-sensitivity can be adjusted and where the context-sensitive analyses of local properties can be combined with flow-insensitive analyses of global properties. To use the widening and narrowing approach on (side-effecting) constraint systems, we present a novel operator together with adapted versions of solving algorithms. Finally, we report on the various implementation challenges that arose in the Goblint tool., Wir zeigen, dass Ungleichungssysteme mit Seiteneffekten einen einheitlichen Rahmen für die Realisierung von effizienten interprozeduralen Analysen von Programmen bieten, speziell wenn der Umfang der Kontextsensitivität einzugestellt ist und lokale, kontextsensitive Analysen mit globalen, kontextinsensitiven Analysen zu kombinieren ist. Um widening und narrowing auf diese Ungleichungssysteme anzuwenden, stellen wir einen neuen Lösungsalgorithmen vor. Weiterhin diskutieren wir Herausforderungen die bei der Implementierung im Goblint Werkzeugs gelöst wurden.

We prove the class H1 of Horn clauses decidable when extended with disequality tests of arbitrary (sub)terms. Decidability even is preserved if the terms are transformed by a given tree homomorphism prior to the test for disequality. Furthermore, a novel class of tree automata with equality and disequality tests is introduced, for which we prove Boolean closure and decidability., Wir zeigen, dass die Klasse H1 von Hornklauseln entscheidbar bleibt, wenn sie mit Ungleichheitstests zwischen beliebigen (Sub-)Termen erweitert wird. Die Entscheidbarkeit bleibt auch erhalten, wenn die Terme vor dem Test auf Ungleichheit durch einen Baumhomomorphismus transformiert werden. Des Weiteren wird eine neue Klasse von Baumautomaten mit Gleichheits- und Ungleichheitsbedingungen eingeführt, für die wir Booleschen Abschluss und Entscheidbarkeit beweisen.

We show how side-effecting constraint systems provide a unified framework for realizing efficient interprocedural analyses of programs, where the amount of context-sensitivity can be adjusted and where the context-sensitive analyses of local properties can be combined with flow-insensitive analyses of global properties. To use the widening and narrowing approach on (side-effecting) constraint systems, we present a novel operator together with adapted versions of solving algorithms. Finally, we report on the various implementation challenges that arose in the Goblint tool., Wir zeigen, dass Ungleichungssysteme mit Seiteneffekten einen einheitlichen Rahmen für die Realisierung von effizienten interprozeduralen Analysen von Programmen bieten, speziell wenn der Umfang der Kontextsensitivität einzugestellt ist und lokale, kontextsensitive Analysen mit globalen, kontextinsensitiven Analysen zu kombinieren ist. Um widening und narrowing auf diese Ungleichungssysteme anzuwenden, stellen wir einen neuen Lösungsalgorithmen vor. Weiterhin diskutieren wir Herausforderungen die bei der Implementierung im Goblint Werkzeugs gelöst wurden.

We prove the class H1 of Horn clauses decidable when extended with disequality tests of arbitrary (sub)terms. Decidability even is preserved if the terms are transformed by a given tree homomorphism prior to the test for disequality. Furthermore, a novel class of tree automata with equality and disequality tests is introduced, for which we prove Boolean closure and decidability., Wir zeigen, dass die Klasse H1 von Hornklauseln entscheidbar bleibt, wenn sie mit Ungleichheitstests zwischen beliebigen (Sub-)Termen erweitert wird. Die Entscheidbarkeit bleibt auch erhalten, wenn die Terme vor dem Test auf Ungleichheit durch einen Baumhomomorphismus transformiert werden. Des Weiteren wird eine neue Klasse von Baumautomaten mit Gleichheits- und Ungleichheitsbedingungen eingeführt, für die wir Booleschen Abschluss und Entscheidbarkeit beweisen.

The goal of this work is the verification of probabilistic systems in the interactive theorem prover Isabelle/HOL. This requires the formalization of probability theory. We construct probability spaces with infinitely many independent random variables and the stochastic process of a Markov chain. We use these probability spaces to verify the correctness of probabilistic model checking and to verify properties of the ZeroConf protocol and the Crowds protocol., Ziel dieser Arbeit ist die Verifikation probabilistischer Systeme in dem interaktiven Theorembeweiser Isabelle/HOL. Dies setzt die Formalisierung von Wahrscheinlichkeitstheorie voraus. Wir konstruieren W-Räume mit unendlich vielen, unabhängigen Zufallsvariablen und den zu einer Markov-Kette gehörenden stochastischen Prozess. Wir verwenden diese W-Räume um die Korrektheit von probabilistischem Model Checking und Eigenschaften des ZeroConf-Protokolls und des Crowds-Protokoll zu verifizieren.

This thesis deals with reachability problems of probabilistic systems with large state spaces. To compute reachability probabilities of probabilistic programs we extend abstraction approaches such that they can use arbitrary abstract domains. We present a method for proving termination with probability one of probabilistic programs which uses termination provers for non-probabilistic programs. We also develop methods for the analysis of branching processes., Diese Arbeit beschäftigt sich mit Erreichbarkeitsproblemen für probabilistische Systeme mit großen Zustandsräumen. Um Erreichbarkeitswahrscheinlichkeiten von probabilistischen Programmen zu bestimmen, erweitern wir Abstraktionsansätze, so dass beliebige abstrakte Domänen benutzt werden können. Wir präsentieren eine Methode, um Terminierung von probabilistischen Programmen mit Wahrscheinlichkeit 1 zu beweisen, die Terminierungsbeweiser für nichtprobabilistische Programme nutzt. Außerdem entwickeln wir Verfahren für die Analyse von Verzweigungsprozessen.

In this thesis we investigate inference of probabilistic subsequential transducers in an active learning environment. First, we propose a novel inference algorithm where the learner interacts with an oracle by asking probabilistic queries on the observed data. Second, we propose another learning algorithm where the oracle can be replaced by statistical tests over observed data. We also provide experimental evidence to show the correctness of the proposed algorithms., In der vorliegenden Arbeit untersuchen wir probabilistische subsequentielle Transducer in einer aktiven Lernumgebung. Zunächst stellen wir einen neuen Lernalgorithmus vor, der probabilistische Anfragen über beobachtete Daten an ein Orakel stellt. Danach stellen wir einen weiteren Lernalgorithmus vor, bei dem das Orakel durch statistische Tests über beobachteten Daten ersetzt wird. Um die Korrektheit nachzuweisen liefern wir darüber hinaus experimentelle Belege.

Autonomous technical systems, such as intelligent production facilities and household robots, have to plan sequences of actions in advance. This doesn't allow to exploit current observations and, in particular, to completely account for system faults. Therefore, the aim of this work is to obtain most probable faults during execution of a plan and to monitor the success probabilities of individual plan goals during runtime. For this computational problem of plan assessment we develop two approaches that translate probabilistic, hierarchical automata models of a system to constraint nets or Bayes nets, in order to then apply generic algorithms from model-based diagnosis or probabilistic reasoning. Theoretical and empirical results show that both approaches are equally well suited for plan assessment and that the method can be a building block for more robust autonomous systems., Autonome technische Systeme, wie beispielsweise intelligente Produktionsanlagen oder Haushaltsroboter, müssen Aktionssequenzen im Voraus planen; dabei können jedoch aktuelle Beobachtungen und insbesondere Fehler des Systems nicht vollständig berücksichtigt werden. Das Ziel dieser Arbeit ist deshalb, während der Ausführung eines Plans wahrscheinlichste Fehler zu ermitteln und die Erfolgswahrscheinlichkeit einzelner Planziele zur Laufzeit zu überwachen. Für dieses Berechnungsproblem des "Plan Assessment" entwickeln wir zwei Ansätze, die probabilistische, hierarchische Automatenmodelle eines Systems in Constraint- oder Bayes-Netze übersetzen, um dann generische Algorithmen der modellbasierten Diagnose oder des probabilistischen Schließens anzuwenden. Theoretische und experimentelle Ergebnisse zeigen, dass beide Ansätze zur Planbewertung gleichermaßen geeignet sind und das Verfahren einen Baustein für robustere autonome Systeme bilden kann.

The goal of this work is the verification of probabilistic systems in the interactive theorem prover Isabelle/HOL. This requires the formalization of probability theory. We construct probability spaces with infinitely many independent random variables and the stochastic process of a Markov chain. We use these probability spaces to verify the correctness of probabilistic model checking and to verify properties of the ZeroConf protocol and the Crowds protocol., Ziel dieser Arbeit ist die Verifikation probabilistischer Systeme in dem interaktiven Theorembeweiser Isabelle/HOL. Dies setzt die Formalisierung von Wahrscheinlichkeitstheorie voraus. Wir konstruieren W-Räume mit unendlich vielen, unabhängigen Zufallsvariablen und den zu einer Markov-Kette gehörenden stochastischen Prozess. Wir verwenden diese W-Räume um die Korrektheit von probabilistischem Model Checking und Eigenschaften des ZeroConf-Protokolls und des Crowds-Protokoll zu verifizieren.

In this thesis we investigate inference of probabilistic subsequential transducers in an active learning environment. First, we propose a novel inference algorithm where the learner interacts with an oracle by asking probabilistic queries on the observed data. Second, we propose another learning algorithm where the oracle can be replaced by statistical tests over observed data. We also provide experimental evidence to show the correctness of the proposed algorithms., In der vorliegenden Arbeit untersuchen wir probabilistische subsequentielle Transducer in einer aktiven Lernumgebung. Zunächst stellen wir einen neuen Lernalgorithmus vor, der probabilistische Anfragen über beobachtete Daten an ein Orakel stellt. Danach stellen wir einen weiteren Lernalgorithmus vor, bei dem das Orakel durch statistische Tests über beobachteten Daten ersetzt wird. Um die Korrektheit nachzuweisen liefern wir darüber hinaus experimentelle Belege.

Autonomous technical systems, such as intelligent production facilities and household robots, have to plan sequences of actions in advance. This doesn't allow to exploit current observations and, in particular, to completely account for system faults. Therefore, the aim of this work is to obtain most probable faults during execution of a plan and to monitor the success probabilities of individual plan goals during runtime. For this computational problem of plan assessment we develop two approaches that translate probabilistic, hierarchical automata models of a system to constraint nets or Bayes nets, in order to then apply generic algorithms from model-based diagnosis or probabilistic reasoning. Theoretical and empirical results show that both approaches are equally well suited for plan assessment and that the method can be a building block for more robust autonomous systems., Autonome technische Systeme, wie beispielsweise intelligente Produktionsanlagen oder Haushaltsroboter, müssen Aktionssequenzen im Voraus planen; dabei können jedoch aktuelle Beobachtungen und insbesondere Fehler des Systems nicht vollständig berücksichtigt werden. Das Ziel dieser Arbeit ist deshalb, während der Ausführung eines Plans wahrscheinlichste Fehler zu ermitteln und die Erfolgswahrscheinlichkeit einzelner Planziele zur Laufzeit zu überwachen. Für dieses Berechnungsproblem des "Plan Assessment" entwickeln wir zwei Ansätze, die probabilistische, hierarchische Automatenmodelle eines Systems in Constraint- oder Bayes-Netze übersetzen, um dann generische Algorithmen der modellbasierten Diagnose oder des probabilistischen Schließens anzuwenden. Theoretische und experimentelle Ergebnisse zeigen, dass beide Ansätze zur Planbewertung gleichermaßen geeignet sind und das Verfahren einen Baustein für robustere autonome Systeme bilden kann.