Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen › Begutachtung
Abstract
Families of deterministic finite automata (FDFA) have been introduced as a concise automaton model that characterizes ω-regular languages by processing their ultimately periodic words. FDFA are known to enjoy many good properties and can be exponentially more succinct than deterministic ω-automata with Rabin, Streett or parity acceptance. This paper addresses two main questions: (1) Are FDFA suitable for probabilistic model checking purposes? and (2) Is it possible to obtain an even more compact representation of ω-regular languages by allowing the components of an FDFA to be unambiguous instead of deterministic? Question (1) is answered in the affirmative by presenting the first polynomial-time algorithm for computing the probability that a discrete-time Markov chain satisfies an ω-regular property represented as an FDFA. Question (2) is motivated by the fact that unambiguous finite automata may require exponentially fewer states than deterministic ones. This paper introduces a model of families of unambiguous finite automata (FUFA) that captures the class of ω-regular languages. FUFA can be exponentially more succinct than both FDFA and unambiguous Büchi automata, and there is a single-exponential translation from linear temporal logic (LTL) to FUFA. This stands in contrast to a double-exponential lower bound for the translation from LTL to FDFA. Moreover, the polynomial-time probabilistic model checking algorithm for discrete-time Markov chains against FDFA-specifications is extended to the case where the property is represented by an FUFA with a deterministic leading automaton.
Details
| Originalsprache | Englisch |
|---|---|
| Titel | 37th International Conference on Concurrency Theory, CONCUR 2026 |
| Redakteure/-innen | Ana Sokolova, Patrick Totzke |
| Herausgeber (Verlag) | Schloss Dagstuhl- Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing |
| ISBN (elektronisch) | 978-3-95977-447-5 |
| Publikationsstatus | Veröffentlicht - 24 Aug. 2026 |
| Peer-Review-Status | Ja |
Publikationsreihe
| Reihe | Leibniz International Proceedings in Informatics, LIPIcs |
|---|---|
| Band | 391 |
| ISSN | 1868-8969 |
Konferenz
| Titel | 37th International Conference on Concurrency Theory |
|---|---|
| Kurztitel | CONCUR 2026 |
| Veranstaltungsnummer | 37 |
| Beschreibung | co-located with QEST+FORMATS, FMICS and a number of workshops under the joint name CONFEST 2026 |
| Dauer | 1 - 4 September 2026 |
| Webseite | |
| Ort | University of Liverpool |
| Stadt | Liverpool |
| Land | Großbritannien/Vereinigtes Königreich |
Externe IDs
| ORCID | /0000-0002-5321-9343/work/227511171 |
|---|---|
| ORCID | /0000-0003-1724-2586/work/227513428 |
| ORCID | /0009-0008-4461-0667/work/227514233 |
Schlagworte
ASJC Scopus Sachgebiete
- Software - Discrete-time Markov Chains, Families of Finite Automata, FDFA, Probabilistic Model Checking, Unambiguous Automata, Verification
Schlagwörter
- Discrete-time Markov Chains, Families of Finite Automata, FDFA, Probabilistic Model Checking, Unambiguous Automata, Verification