From LRDE
< User:CdLine 18: | Line 18: | ||
}} |
}} |
||
+ | <!-- |
||
[[User:Cd]] |
[[User:Cd]] |
||
Line 37: | Line 38: | ||
<math>\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|+n)})</math> |
<math>\mathrm{O}(|S|\times 2^{\mathrm{O}(|\varphi|+n)})</math> |
||
+ | --> |
||
− | |||
<!-- |
<!-- |
||
{{#ask: [[Category:Publications]] [[Publication type::inproceedings]] [[Related project::Vaucanson]] OR [[Category:Publications]] [[Publication type::inproceedings]] [[Related project::Vcsn]] OR [[Category:Publications]] [[Publication type::inproceedings]] [[Related project::Spot]] |
{{#ask: [[Category:Publications]] [[Publication type::inproceedings]] [[Related project::Vaucanson]] OR [[Category:Publications]] [[Publication type::inproceedings]] [[Related project::Vcsn]] OR [[Category:Publications]] [[Publication type::inproceedings]] [[Related project::Spot]] |
Revision as of 16:55, 5 January 2018
- 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