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 exists. 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.
CITATION STYLE
Baarir, S., & Duret-Lutz, A. (2015). SAT-based minimization of deterministic ω-Automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9450, pp. 79–87). Springer Verlag. https://doi.org/10.1007/978-3-662-48899-7_6
Mendeley helps you to discover research relevant for your work.