Model Checking Quantum Continuous-Time Markov Chains

TL;DR

This paper introduces a novel model checking approach for quantum continuous-time Markov chains (QCTMCs), utilizing signal temporal logic and advanced real root isolation algorithms to verify quantum systems efficiently.

Contribution

The paper develops the first model checking framework for QCTMCs using STL and a new real root isolation algorithm under Schanuel's conjecture, enabling efficient verification.

Findings

Effective verification of quantum systems demonstrated on open quantum walk example.

Linear query complexity in the size of the STL formula.

Development of a state-of-the-art real root isolation algorithm.

Abstract

Verifying quantum systems has attracted a lot of interests in the last decades. In this paper, we initialised the model checking of quantum continuous-time Markov chain (QCTMC). As a real-time system, we specify the temporal properties on QCTMC by signal temporal logic (STL). To effectively check the atomic propositions in STL, we develop a state-of-art real root isolation algorithm under Schanuel's conjecture; further, we check the general STL formula by interval operations with a bottom-up fashion, whose query complexity turns out to be linear in the size of the input formula by calling the real root isolation algorithm. A running example of an open quantum walk is provided to demonstrate our method.