17 citations · 57 across the 9 of their papers we have counts for
10 papers
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…
Robust Regions of Attraction Generation for State-Constrained Perturbed Discrete-Time Polynomial Systems
Bai Xue, Naijun Zhan, Yangjia Li
In this paper we propose a convex programming based method for computing robust regions of attraction for state-constrained perturbed discrete-time polynomial systems. The robust r…
Robust Non-termination Analysis of Numerical Software
Bai Xue, Naijun Zhan, Yangjia Li +1
Numerical software are widely used in safety-critical systems such as aircrafts, satellites, car engines and so on, facilitating dynamics control of such systems in real time, it i…
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…
On Termination of Polynomial Programs with Equality Conditions
Yangjia Li, Naijun Zhan, Mingshuai Chen +3
We investigate the termination problem of a family of multi-path polynomial programs (MPPs), in which all assignments to program variables are polynomials, and test conditions of l…
Debugging Quantum Processes Using Monitoring Measurements
Yangjia Li, Mingsheng Ying
Since observation on a quantum system may cause the system state collapse, it is usually hard to find a way to monitor a quantum process, which is a quantum system that continuousl…
(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…
Local Unambiguous Discrimination with Remaining Entanglement
Yangjia Li, Runyao Duan, Mingsheng Ying
A bipartite state which is secretly chosen from a finite set of known entangled pure states cannot be immediately useful in standard quantum information processing tasks. To effect…