Symbolic Controller Synthesis for LTL Specifications

  • 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.
  • Symbolische Überwachersynthese für LTL Spezifikationen

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Andreas Morgenstern
URN (permanent link):urn:nbn:de:hbz:386-kluedo-25721
Advisor:Klaus Schneider
Document Type:Doctoral Thesis
Language of publication:German
Year of Completion:2010
Year of Publication:2010
Publishing Institute:Technische Universität Kaiserslautern
Granting Institute:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2010/02/12
Tag:Controller Synthesis; Symbolic Methods; Temporal Logic
Faculties / Organisational entities:Fachbereich Informatik
CCS-Classification (computer science):F.3.1 Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
F.4.1 Mathematical Logic (F.1.1, I.2.2-4)
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $