An Algebraic Method to Fidelity-based Model Checking over Quantum Markov Chains

• DOI: 10.48550/arxiv.2101.04971
• Publication Date: 2021-01-01
• Authors: Ming Xu; Jianling Fu; Jingyi Mei; Yuxin Deng
• Keywords: FOS: Computer and information sciences; 0301 basic medicine; Computer Science - Logic in Computer Science; 03 medical and health sciences; 0102 computer and information sciences; 01 natural sciences; Logic in Computer Science (cs.LO)

Fidelity is one of the most widely used quantities in quantum information that measure distance states through a noisy channel. In this paper, we introduce analogy computation tree logic (CTL) called QCTL, which concerns fidelity instead probability probabilistic CTL, over Markov chains (QMCs). Noisy channels are modelled by super-operators, specified QCTL formulas; initial density operators, left parametric given QMC. The problem to compute minimumfidelity all for conservation. We achieve it reduction quantifier elimination existential theory reals. method absolutely exact, so formulas proven be decidable exponential time. Finally, implement proposed and demonstrate its effectiveness via IPv4 protocol.