## 5 Model Checking LTL and \(\omega\)-Regular Properties
### The Standard Automata-Based Approach  
In the standard automata-based approach [62] to LTL model checking in the context of classical Markov chains, the first step requires to transform the given LTL formula \(\varphi\) into an equivalent nondeterministic Buchi automaton accepting the same language as \(\varphi\), i.e., \(\mathit{Words}(\varphi)\); such an automaton always exists (cf. [27] (Theorem 5.37)). Since nondeterministic Buchi automata are as expressive as \(\omega\)-regular languages (cf. [27] (Theorem 4.32)), we can also solve the model checking problem against \(\omega\)-regular properties, by the same approach.  
The nondeterminism present in the Buchi automaton, however, does not play well with the computation of the probability measure. For this motivation, the Buchi automaton needs to be made deterministic; however, deterministic Buchi automata are strictly less expressive than nondeterministic ones (cf. [27] (Theorem 4.50)), so more powerful deterministic automata need to be used. Therefore, the nondeterministic Buchi automaton is transformed into an equivalent deterministic automaton \(\mathfrak{A}\) with a more complex acceptance condition, such as Rabin, Streett, Muller, or parity (cf. [63; 64; 65]). The construction of such deterministic automata usually makes use of a variant of the [PERSON]'s [66] approach, see for instance [67; 68], or some of the more recent Safraless constructions, such as the ones proposed in [69; 70; 71].  
Once the deterministic automaton \(\mathfrak{A}\) is available, it can be combined with the Markov chain \(\mathfrak{M}\) as the product \(\mathfrak{M}\otimes\mathfrak{A}\); this product is in practice a Markov chain extended with the information about the paths that are accepted by the automaton \(\mathfrak{A}\) (i.e., the paths that satisfy the formula \(\varphi\)); we call such a product a parity Markov chain, when \(\mathfrak{A}\) is a parity automaton. As the last step, the probability of the accepting paths is computed. Since all accepting paths need to be infinite, the finite number of states of \(\mathfrak{M}\otimes\mathfrak{M}\) implies that such paths need to become trapped into a set of states from which they cannot escape, that is, the states that form a _bottom strongly connected component_ (BSCC). Intuitively, a BSCC is composed by states that can be reached by each other, and all their successors are also in the same BSCC. These BSCCs can be computed by means of algorithms operating on the graph structure of the product Markov chain; the outcome of these algorithms is a classification of the states of \(\mathfrak{M}\otimes\mathfrak{A}\) as those belonging to a BSCC and the _transient states_, i.e., all other states. Since only states in a BSCC can be visited infinitely often with strictly positive probability, the acceptance condition provided by \(\mathfrak{A}\) is used to mark each BSCC as either accepting or rejecting. As the last step, the probability that \(\varphi\) holds in a given state \(s\) of the Markov chain \(\mathfrak{M}\) is computed by finding the unique solution of a systems of equations: if \(s\) belongs to an accepting BSCC, the probability \(p_{s}\) is 1; if \(s\) belongs to a rejecting BSCC, the probability \(p_{s}\) is 0; if \(s\) is a transient state, then the probability \(p_{s}\) satisfies the Bellman equation \(p_{s}=\sum_{s^{\prime}\in S}\mathbf{P}(s,s^{\prime})\cdot p_{s^{\prime}}\), where \(\mathbf{P}(s,s^{\prime})\) is the probability in \(\mathfrak{M}\) to make a transition from \(s\) to \(s^{\prime}\), i.e., the probabilistic counterpart of \(\mathbf{Q}\) in quantum Markov chains.