# SAT-based Minimization of Deterministic ω-Automata

### From LRDE

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

## Abstract

We describe a tool that inputs a deterministic $\displaystyle \omega$ -automaton with any acceptance condition, and synthesizes an equivalent $\displaystyle \omega$ -automaton with another arbitrary acceptance condition and a given number of states, if such an automaton exists. This tool, that relies on a SAT-based encoding of the problem, can be used to provide minimal $\displaystyle \omega$ -automata equivalent to given properties, for different acceptance conditions.

## Bibtex (lrde.bib)

@InProceedings{	  baarir.15.lpar,
author	= {Souheib Baarir and Alexandre Duret-Lutz},
booktitle	= {Proceedings of the 20th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning
(LPAR'15)},
title		= {{SAT}-based Minimization of Deterministic
$\omega$-Automata},
year		= {2015},
month		= nov,
pages		= {79--87},
publisher	= {Springer},
doi		= {10.1007/978-3-662-48899-7_6},
volume	= {9450},
series	= {Lecture Notes in Computer Science},
abstract	= {We describe a tool that inputs a deterministic
$\omega$-automaton with any acceptance condition, and
synthesizes an equivalent $\omega$-automaton with another
arbitrary acceptance condition and a given number of
states, if such an automaton exists. This tool, that relies
on a SAT-based encoding of the problem, can be used to
provide minimal $\omega$-automata equivalent to given
properties, for different acceptance conditions.}
}