Determinization and Limit-Determinization of Emerson-Lei Automata

Research output: Contribution to book/conference proceedings/anthology/reportConference contributionContributedpeer-review

Contributors

Abstract

We study the problem of determinizing 𝜔-automata whose acceptance condition is defined on the transitions using Boolean formulas, also known as transition-based Emerson-Lei automata (TELA). The standard approach to determinize TELA first constructs an equivalent generalized Büchi automaton (GBA), which is later determinized. We introduce three new ways of translating TELA to GBA. Furthermore, we give a new determinization construction which determinizes several GBA separately and combines them using a product construction. An experimental evaluation shows that the product approach is competitive when compared with state-of-the-art determinization procedures. We also study limit-determinization of TELA and show that this can be done with a single-exponential blow-up, in contrast to the known double-exponential lower-bound for determinization. Finally, one version of the limit-determinization procedure yields good-for-MDP automata which can be used for quantitative probabilistic model checking.

Details

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis
EditorsZhe Hou, Vijay Ganesh
PublisherSpringer, Cham
Pages15–31
ISBN (Print)978-3-030-88884-8
Publication statusPublished - 12 Oct 2021
Peer-reviewedYes

Publication series

SeriesLecture Notes in Computer Science
Volume12971
ISSN0302-9743

Conference

TitleThe 19th International Symposium on Automated Technology for Verification and Analysis
Abbreviated titleATVA 2021
Conference number
Duration18 - 22 October 2021
Website
Degree of recognitionInternational event
Locationonline
CityGold Coast
CountryAustralia

Keywords

Research priority areas of TU Dresden

    DFG Classification of Subject Areas according to Review Boards

      Subject groups, research areas, subject areas according to Destatis