# From LTL and Limit-Deterministic B\"uchi Automata to Deterministic Parity Automata

## TL;DR

This paper presents a more efficient, single exponential method for translating limit-deterministic B"uchi automata to deterministic parity automata, improving the process of controller synthesis from LTL specifications.

## Contribution

It introduces a novel single exponential translation from LDBA to DPA and combines it with existing LTL-to-LDBA translation for a double exponential, Safraless LTL-to-DPA method.

## Key findings

- The new translation is more efficient than previous methods.
- Implementation shows competitive performance against existing tools.
- Applicable to complex LTL formulas, including benchmark instances.

## Abstract

Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper we describe a single exponential translation from limit-deterministic B\"uchi automata (LDBA) to DPA, and show that it can be concatenated with a recent efficient translation from LTL to LDBA to yield a double exponential, \enquote{Safraless} LTL-to-DPA construction. We also report on an implementation, a comparison with the SPOT library, and performance on several sets of formulas, including instances from the 2016 SyntComp competition.