A Unified Translation of Linear Temporal Logic to ω-Automata

Sickert, Salomon

Salomon Sickert

If you experience problems opening the document, please try this link.

Original title:: A Unified Translation of Linear Temporal Logic to ω-Automata
Translated title:: Eine uniforme Übersetzung von Linearer Temporaler Logik zu ω-Automaten
Author:: Sickert, Salomon
Year:: 2019
Document type:: Dissertation
Faculty/School:: 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 Büchi automata, limit-deterministic Bü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 into ω-automata by elementary means. All three translations are direct and no intermediate constructions are used. «
We present a unified translation of LTL formulas into nondeterministic Büchi automata, limit-deterministic Bü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 präsentieren eine uniforme Übersetzung von LTL Formeln zu nichtdeterministischen Büchi-Automaten (NBA), limit-deterministischen Büchi-Automaten (LDBA) und deterministischen Rabin-Automaten (DRA). Die Übersetzungen erzeugen Automaten von asymptotisch optimaler Größe (doppelt bzw. einfach exponentiell). Alle drei Übersetzungen werden aus einem einzigen Master Theorem abgeleitet. Das Master Theorem zerlegt die Sprache einer Formel in eine Boolesche Kombination von Sprachen, die mit elementaren Techniken zu ω-Automaten übersetzt werden können. Alle drei Übersetzungen sind direkt und benötigen keine Zwischenkonstruktionen. «
Wir präsentieren eine uniforme Übersetzung von LTL Formeln zu nichtdeterministischen Büchi-Automaten (NBA), limit-deterministischen Büchi-Automaten (LDBA) und deterministischen Rabin-Automaten (DRA). Die Übersetzungen erzeugen Automaten von asymptotisch optimaler Größe (doppelt bzw. einfach exponentiell). Alle drei Ü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... »
WWW:: https://mediatum.ub.tum.de/?id=1484932
Date of submission:: 30.04.2019
Oral examination:: 01.08.2019
File size:: 1338538 bytes
Pages:: 130
Urn (citeable URL):: https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20190801-1484932-1-4
Last change:: 04.09.2019
BibTeX