Difference between revisions of "Publications/baarir.15.lpar"
From LRDE
| Line 5: | Line 5: | ||
| booktitle = Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'15) |
| booktitle = Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'15) |
||
| title = SAT-based Minimization of Deterministic ω-Automata |
| title = SAT-based Minimization of Deterministic ω-Automata |
||
| − | | pages = |
+ | | pages = 79 to 87 |
| publisher = Springer |
| publisher = Springer |
||
| − | | volume = |
+ | | volume = 9450 |
| + | | series = Lecture Notes in Computer Science |
||
| 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. |
| 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 |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| lrdenewsdate = 2015-09-01 |
| lrdenewsdate = 2015-09-01 |
||
| Line 24: | Line 24: | ||
year = <nowiki>{</nowiki>2015<nowiki>}</nowiki>, |
year = <nowiki>{</nowiki>2015<nowiki>}</nowiki>, |
||
month = nov, |
month = nov, |
||
| − | pages = <nowiki>{</nowiki> |
+ | pages = <nowiki>{</nowiki>79--87<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
publisher = <nowiki>{</nowiki>Springer<nowiki>}</nowiki>, |
||
| − | volume = <nowiki>{</nowiki> |
+ | volume = <nowiki>{</nowiki>9450<nowiki>}</nowiki>, |
| ⚫ | |||
abstract = <nowiki>{</nowiki>We describe a tool that inputs a deterministic |
abstract = <nowiki>{</nowiki>We describe a tool that inputs a deterministic |
||
$\omega$-automaton with any acceptance condition, and |
$\omega$-automaton with any acceptance condition, and |
||
| Line 34: | Line 35: | ||
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 |
||
| − | properties, for different acceptance conditions.<nowiki>}</nowiki> |
+ | properties, for different acceptance conditions.<nowiki>}</nowiki> |
| ⚫ | |||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Revision as of 14:16, 13 May 2016
- 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 = {79--87},
publisher = {Springer},
volume = {9450},
series = {Lecture Notes in Computer Science},
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.}
}