Büchi automata, semi-deterministic, probabilistic
model-checking