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

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 |

Date of the Publication (Server): | 2011/01/03 |

Tag: | Controller Synthesis; Symbolic Methods; Temporal Logic |

Faculties / Organisational entities: | 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 |