From LRDE
< User:CdRevision as of 17:55, 5 January 2018 by Clément Démoulins (talk | contribs)
- Authors
- AA
- Where
- AA
- Type
- inproceedings
- Date
- 2015-09-01
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 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.
Documents