Symbolic Controller Synthesis for LTL Specifications

  • Symbolische Überwachersynthese für LTL Spezifikationen
  • It is an old dream in computer science to automatically generate a system from a formal specification or at least to automatically check whether a system is guaranteed to satisfy a specification. The second problem is known as the verification problem and powerful tools exist that automatically check the correctness of a system with respect to a given declarative specification. In this thesis we consider the first problem with respect to a given declarative specification in linear temporal logic LTL. We refer to this problem as the controller synthesis problem. The controller synthesis problem is to check whether an (incomplete) implementation of a system can be refined by a controller such that a given property holds, and if so, to automatically construct this controller. Although the idea to automatically synthesize an implementation from a formal declaration is nearly 50 years old, it has not yet made its way to practice. A major breakthrough in verification has been achieved by considering symbolic representations of states and transitions by propositional formulas which lead to the invention of symbolic model checking. With the advent of succinct data structures and efficient decision procedures for propositional formulas, which are the heart of almost all approaches to hardware verification, it has become possible to verify complex systems. This thesis considers the Controller Synthesis Problem for full LTL and concentrates on decision procedures that are amenable to a symbolic implementation so that the available decision procedures like BDDs or SAT solvers can be employed.

Volltext Dateien herunterladen

Metadaten exportieren

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Verfasserangaben:Andreas Morgenstern
URN (Permalink):urn:nbn:de:hbz:386-kluedo-25721
Betreuer:Klaus Schneider
Sprache der Veröffentlichung:Deutsch
Jahr der Fertigstellung:2010
Jahr der Veröffentlichung:2010
Veröffentlichende Institution:Technische Universität Kaiserslautern
Titel verleihende Institution:Technische Universität Kaiserslautern
Datum der Annahme der Abschlussarbeit:12.02.2010
Datum der Publikation (Server):03.01.2011
Freies Schlagwort / Tag:Controller Synthesis; Symbolic Methods; Temporal Logic
Fachbereiche / Organisatorische Einheiten:Fachbereich Informatik
CCS-Klassifikation (Informatik):F. Theory of Computation / F.3 LOGICS AND MEANINGS OF PROGRAMS / F.3.1 Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
F. Theory of Computation / F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES / F.4.1 Mathematical Logic (F.1.1, I.2.2-4)
DDC-Sachgruppen:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011