Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata

Christel Baier, Sascha Klüppelholz, Timm Spork

Families of deterministic finite automata (FDFA) have been introduced as a concise automaton model that characterizes $\omega$-regular languages by processing their ultimately periodic…