Determinization and Limit-Determinization of Emerson-Lei Automata

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

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

OriginalspracheEnglisch
TitelAutomated Technology for Verification and Analysis
Redakteure/-innenZhe Hou, Vijay Ganesh
Herausgeber (Verlag)Springer, Berlin [u. a.]
Seiten15–31
Seitenumfang17
ISBN (Print)978-3-030-88884-8
PublikationsstatusVeröffentlicht - 12 Okt. 2021
Peer-Review-StatusJa

Publikationsreihe

ReiheLecture Notes in Computer Science, Volume 12971
ISSN0302-9743

Konferenz

Titel19th International Symposium on Automated Technology for Verification and Analysis
KurztitelATVA 2021
Veranstaltungsnummer19
Dauer18 - 22 Oktober 2021
Webseite
BekanntheitsgradInternationale Veranstaltung
Ortonline
StadtGold Coast
LandAustralien

Externe IDs

ORCID /0000-0002-5321-9343/work/142236773
ORCID /0000-0003-1724-2586/work/165453612
Scopus 85118190202

Schlagworte

Bibliotheksschlagworte