ﻻ يوجد ملخص باللغة العربية
Fidelity is one of the most widely used quantities in quantum information that measure the distance of quantum states through a noisy channel. In this paper, we introduce a quantum analogy of computation tree logic (CTL) called QCTL, which concerns fidelity instead of probability in probabilistic CTL, over quantum Markov chains (QMCs). Noisy channels are modelled by super-operators, which are specified by QCTL formulas; the initial quantum states are modelled by density operators, which are left parametric in the given QMC. The problem is to compute the minimumfidelity over all initial states for conservation. We achieve it by a reduction to quantifier elimination in the existential theory of the reals. The method is absolutely exact, so that QCTL formulas are proven to be decidable in exponential time. Finally, we implement the proposed method and demonstrate its effectiveness via a quantum IPv4 protocol.
Parametric Markov chains occur quite naturally in various applications: they can be used for a conservative analysis of probabilistic systems (no matter how the parameter is chosen, the system works to specification); they can be used to find optimal
We revisit the symbolic verification of Markov chains with respect to finite horizon reachability properties. The prevalent approach iteratively computes step-bounded state reachability probabilities. By contrast, recent advances in probabilistic inf
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 si
Many complex systems can be described by population models, in which a pool of agents interacts and produces complex collective behaviours. We consider the problem of verifying formal properties of the underlying mathematical representation of these
Knowledge-based programs provide an abstract level of description of protocols in which agent actions are related to their states of knowledge. The paper describes how epistemic model checking technology may be applied to discover and verify concrete