You are presented with multiple paper abstracts, alongside the associated literature review and chapter titles. Given the provided information, you are going to do a literature review. Please generate a coherent literature review that synthesizes the content, draws connections between different works, highlights major findings, and identifies any gaps in the existing research.

Literature Review Title: Model Checking Quantum Systems --- A Survey 
Chapter Title:  Definition 5.1 (Super-operator-valued Markov chains [18]): 
1. Abstract of Cited Paper (BIB001):  We introduce the notion of recursive quantum Markov chain (RQMC) for analysing recursive quantum programs with procedure calls. RQMCs are natural extension of Etessami and Yannakakis’s recursive Markov chains where the probabilities along transitions are replaced by completely positive and trace-nonincreasing super-operators on a state Hilbert space of a quantum system. 
2. Abstract of Cited Paper (BIB002):  We introduce the web-based model checker iscasMc for probabilistic systems see http://iscasmc.ios.ac.cn/IscasMC . This Java application offers an easy-to-use web interface for the evaluation of Markov chains and decision processes against PCTL and PCTL* specifications. Compared to PRISM or MRMC, iscasMc is particularly efficient in evaluating the probabilities of LTL properties. 
3. Abstract of Cited Paper (BIB003):  We present QPMC (Quantum Program/Protocol Model Checker), an extension of the probabilistic model checker IscasMC to automatically verify quantum programs and quantum protocols. QPMC distinguishes itself from the previous quantum model checkers proposed in the literature in that it works for general quantum programs and protocols, not only those using Clifford operations. A command-line version of QPMC is available at http://iscasmc.ios.ac.cn/tool/qmc/ . 
4. Abstract of Cited Paper (BIB004):  Quantum Markov chains are an extension of classical Markov chains which are labelled with super-operators rather than probabilities. They allow to faithfully represent quantum programs and quantum protocols. In this paper, we investigate model checking omega-regular properties, a very general class of properties (including, e.g., LTL properties) of interest, against this model. ::: ::: For classical Markov chains, such properties are usually checked by building the product of the model with a language automaton. Subsequent analysis is then performed on this product. When doing so, one takes into account its graph structure, and for instance performs different analyses per bottom strongly connected component (BSCC). Unfortunately, for quantum Markov chains such an approach does not work directly, because super-operators behave differently from probabilities. To overcome this problem, we transform the product quantum Markov chain into a single super-operator, which induces a decomposition of the state space (the tensor product of classical state space and the quantum one) into a family of BSCC subspaces. Interestingly, we show that this BSCC decomposition provides a solution to the issue of model checking omega-regular properties for quantum Markov chains.

Literature Review:
A labelled super-operator-valued Markov chain over a set AP of predefined atomic propositions is a 5-tuple (S, s 0 , H, Q, L), where: 1) S is a finite set of classical states with s 0 ∈ S being the initial state; 2) H is a finite-dimensional Hilbert space, called the quantum state space; 3) Q : S × S → SO H is a transition super-operator function, where SO H denotes the set of trace-nonincreasing super-operators on H, and for each s ∈ S, t∈S Q(s, t) is trace-preserving; and 4) L : S → 2 AP is a labelling function. A super-operator-valued Markov chain has two state spaces, a classical one and a quantum one, which are connected through the transition super-operator function. It behaves in a similar manner as classical Markov chains. It starts from the classical initial state s 0 but with the quantum initial state unspecified (it can be taken arbitrarily). Then at each step, given the current classical state s and quantum state ρ, it proceeds to classical state t with probability tr[Q(s, t)(ρ)], and the accompanied quantum state evolves into Q(s, t)(ρ)/tr[Q(s, t)(ρ)] provided that tr[Q(s, t)(ρ)] = 0. The normalisation requirement that t∈S Q(s, t) is trace-preserving guarantees that the probabilities of going from s to some classical state sum up to 1. As the atomic propositions are taken to be classical (they apply only to classical states), this Markov chain model is suitable for verification of quantum systems against classical properties, such as running time, termination, reachability, etc. One distinct feature of this model, however, for verification purpose, is that it provides a way to check once-for-all in that once a property is checked to hold, it holds for all initial quantum states. For example, for the reachability problem, the model checking algorithm essentially calculates a positive operator Π, accounting for all (classical) paths satisfying the concerned property. Then the reachability probability when the Markov chain is started in the initial quantum state ρ is simply tr(Πρ). A corresponding computation tree logic (CTL) for superoperator-valued Markov chains was defined, and algorithms for checking such properties were developed in BIB001 . A tool implementation of these algorithms has been provided BIB004 based on the probabilistic model checker ISCASMC BIB003 . Algorithms for model checking ω-regular properties, a very general class of properties subsuming those expressible by LTL formulae, against super-operator-valued Markov chains were proposed in BIB005 . This allows to express and analyse a wide range of relevant properties, such as repeated reachability, reachability in a restricted order, nested Until properties, or conjunctions of such properties. Furthermore, the reachability problem of a recursive extension of super-operator-valued Markov chains was studied in BIB002 , with the application of analysing quantum programs with procedure calls.