Quantum Markov chains: description of hybrid systems, decidability of equivalence, and model checking linear-time properties

TL;DR

This paper introduces a quantum Markov chain model for hybrid quantum-classical systems, proves polynomial-time decidability of equivalence problems, and demonstrates effective model checking of linear-time properties.

Contribution

It proposes a new hybrid quantum automata model, establishes polynomial-time decidability of key equivalence problems, and advances model checking techniques for quantum systems.

Findings

Polynomial-time decidability of language and trace equivalence for HQA and quantum Markov chains.

Effective model checking of linear-time properties in quantum Markov chains.

Hybrid quantum automata can describe quantum-classical hybrid systems with practical verification methods.

Abstract

In this paper, we study a model of quantum Markov chains that is a quantum analogue of Markov chains and is obtained by replacing probabilities in transition matrices with quantum operations. We show that this model is very suited to describe hybrid systems that consist of a quantum component and a classical one, although it has the same expressive power as another quantum Markov model proposed in the literature. Indeed, hybrid systems are often encountered in quantum information processing; for example, both quantum programs and quantum protocols can be regarded as hybrid systems. Thus, we further propose a model called hybrid quantum automata (HQA) that can be used to describe these hybrid systems that receive inputs (actions) from the outer world. We show the language equivalence problem of HQA is decidable in polynomial time. Furthermore, we apply this result to the trace equivalence problem of quantum Markov chains, and thus it is also decidable in polynomial time. Finally, we discuss model checking linear-time properties of quantum Markov chains, and show the quantitative analysis of regular safety properties can be addressed successfully.