175 citations · 1.2k across the 63 of their papers we have counts for
8 papers · 1 filter
Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains
Ming Xu, Jingyi Mei, Ji Guan +2
Verifying quantum systems has attracted a lot of interest in the last decades.In this paper, we study the quantitative model-checking of quantum continuous-time Markov chains (quan…
A Quantum Interpretation of Bunched Logic for Quantum Separation Logic
Li Zhou, Gilles Barthe, Justin Hsu +2
We propose a model of the substructural logic of Bunched Implications (BI) that is suitable for reasoning about quantum states. In our model, the separating conjunction of BI descr…
A Probabilistic Logic for Verifying Continuous-time Markov Chains
Ji Guan, Nengkun Yu
A continuous-time Markov chain (CTMC) execution is a continuous class of probability distributions over states. This paper proposes a probabilistic linear-time temporal logic, name…
Quantum Temporal Logic
Nengkun Yu
In this paper, we introduce a model of quantum concurrent program, which can be used to model the behaviour of reactive quantum systems and to design quantum compilers. We investig…
Relational Proofs for Quantum Programs
Gilles Barthe, Justin Hsu, Mingsheng Ying +2
Relational verification of quantum programs has many potential applications in quantum and post-quantum security and other domains. We propose a relational program logic for quantu…
Reachability and Termination Analysis of Concurrent Quantum Programs
Nengkun Yu, Mingsheng Ying
We introduce a Markov chain model of concurrent quantum programs. This model is a quantum generalization of Hart, Sharir and Pnueli's probabilistic concurrent programs. Some charac…