Difference between revisions of "Publications/baarir.15.lpar"
From LRDE
m |
|||
Line 8: | Line 8: | ||
| publisher = Springer |
| publisher = Springer |
||
| volume = ??? |
| volume = ??? |
||
− | | 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 |
+ | | 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. |
| note = To appear. |
| note = To appear. |
||
| urllrde = 201511-LPAR |
| urllrde = 201511-LPAR |
||
Line 32: | Line 32: | ||
synthesizes an equivalent $\omega$-automaton with another |
synthesizes an equivalent $\omega$-automaton with another |
||
arbitrary acceptance condition and a given number of |
arbitrary acceptance condition and a given number of |
||
− | states, if such an automaton |
+ | states, if such an automaton exists. This tool, that relies |
on a SAT-based encoding of the problem, can be used to |
on a SAT-based encoding of the problem, can be used to |
||
provide minimal $\omega$-automata equivalent to given |
provide minimal $\omega$-automata equivalent to given |
Revision as of 16:31, 3 September 2015
- Authors
- Souheib Baarir, Alexandre Duret-Lutz
- Where
- Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'15)
- Type
- inproceedings
- Publisher
- Springer
- Projects
- Spot
- 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.
Bibtex (lrde.bib)
@InProceedings{ baarir.15.lpar, author = {Souheib Baarir and Alexandre Duret-Lutz}, booktitle = {Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'15)}, title = {{SAT}-based Minimization of Deterministic $\omega$-Automata}, year = {2015}, month = nov, pages = {???--???}, publisher = {Springer}, volume = {???}, abstract = {We describe a tool that inputs a deterministic $\omega$-automaton with any acceptance condition, and synthesizes an equivalent $\omega$-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 $\omega$-automata equivalent to given properties, for different acceptance conditions.}, note = {To appear.} }