Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization

We present the second generation of the tool Seminator that transforms transition-based generalized Büchi automata (TGBAs) into equivalent semi-deterministic automata. The tool has been extended with numerous optimizations and produces considerably smaller automata than its first version. In connect...

Descripción completa

Detalles Bibliográficos
Autores principales: Blahoudek, František, Duret-Lutz, Alexandre, Strejček, Jan
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363224/
http://dx.doi.org/10.1007/978-3-030-53291-8_2
_version_ 1783559626787127296
author Blahoudek, František
Duret-Lutz, Alexandre
Strejček, Jan
author_facet Blahoudek, František
Duret-Lutz, Alexandre
Strejček, Jan
author_sort Blahoudek, František
collection PubMed
description We present the second generation of the tool Seminator that transforms transition-based generalized Büchi automata (TGBAs) into equivalent semi-deterministic automata. The tool has been extended with numerous optimizations and produces considerably smaller automata than its first version. In connection with the state-of-the-art LTL to TGBAs translator Spot, Seminator  2 produces smaller (on average) semi-deterministic automata than the direct LTL to semi-deterministic automata translator ltl2ldgba of the Owl library. Further, Seminator  2 has been extended with an improved NCSB complementation procedure for semi-deterministic automata, providing a new way to complement automata that is competitive with state-of-the-art complementation tools.
format Online
Article
Text
id pubmed-7363224
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73632242020-07-16 Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization Blahoudek, František Duret-Lutz, Alexandre Strejček, Jan Computer Aided Verification Article We present the second generation of the tool Seminator that transforms transition-based generalized Büchi automata (TGBAs) into equivalent semi-deterministic automata. The tool has been extended with numerous optimizations and produces considerably smaller automata than its first version. In connection with the state-of-the-art LTL to TGBAs translator Spot, Seminator  2 produces smaller (on average) semi-deterministic automata than the direct LTL to semi-deterministic automata translator ltl2ldgba of the Owl library. Further, Seminator  2 has been extended with an improved NCSB complementation procedure for semi-deterministic automata, providing a new way to complement automata that is competitive with state-of-the-art complementation tools. 2020-06-16 /pmc/articles/PMC7363224/ http://dx.doi.org/10.1007/978-3-030-53291-8_2 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Blahoudek, František
Duret-Lutz, Alexandre
Strejček, Jan
Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization
title Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization
title_full Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization
title_fullStr Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization
title_full_unstemmed Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization
title_short Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization
title_sort seminator 2 can complement generalized büchi automata via improved semi-determinization
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363224/
http://dx.doi.org/10.1007/978-3-030-53291-8_2
work_keys_str_mv AT blahoudekfrantisek seminator2cancomplementgeneralizedbuchiautomataviaimprovedsemideterminization
AT duretlutzalexandre seminator2cancomplementgeneralizedbuchiautomataviaimprovedsemideterminization
AT strejcekjan seminator2cancomplementgeneralizedbuchiautomataviaimprovedsemideterminization

Ejemplares similares