• 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.
Jens Chr. Godskesen (Fri,) studied this question.