Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques

Stefan Kiefer, Cas Widdershoven

TL;DR

A novel technique to analyse unambiguous Buchi automata quantitatively is introduced, based on linear-algebra arguments that originate from the analysis of matrix semigroups with constant spectral radius that can replace a combinatorial procedure that dominates the computational complexity of the existing procedure.

Abstract

We introduce a novel technique to analyse unambiguous Büchi 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|$.

Efficient Analysis of Unambiguous Automata Using Matrix Semigroup Techniques

TL;DR

A novel technique to analyse unambiguous Buchi automata quantitatively is introduced, based on linear-algebra arguments that originate from the analysis of matrix semigroups with constant spectral radius that can replace a combinatorial procedure that dominates the computational complexity of the existing procedure.

Abstract

We introduce a novel technique to analyse unambiguous Büchi 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 of states of the automaton, the new algorithm runs in time , improving on an efficient implementation of the combinatorial algorithm by a factor of .

Paper Structure

This paper contains 12 sections, 23 theorems, 6 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Algorithms
  4. The Basic Linear System
  5. Calculating D-Normalisers Using Cuts
  6. Calculating D-Normalisers Using Linear Algebra
  7. Discussion
  8. The Number of Transitions Can Be Quadratic.
  9. Missing Proofs
  10. Proof From Section \ref{['sec:prelim']}
  11. Proofs From Section \ref{['sub:cuts']}
  12. Proofs From Section \ref{['sub:pseudo-cuts']}

Key Result

Lemma 5

Given a UBA, one can compute in time $O(|\delta|^2|\Sigma|)$ a UBA of at most the same size, with the same language and without diamonds.

Figures (3)

  • Figure 1: Left: unambiguous automaton $\mathcal{A}$. Right: visualisation of the affine space $\mathcal{F}$ (blue) and the vector space spanned by (pseudo-)cuts (red); these spaces are orthogonal.
  • Figure 2: The UBA from Figure \ref{['fig:automaton']} and the Markov chain $\mathcal{M}$ on the left, and their product, $B$, on the right. The (single) accepting recurrent SCC is shaded green, and the two other SCCs are shaded red.
  • Figure 3: An unambiguous automaton with a single recurrent strongly connected SCC and a quadratic number of edges.

Theorems & Definitions (35)

  • Example 1
  • Example 2
  • Example 3
  • Example 4
  • Example 5
  • Lemma 5
  • Theorem 6
  • Example 7
  • Example 8
  • Lemma 9: Lemma 12 in baieunp1
  • ...and 25 more