Model Checking

Model Checking Omega-regular Properties for Quantum Markov Chains
Quantum Markov chains are an extension of classical Markov chains which are labelled with super-operators rather than probabilities. …
Yuan Feng, \Ernst Moritz\ Hahn, Andrea Turrini, Shenggang Ying
引用 DOI
Asymptotic Perturbation Bounds for Probabilistic Model Checking with Empirically Determined Probability Parameters
Guoxin Su, Yuan Feng, Taolue Chen, David S. Rosenblum
引用 DOI
Verify LTL with Fairness Assumptions Efficiently
Yong Li, Lei Song, Yuan Feng, Lijun Zhang
引用 DOI
Quantum Markov chains: Description of hybrid systems, decidability of equivalence, and model checking linear-time properties
In this paper, we study a model of quantum Markov chains that is a quantum analogue of Markov chains and is obtained by replacing …
Lvzhou Li, Yuan Feng
引用 DOI URL
Model-Checking Linear-Time Properties of Quantum Systems
We define a formal framework for reasoning about linear-time properties of quantum systems in which quantum automata are employed in …
Mingsheng Ying, Yangjia Li, Nengkun Yu, Yuan Feng
引用 DOI URL
Model checking quantum Markov chains
Although security of quantum cryptography is provable based on principles of quantum mechanics, it can be compromised by flaws in the …
Yuan Feng, Nengkun Yu, Mingsheng Ying
引用 DOI URL