Please use this identifier to cite or link to this item: doi:10.22028/D291-26532
Title: A uniform approach to the complexity and analysis of succinct systems
Author(s): Peter, Hans-Jörg
Language: English
Year of Publication: 2012
SWD key words: Beschreibungskomplexität
Komplexitätstheorie
Strukturkomplexität
Verifikation
Model Checking
Formale Methode
Spieltheorie
Logik
Free key words: Kompaktheit
gezeitete Automaten
Steuerungssynthese
unvollständige Information
beschränkte Synthese
succinctness
timed automata
bounded synthesis
imperfect information
small witness problem
DDC notations: 004 Computer science, internet
Publikation type: Doctoral Thesis
Abstract: “ This thesis provides a unifying view on the succinctness of systems: the capability of a modeling formalism to describe the behavior of a system of exponential size using a polynomial syntax. The key theoretical contribution is the introduction of sequential circuit machines as a new universal computation model that focuses on succinctness as the central aspect. The thesis demonstrates that many well-known modeling formalisms such as communicating state machines, linear-time temporal logic, or timed automata exhibit an immediate connection to this machine model. Once a (syntactic) connection is established, many complexity bounds for structurally restricted sequential circuit machines can be transferred to a certain formalism in a uniform manner. As a consequence, besides a far-reaching unification of independent lines of research, we are also able to provide matching complexity bounds for various analysis problems, whose complexities were not known so far. For example, we establish matching lower and upper bounds of the small witness problem and several variants of the bounded synthesis problem for timed automata, a particularly important succinct modeling formalism. Also for timed automata, our complexity-theoretic analysis leads to the identification of tractable fragments of the timed synthesis problem under partial observability. Specifically, we identify timed controller synthesis based on discrete or template-based controllers to be equivalent to model checking. Based on this discovery, we develop a new model checking-based algorithm to efficiently find feasible template instantiations. From a more practical perspective, this thesis also studies the preservation of succinctness in analysis algorithms using symbolic data structures. While efficient techniques exist for specific forms of succinctness considered in isolation, we present a general approach based on abstraction refinement to combine off-the-shelf symbolic data structures. In particular, for handling the combination of concurrency and quantitative timing behavior in networks of timed automata, we report on the tool Synthia which combines binary decision diagrams with difference bound matrices. In a comparison with the timed model checker Uppaal and the timed game solver Tiga running on standard benchmarks from the timed model checking and synthesis domain, respectively, the experimental results clearly demonstrate the effectiveness of our new approach.
Diese Dissertation liefert eine vereinheitlichende Sicht auf die Kompaktheit von Systemen: die Fähigkeit eines Modellierungsformalismus, das Verhalten eines Systems exponentieller Größe mit polynomieller Syntax zu beschreiben. Der wesentliche theoretische Beitrag ist die Einführung von sequenziellen Schaltkreis-Maschinen als neues universelles Berechnungsmodell, das sich auf den zentralen Aspekt der Kompaktheit konzentriert. Die Dissertation demonstriert, dass viele bekannte Modellierungsformalismen, wie z.B. kommunizierende Zustandsmaschinen, linear-Zeit temporale Logik (LTL) oder gezeitete Automaten eine direkte Verbindung zu diesem Maschinenmodell aufzeigen. Sobald eine (syntaktische) Verbindung hergestellt ist, können viele Komplexitätsschranken für strukturell beschränkte sequenzielle Schaltkreis-Maschinen für einen bestimmten Formalismus einheitlich übernommen werden. Neben einer weitreichenden Vereinheitlichung unabhängiger Forschungsrichtungen können auch zahlreiche Komplexitätsschranken für Analyse-Probleme etabliert werden, deren genaue Komplexität bisher noch nicht bekannt war. Zum Beispiel werden passende untere und obere Schranken des small witness Problems und mehrere Varianten des Synthese-Problems von Controllern mit beschränkter Größe für gezeitete Automaten bewiesen. Die theoretische Analyse deckt Fragmente geringerer Komplexität des partiell informierten Syntheseproblems für gezeitete Automaten auf. Es wird im Besonderen gezeigt, dass das gezeitete Syntheseproblem für diskrete oder Vorlagen-basierte Controller äquivalent zum Model Checking-Problem ist. Basierend auf dieser Einsicht wird ein neuartiger Model Checking-basierter Algorithmus zur effizienten Synthese von gültigen Instantiierungen von Vorlagen entwickelt. Der praktische Beitrag der Dissertation untersucht die Erhaltung von Kompaktheit in Analyse-Algorithmen durch die Benutzung symbolischer Datenstrukturen. Es wird ein allgemeiner Ansatz zur Kombination von Standard-Datenstrukturen vorgestellt, die jeweils bisher nur in Isolation verwendet werden konnten. Insbesondere wird für die Analyse von Netzwerken von gezeiteten Automaten das Tool Synthia vorgestellt, welches binäre Entscheidungs-Diagramme mit Differenzen-Matrizen verbindet. In einem experimentellen Vergleich mit den Tools Uppaal und Tiga wird klar die Effektivität des neuen Ansatzes belegt.
Link to this record: urn:nbn:de:bsz:291-scidok-54825
hdl:20.500.11880/26588
http://dx.doi.org/10.22028/D291-26532
Advisor: Finkbeiner, Bernd
Date of oral examination: 2-Nov-2012
Date of registration: 28-Aug-2013
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
thesis.pdf1,27 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.