Difference between revisions of "Publications/blahoudek.17.lpar"
From LRDE
| (4 intermediate revisions by the same user not shown) | |||
| Line 4: | Line 4: | ||
| authors = František Blahoudek, Alexandre Duret-Lutz, Mikuláš Klokočka, Mojmír Křetínský, Jan Strejček |
| authors = František Blahoudek, Alexandre Duret-Lutz, Mikuláš Klokočka, Mojmír Křetínský, Jan Strejček |
||
| title = Seminator: A Tool for Semi-Determinization of Omega-Automata |
| title = Seminator: A Tool for Semi-Determinization of Omega-Automata |
||
| − | | booktitle = Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR |
+ | | booktitle = Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'17) |
| editors = Thomas Eiter, David Sands, Geoff Sutcliffe |
| editors = Thomas Eiter, David Sands, Geoff Sutcliffe |
||
| volume = 46 |
| volume = 46 |
||
| series = EPiC Series in Computing |
| series = EPiC Series in Computing |
||
| − | | pages = |
+ | | pages = 356 to 367 |
| publisher = EasyChair Publications |
| publisher = EasyChair Publications |
||
| lrdeprojects = Spot |
| lrdeprojects = Spot |
||
| lrdenewsdate = 2017-04-03 |
| lrdenewsdate = 2017-04-03 |
||
| lrdepaper = http://www.lrde.epita.fr/dload/papers/blahoudek.17.lpar.pdf |
| lrdepaper = http://www.lrde.epita.fr/dload/papers/blahoudek.17.lpar.pdf |
||
| − | | abstract = We present a tool that transforms nondeterministic |
+ | | abstract = We present a tool that transforms nondeterministic <math>\omega</math>-automata to semi-deterministic <math>\omega</math>-automata. The tool Seminator accepts transition-based generalized Büchi automata (TGBA) as an input and produces automata with two kinds of semi-determinism. The implemented procedure performs degeneralization and semi-determinization simultaneously and employs several other optimizations. We experimentally evaluate Seminator in the context of LTL to semi-deterministic automata translation. |
| type = inproceedings |
| type = inproceedings |
||
| id = blahoudek.17.lpar |
| id = blahoudek.17.lpar |
||
| + | | identifier = doi:10.29007/k5nl |
||
| bibtex = |
| bibtex = |
||
@InProceedings<nowiki>{</nowiki> blahoudek.17.lpar, |
@InProceedings<nowiki>{</nowiki> blahoudek.17.lpar, |
||
author = <nowiki>{</nowiki>Franti\v<nowiki>{</nowiki>s<nowiki>}</nowiki>ek Blahoudek and Alexandre Duret-Lutz and |
author = <nowiki>{</nowiki>Franti\v<nowiki>{</nowiki>s<nowiki>}</nowiki>ek Blahoudek and Alexandre Duret-Lutz and |
||
| − | Mikul\'<nowiki>{</nowiki>a<nowiki>}</nowiki>\v<nowiki>{</nowiki>s<nowiki>}</nowiki> Kloko\v<nowiki>{</nowiki>c<nowiki>}</nowiki>ka and Mojm |
+ | Mikul\'<nowiki>{</nowiki>a<nowiki>}</nowiki>\v<nowiki>{</nowiki>s<nowiki>}</nowiki> Kloko\v<nowiki>{</nowiki>c<nowiki>}</nowiki>ka and Mojm<nowiki>{</nowiki>\'i<nowiki>}</nowiki>r |
| − | K\v<nowiki>{</nowiki>r<nowiki>}</nowiki>et |
+ | K<nowiki>{</nowiki>\v<nowiki>{</nowiki>r<nowiki>}</nowiki><nowiki>}</nowiki>et<nowiki>{</nowiki>\'i<nowiki>}</nowiki>nsk<nowiki>{</nowiki>\'y<nowiki>}</nowiki> and Jan Strej<nowiki>{</nowiki>\v<nowiki>{</nowiki>c<nowiki>}</nowiki><nowiki>}</nowiki>ek<nowiki>}</nowiki>, |
title = <nowiki>{</nowiki>Seminator: A Tool for Semi-Determinization of |
title = <nowiki>{</nowiki>Seminator: A Tool for Semi-Determinization of |
||
Omega-Automata<nowiki>}</nowiki>, |
Omega-Automata<nowiki>}</nowiki>, |
||
booktitle = <nowiki>{</nowiki>Proceedings of the 21th International Conference on Logic |
booktitle = <nowiki>{</nowiki>Proceedings of the 21th International Conference on Logic |
||
for Programming, Artificial Intelligence, and Reasoning |
for Programming, Artificial Intelligence, and Reasoning |
||
| − | (LPAR |
+ | (LPAR'17)<nowiki>}</nowiki>, |
year = <nowiki>{</nowiki>2017<nowiki>}</nowiki>, |
year = <nowiki>{</nowiki>2017<nowiki>}</nowiki>, |
||
editor = <nowiki>{</nowiki>Thomas Eiter and David Sands and Geoff Sutcliffe<nowiki>}</nowiki>, |
editor = <nowiki>{</nowiki>Thomas Eiter and David Sands and Geoff Sutcliffe<nowiki>}</nowiki>, |
||
| Line 42: | Line 43: | ||
other optimizations. We experimentally evaluate Seminator |
other optimizations. We experimentally evaluate Seminator |
||
in the context of LTL to semi-deterministic automata |
in the context of LTL to semi-deterministic automata |
||
| − | translation.<nowiki>}</nowiki> |
+ | translation.<nowiki>}</nowiki>, |
| + | doi = <nowiki>{</nowiki>10.29007/k5nl<nowiki>}</nowiki> |
||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Latest revision as of 18:48, 10 March 2023
- Authors
- František Blahoudek, Alexandre Duret-Lutz, Mikuláš Klokočka, Mojmír Křetínský, Jan Strejček
- Where
- Proceedings of the 21th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'17)
- Type
- inproceedings
- Publisher
- EasyChair Publications
- Projects
- Spot
- Date
- 2017-04-03
Abstract
We present a tool that transforms nondeterministic -automata to semi-deterministic -automata. The tool Seminator accepts transition-based generalized Büchi automata (TGBA) as an input and produces automata with two kinds of semi-determinism. The implemented procedure performs degeneralization and semi-determinization simultaneously and employs several other optimizations. We experimentally evaluate Seminator in the context of LTL to semi-deterministic automata translation.
Documents
Bibtex (lrde.bib)
@InProceedings{ blahoudek.17.lpar,
author = {Franti\v{s}ek Blahoudek and Alexandre Duret-Lutz and
Mikul\'{a}\v{s} Kloko\v{c}ka and Mojm{\'i}r
K{\v{r}}et{\'i}nsk{\'y} and Jan Strej{\v{c}}ek},
title = {Seminator: A Tool for Semi-Determinization of
Omega-Automata},
booktitle = {Proceedings of the 21th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning
(LPAR'17)},
year = {2017},
editor = {Thomas Eiter and David Sands and Geoff Sutcliffe},
volume = {46},
series = {EPiC Series in Computing},
pages = {356--367},
month = may,
publisher = {EasyChair Publications},
abstract = {We present a tool that transforms nondeterministic
$\omega$-automata to semi-deterministic $\omega$-automata.
The tool Seminator accepts transition-based generalized
B\"uchi automata (TGBA) as an input and produces automata
with two kinds of semi-determinism. The implemented
procedure performs degeneralization and
semi-determinization simultaneously and employs several
other optimizations. We experimentally evaluate Seminator
in the context of LTL to semi-deterministic automata
translation.},
doi = {10.29007/k5nl}
}