## 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.

### Additional Services

Author: Andreas Morgenstern urn:nbn:de:hbz:386-kluedo-25721 Klaus Schneider Doctoral Thesis German 2010 2010 Technische Universität Kaiserslautern Technische Universität Kaiserslautern 2010/02/12 2011/01/03 Controller Synthesis; Symbolic Methods; Temporal Logic Fachbereich 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) 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581$