I am happy to announce that the following papers has been accepted at
the 20th International Conferences on Logic for Programming,
Artificial Intelligence and Reasoning (LPAR) to be held at the
University of the South Pacific (Suva, Fiji) on 24–28 November 2015.
SAT-based Minimization of Deterministic ω-Automata
Souheib Baarir¹, Alexandre Duret-Lutz¹
¹LRDE, EPITA, Le Kremlin-Bicêtre, France
https://www.lrde.epita.fr/wiki/Publications/baarir.15.lpar
Abstract:
We describe a tool that inputs a deterministic ω-automaton with any
acceptance condition, and synthesizes an equivalent ω-automaton with
another arbitrary acceptance condition and a given number of states,
if such an automaton exist. This tool, that relies on a SAT-based
encoding of the problem, can be used to provide minimal ω-automata
equivalent to given properties, for different acceptance conditions.
--
Alexandre Duret-Lutz