Not logged in.

Quick Search - Contribution

Contribution Details

Type Master's Thesis
Scope Discipline-based scholarship
Title Widening for Automata
Organization Unit
Authors
  • Vijay Victor D'Silva
Supervisors
  • Abraham Bernstein
Institution University of Zurich
Faculty Faculty of Economics, Business Administration and Information Technology
Date 2006
Abstract Text Computing fixpoints of increasing sequences of sets is an important problem in many areas of computer science including algorithmic verification, program analysis, inductive inference and systems biology. For most problems, the fixpoint computation does not terminate, so an approximate solution has to be found. Widening is a technique to compute an over-approximation of an infinite, increasing sequence of sets. In this thesis, we present a framework for constructing widening operators for fixpoint computations over sets represented as automata. Many widening operators for automata that appear in the literature are instances of our framework. Moreover, two inductive inference algorithms in the literature naturally fall out as instances of this framework. We identify general criteria that characterise the effect of widening and use these criteria to study various properties of widening operators. We also provide several new results and generalise existing results about widening operators and inductive inference algorithms. Finally, we show how a widening operator defined in our framework can be combined with algorithms for automated verification of infinite state systems and provide a heuristic for generating counterexamples if verification fails.
Zusammenfassung Die Bestimmng des kleinsten Fixpunktes einer aufsteigender Folge von Mengen ist ein zentrales Problem in vielen Teilgebieten der Informatik, wie zum Beispiel in der algorithmischen Verifikation, der Programm-Analyse, induktiver Inferenz und der Bioinformatik. Oft ist eine genaue Bestimmung des Fixpunkts nicht möglich; eine Überapproximation ist jedoch meist ausreichend. Widening ist eine Methode die zur Berechnung solcher Überapproximationen eingesetzt wird. Diese Arbeit präsentiert einen Framework zur Konstruktion von Widening Operatoren zur Berechnung solcher Überapproximationen, die als Automaten dargestellt werden können. Unser Framework stellt eine Verallgemeinerung vieler in der einschlägigen Literatur verwendeten Widening-Operatoren dar. Insbesondere deckt unsere Kategorisierung auch zwei auf induktiver Inferenz basierende Algorithmen ab. Wir definieren allgemeine Kriterien die den Effekt von Widening erfassen und wenden diese auf Widening Operatoren an. Wir präsentieren sowohl neue als auch Generalisierungen bereits vorhanderer Ergebnisse für Widening Operatoren und Algorithmen basierend auf induktiver Inferenz. Wir zeigen wie mit Hilfe unseres Frameworks erstellte Operatoren mit Algorithmen zur automatischen Verifikation von Systemen mit unendlichen Zustandsräumen kombiniert werden können und präsentieren Heuristiken zur Berechnung von Gegenbeispielen f ür den Fall dass die Verifikation fehlschlägt.
PDF File Download
Export BibTeX