From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
Abstract
This paper proposes a new algorithm for the generation of unambiguous Büchi automata (UBA) from LTL formulas. Unlike existing tableau-based LTL-to-UBA translations, our algorithm deals with very weak alternating automata (VWAA) as an intermediate representation. It relies on a new notion of unambiguity for VWAA and a disambiguation procedure for VWAA. We introduce optimizations on the VWAA level and new LTL simplifications targeted at generating small UBA. We report on an implementation of the construction in our tool Duggi and discuss experimental results that compare the automata sizes and computation times of Duggi with the tableau-based LTL-to-UBA translation of the SPOT tool set. Our experiments also cover the analysis of Markov chains under LTL specifications, which is an important application of UBA.
Details
Original language | English |
---|---|
Title of host publication | Formal Methods – The Next 30 Years |
Editors | Maurice H. ter Beek, Annabelle McIver, José N. Oliveira |
Publisher | Springer, Berlin [u. a.] |
Pages | 262-279 |
Number of pages | 18 |
ISBN (print) | 978-3-030-30941-1 |
Publication status | Published - 2019 |
Peer-reviewed | Yes |
Publication series
Series | Lecture Notes in Computer Science, Volume 11800 |
---|---|
ISSN | 0302-9743 |
Conference
Title | International Symposium on Formal Methods 2019 |
---|---|
Abbreviated title | FM 2019 |
Conference number | |
Duration | 7 - 11 October 2019 |
Website | |
Degree of recognition | International event |
Location | |
City | Porto |
Country | Italy |
External IDs
ORCID | /0000-0002-5321-9343/work/142236711 |
---|---|
Scopus | 85076082294 |
Keywords
Keywords
- LTL, Unambiguous Büchi Automata, alternating automata, disambiguation