Classical-Quantum State Quantum Markov Chains and Finiteness

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. 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. 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.