From LTL to Unambiguous Büchi Automata via Disambiguation of Alternating Automata

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

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 languageEnglish
Title of host publicationFormal Methods – The Next 30 Years
EditorsMaurice H. ter Beek, Annabelle McIver, José N. Oliveira
PublisherSpringer, Berlin [u. a.]
Pages262-279
Number of pages18
ISBN (print)978-3-030-30941-1
Publication statusPublished - 2019
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science, Volume 11800
ISSN0302-9743

Conference

TitleInternational Symposium on Formal Methods 2019
Abbreviated titleFM 2019
Conference number
Duration7 - 11 October 2019
Website
Degree of recognitionInternational event
Location
CityPorto
CountryItaly

External IDs

ORCID /0000-0002-5321-9343/work/142236711
Scopus 85076082294

Keywords

Keywords

  • LTL, Unambiguous Büchi Automata, alternating automata, disambiguation

Library keywords