# Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques

## TL;DR

This paper presents a new linear-algebra-based technique for analyzing unambiguous automata, significantly improving the efficiency of model checking by reducing computational complexity from combinatorial methods.

## Contribution

It introduces a novel matrix semigroup approach to analyze unambiguous automata, replacing a complex combinatorial procedure with a more efficient linear-algebraic method.

## Key findings

- New algorithm runs in O(|Q|^4) time
- Improves efficiency over existing combinatorial methods by a factor of |Q|
- Applicable to quantitative analysis of unambiguous Büchi automata

## Abstract

We introduce a novel technique to analyse unambiguous B\"uchi automata quantitatively, and apply this to the model checking problem. It is based on linear-algebra arguments that originate from the analysis of matrix semigroups with constant spectral radius. This method can replace a combinatorial procedure that dominates the computational complexity of the existing procedure by Baier et al. We analyse the complexity in detail, showing that, in terms of the set $Q$ of states of the automaton, the new algorithm runs in time $O(|Q|^4)$, improving on an efficient implementation of the combinatorial algorithm by a factor of $|Q|$.