Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata (opens in new tab)

Families of deterministic finite automata (FDFA) have been introduced as a concise automaton model that characterizes $\omega$-regular languages by processing their ultimately periodic words. FDFA are known to enjoy many good properties and can be exponentially more succinct than deterministic $\omega$-automata with Rabin, Streett or parity acceptance. This paper addresses two main questions: (1) Are FDFA suitable for probabilistic model checkin...