Model Checking Quantum Systems --- A Survey <s> Definition 5.1 (Super-operator-valued Markov chains [18]): <s> Abstract Although security of quantum cryptography is provable based on principles of quantum mechanics, it can be compromised by flaws in the design of quantum protocols. So, it is indispensable to develop techniques for verifying and debugging quantum cryptographic systems. Model-checking has proved to be effective in the verification of classical cryptographic protocols, but an essential difficulty arises when it is applied to quantum systems: the state space of a quantum system is always a continuum even when its dimension is finite. To overcome this difficulty, we introduce a novel notion of quantum Markov chain , especially suited for modelling quantum cryptographic protocols, in which quantum effects are encoded as super-operators labelling transitions, leaving the location information (nodes) being classical. Then we define a quantum extension of probabilistic computation tree logic (PCTL) and develop a model-checking algorithm for quantum Markov chains. <s> BIB001 </s> Model Checking Quantum Systems --- A Survey <s> Definition 5.1 (Super-operator-valued Markov chains [18]): <s> 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. <s> BIB002 </s> Model Checking Quantum Systems --- A Survey <s> Definition 5.1 (Super-operator-valued Markov chains [18]): <s> 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. <s> BIB003 </s> Model Checking Quantum Systems --- A Survey <s> Definition 5.1 (Super-operator-valued Markov chains [18]): <s> 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/ . <s> BIB004 </s> Model Checking Quantum Systems --- A Survey <s> Definition 5.1 (Super-operator-valued Markov chains [18]): <s> 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. <s> BIB005
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.