User: Guest  Login
Original title:
Formalizing Symbolic Decision Procedures for Regular Languages 
Translated title:
Formalisierung Symbolischer Entscheidungsprozeduren für Reguläre Sprachen 
Year:
2015 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof., Ph.D.) 
Referee:
Nipkow, Tobias (Prof., Ph.D.); Silva, Alexandra (Prof. Dr.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Keywords:
decision procedure, regular language, Isabelle 
Translated keywords:
Entscheidungsprozedur, reguläre Sprache, Isabelle 
TUM classification:
DAT 706d; DAT 540d 
Abstract:
We study decision procedures for the equivalence of regular languages represented as regular expressions or logical formulas. Traditional algorithms in this context dispose of this symbolic representation by translating it into finite automata, which then are minimized and checked for structural equality. We develop concise algorithms that avoid this explicit translation by working with the symbolic structures directly. Our procedures are specified and proved correct in the proof assistant Isab...    »
 
Translated abstract:
Wir beschäftigen uns mit Entscheidungsprozeduren für die Äquivalenz regulärer Sprachen, die durch reguläre Ausdrücke oder logische Formeln dargestellt sind. Traditionelle Algorithmen hierfür entledigen sich dieser symbolischen Darstellung, indem sie sie in endliche Automaten übersetzen, welche anschließend minimiert und auf strukturelle Gleichheit überprüft werden. Wir entwickeln kompakte funktionale Algorithmen, die diese explizite Übersetzung vermeiden und stattdessen mit der symbolischen Dars...    »
 
Oral examination:
16.10.2015 
File size:
688689 bytes 
Pages:
132 
Last change:
20.11.2015