Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata
For researchers in formal verification and automata theory, this work provides more efficient representations and algorithms for probabilistic model checking of ω-regular properties.
The paper shows that families of deterministic finite automata (FDFA) are suitable for probabilistic model checking by presenting a polynomial-time algorithm for computing the probability that a Markov chain satisfies an ω-regular property given as an FDFA. It also introduces families of unambiguous finite automata (FUFA), which can be exponentially more succinct than FDFA and unambiguous Büchi automata, and provides a single-exponential translation from LTL to FUFA, compared to a double-exponential lower bound for LTL to FDFA.
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.