User: Guest  Login
Original title:
A Unified Translation of Linear Temporal Logic to ω-Automata 
Translated title:
Eine uniforme Übersetzung von Linearer Temporaler Logik zu ω-Automaten 
Year:
2019 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Esparza Estaun, Francisco Javier (Prof. Dr.) 
Referee:
Esparza Estaun, Francisco Javier (Prof. Dr.); Kupferman, Orna (Prof., Ph.D.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Keywords:
Linear Temporal Logic, ω-automata, Büchi automata, Rabin automata 
TUM classification:
DAT 500d 
Abstract:
We present a unified translation of LTL formulas into nondeterministic Büchi automata, limit-deterministic Büchi automata (LDBA), and deterministic Rabin automata (DRA). The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive Boolean combination of languages that can be translated...    »
 
Translated abstract:
Wir präsentieren eine uniforme Übersetzung von LTL Formeln zu nichtdeterministischen Büchi-Automaten (NBA), limit-deterministischen Büchi-Automaten (LDBA) und deterministischen Rabin-Automaten (DRA). Die Übersetzungen erzeugen Automaten von asymptotisch optimaler Größe (doppelt bzw. einfach exponentiell). Alle drei Übersetzungen werden aus einem einzigen Master Theorem abgeleitet. Das Master Theorem zerlegt die Sprache einer Formel in eine Boolesche Kombination von Sprachen, die mit eleme...    »
 
Oral examination:
01.08.2019 
File size:
1338538 bytes 
Pages:
130 
Last change:
04.09.2019