• Quantum Markov chain for quantum programs based on classical control and quantum data • A QCTL where a proposition is a pair of a classical state and a projection • Sound and complete translation of quantum Markov chains to DTMCs • Convergence and simple cycles make model checking decidable Several quantum Markov chains and temporal quantum logics have been considered in the literature. In this paper we propose a discrete time classical-quantum state quantum Markov chain (cqQMC) with super-operators over a finite dimensional Hilbert space H . The cqQMC is related to previous proposals but yet with a different semantics in that states are pairs of a classical and a quantum state. We define a quantum temporal logic (QCTL) where propositions are pairs of a classical state and a projection over H . We demonstrate how a cqQMC can be translated to a discrete time Markov chain (DTMC). The translation is sound and complete in that model checking any QCTL formula for a cqQMC can equivalently be carried out by checking the same formula for the inferred DTMC. Taking advantage of the finite classical control we show that even though a cqQMC may have infinitely many states then under certain restrictions the inferred DTMC is finite, and hence model checking is decidable.

Abstraction refinement techniques in probabilistic model checking are prominent approaches for verification of very large or infinite-state probabilistic concurrent systems. At the core of the refinement step lies the implicit or explicit analysis of a counterexample. This article proposes an abstraction refinement approach for the probabilistic computation tree logic (PCTL), which is based on incrementally computing a sequence of may- and must-quotient automata. These are induced by depth-bounded bisimulation equivalences of increasing depth. The approach is both sound and complete, since the equivalences converge to the genuine PCTL equivalence. Experimental results with a prototype implementation show the effectiveness of the approach.