Difference between revisions of "Publications/baarir.15.lpar"
From LRDE
| Line 4: | Line 4: | ||
| authors = Souheib Baarir, Alexandre Duret-Lutz |
| authors = Souheib Baarir, Alexandre Duret-Lutz |
||
| 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 <math>ω</math>-Automata |
| pages = ??? to ??? |
| pages = ??? to ??? |
||
| 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 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 <math>ω</math>-automaton with any acceptance condition, and synthesizes an equivalent <math>ω</math>-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 <math>ω</math>-automata equivalent to given properties, for different acceptance conditions. |
| − | | note = To appear |
+ | | note = To appear. |
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| lrdenewsdate = 2015-09-01 |
| lrdenewsdate = 2015-09-01 |
||
| Line 35: | Line 35: | ||
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>, |
||
| − | note = <nowiki>{</nowiki>To appear<nowiki>}</nowiki> |
+ | note = <nowiki>{</nowiki>To appear.<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Revision as of 16:51, 28 April 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 Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle ω} -automaton with any acceptance condition, and synthesizes an equivalent Failed to parse (syntax error): {\displaystyle ω} -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 Failed to parse (syntax error): {\displaystyle ω} -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.}
}