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

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 elementaren Techniken zu ω-Automaten übersetzt werden können. Alle drei Übersetzungen sind direkt und benötigen keine Zwischenkonstruktionen.     «

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