Difference between revisions of "Publications/blahoudek.17.lpar"
From LRDE
Line 19: | Line 19: | ||
@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>, |
Revision as of 23:01, 5 February 2018
- 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-21)
- 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-21)}, 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.} }