2026-08-26T02:35:03Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27346 2026-08-24T14:08:30Z ddc:004 open_access

Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata Baier, Christel Klüppelholz, Sascha Spork, Timm Families of Finite Automata FDFA Unambiguous Automata Discrete-time Markov Chains Probabilistic Model Checking Verification 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christel Baier and Sascha Klüppelholz and Timm Spork 2026 Is Part Of LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2026.15 urn:nbn:de:0030-drops-273461 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.15 eng https://creativecommons.org/licenses/by/4.0/legalcode