17 citations · 57 across the 9 of their papers we have counts for
5 papers · 1 filter
Quantum Relational Hoare Logic with Expectations
Yangjia Li, Dominique Unruh
We present a variant of the quantum relational Hoare logic from (Unruh, POPL 2019) that allows us to use "expectations" in pre- and postconditions. That is, when reasoning about pa…
Approximate Bisimulation and Discretization of Hybrid CSP
Gaogao Yan, Li Jiao, Yangjia Li +2
Hybrid Communicating Sequential Processes (HCSP) is a powerful formal modeling language for hybrid systems, which is an extension of CSP by introducing differential equations for m…
A Theorem Prover for Quantum Hoare Logic and Its Applications
Tao Liu, Yangjia Li, Shuling Wang +2
Quantum Hoare Logic (QHL) was introduced in Ying's work to specify and reason about quantum programs. In this paper, we implement a theorem prover for QHL based on Isabelle/HOL. By…
(Un)decidable Problems about Reachability of Quantum Systems
Yangjia Li, Mingsheng Ying
We study the reachability problem of a quantum system modelled by a quantum automaton. The reachable sets are chosen to be boolean combinations of (closed) subspaces of the state s…
Termination of Nondeterministic Quantum Programs
Yangjia Li, Nengkun Yu, Mingsheng Ying
We define a language-independent model of nondeterministic quantum programs in which a quantum program consists of a finite set of quantum processes. These processes are represente…