User

From LRDE

< User:Cd
Line 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

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