In standard model checking against linear temporal logic (LTL) properties, it is sufficient to translate an LTL formula into a non-deterministic Büchi automaton.
But, in probabilistic model checking, LTL formulae are typically translated into deterministic Rabin automata (DRA), as for instance in the PRISM tool.
Indeed, semi-deterministic Büchi automata are sufficient in probabilistic model checking.
The equivalent semi-deterministic Büchi automaton is A'=(N ∪ D,Σ,∆',Q'0,F'), where Note the structure of states and transitions of A′.
A D-state is defined as a pair of elements of power set of states of A.
Therefore, there exist a strictly increasing and infinite sequence of indexes i0,i1,... such that i0=0 and, for each j > 0, Lij=Rij and Lij≠∅.
This tree is infinite, finitely branching, and fully connected.
Therefore, by Kőnig's lemma, there exists an infinite path (q0,0),(q1,1),(q2,2),... in the tree.
Proof: The definition of projection function Pr can be extended such that in the second argument it can accept a finite word.
In any run, A' can only once make a non-deterministic choice that is when it chooses to take a Δ2 transition and rest of the execution of A' is deterministic.