Model checking ω-regular properties for quantum Markov chains

Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, Shenggang Ying

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

7 Citations (Scopus)
19 Downloads (Pure)


Quantum Markov chains are an extension of classical Markov chains which are labelled with super-operators rather than probabilities. They allow to faithfully represent quantum programs and quantum protocols. In this paper, we investigate model checking !-regular properties, a very general class of properties (including, e.g., LTL properties) of interest, against this model. For classical Markov chains, such properties are usually checked by building the product of the model with a language automaton. Subsequent analysis is then performed on this product. When doing so, one takes into account its graph structure, and for instance performs different analyses per bottom strongly connected component (BSCC). Unfortunately, for quantum Markov chains such an approach does not work directly, because super-operators behave differently from probabilities. To overcome this problem, we transform the product quantum Markov chain into a single super-operator, which induces a decomposition of the state space (the tensor product of classical state space and the quantum one) into a family of BSCC subspaces. Interestingly, we show that this BSCC decomposition provides a solution to the issue of model checking ω-regular properties for quantum Markov chains.

Original languageEnglish
Title of host publication28th International Conference on Concurrency Theory, CONCUR 2017
EditorsRoland Meyer, Uwe Nestmann
Place of PublicationLeibniz
Number of pages16
ISBN (Electronic)978-3-95977-048-4
Publication statusPublished - 2017
Externally publishedYes
Event28th International Conference on Concurrency Theory, CONCUR 2017 - Berlin, Germany
Duration: 5 Sept 20178 Sept 2017

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
ISSN (Print)1868-8969


Conference28th International Conference on Concurrency Theory, CONCUR 2017


  • Bottom strongly connected component
  • Model checking
  • ω-regular properties
  • Quantum Markov chains


Dive into the research topics of 'Model checking ω-regular properties for quantum Markov chains'. Together they form a unique fingerprint.

Cite this