Model Checking Omega-regular Properties for Quantum Markov Chains

• DOI: 10.4230/lipics.concur.2017.35
• Publication Date: 2017-08-25
• Authors: Yuan Feng; Ernst Moritz Hahn; Andrea Turrini; Shenggang Ying
• Keywords: Markov kernel

Quantum Markov chains are an extension of classical which labelled with super-operators rather than probabilities. They allow to faithfully represent quantum programs and protocols. In this paper, we investigate model checking omega-regular properties, a very general class properties (including, e.g., LTL properties) interest, against model.

For chains, such usually checked by building the product language automaton. Subsequent analysis is then performed on product. When doing so, one takes into account its graph structure, for instance performs different analyses per bottom strongly connected component (BSCC). Unfortunately, approach does not work directly, because behave differently from To overcome problem, transform chain single super-operator, induces decomposition state space (the tensor one) family BSCC subspaces. Interestingly, show that provides solution issue chains.