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.

Download full text files

Export metadata

Additional Services

Search Google Scholar
Metadaten
Author:Andreas Morgenstern
URN:urn:nbn:de:hbz:386-kluedo-25721
Advisor:Klaus Schneider
Document Type:Doctoral Thesis
Language of publication:German
Year of Completion:2010
Year of first Publication:2010
Publishing Institution:Technische Universität Kaiserslautern
Granting Institution:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2010/02/12
Date of the Publication (Server):2011/01/03
Tag:Controller Synthesis; Symbolic Methods; Temporal Logic
Faculties / Organisational entities:Kaiserslautern - Fachbereich Informatik
CCS-Classification (computer science):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-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011