# From LTL to Unambiguous B\"uchi Automata via Disambiguation of Alternating Automata

## TL;DR

This paper introduces a novel algorithm for converting LTL formulas into unambiguous B"uchi automata using a new disambiguation approach for very weak alternating automata, resulting in smaller automata and improved efficiency.

## Contribution

It presents a new disambiguation method for VWAA, optimizations for automata size reduction, and an implementation that outperforms existing tableau-based methods.

## Key findings

- Automata sizes are smaller with the new method.
- The approach reduces computation times compared to tableau-based translation.
- Effective analysis of Markov chains under LTL using UBA.

## Abstract

This paper proposes a new algorithm for the generation of unambiguous B\"uchi automata (UBA) from LTL formulas. Unlike existing tableau-based LTL-to-UBA translations, our algorithm deals with very weak alternating automata (VWAA) as an intermediate representation. It relies on a new notion of unambiguity for VWAA and a disambiguation procedure for VWAA. We introduce optimizations on the VWAA level and new LTL simplifications targeted at generating small UBA. We report on an implementation of the construction in our tool duggi and discuss experimental results that compare the automata sizes and computation times of duggi with the tableau-based LTL-to-UBA translation of the SPOT tool set. Our experiments also cover the analysis of Markov chains under LTL specifications, which is an important application of UBA.