ABSTRACT:

We define a quantum temporal logic, QTL, for the specification of the concurrent quantum programs. QTL first introduces a concurrent quantum programming model to characterize the behavior of the most general reactive distributed quantum programs, including the quantum leader election algorithm and the dining philosophers in the quantum setting. QTL suggests the time-dependence of events including the basic temporal operators, eventually, Always, and employs the projections on subspaces as atomic propositions. We prove Bohm-Jacopini Theorems for quantum programs and probabilistic programs, respectively. We further explore the rich mathematical connotations of basic QTL formulae by studying the corresponding decidability problems.

First, we show that, for sequential quantum programs, the problem of whether a subspace contains a limit point of the system state sequence, which can be regarded as an approximate version of the famous Skolem problem is decidable, although the decidability of the original Skolem problem has been open since proposed in the 1930s. Second, for general concurrent programs, we show that Eventually-Always and Always-Eventually are decidable. Notably, the decidability of Always-Eventually can be regarded as a generalization of the famous Skolem-Mahler-Lech Theorem in additive number theory.

BIO:

Nengkun Yu received the B.S. and Ph.D. degrees from the Department of Computer Science and Technology, Tsinghua University, Beijing, China, in July of 2008 and 2013, respectively. From January 2014 to July 2016, he was a postdoc at the Institute for Quantum Computing at the University of Waterloo. He is now with the Centre for Quantum Software and Information, University of Technology Sydney, Australia as Senior Lecturer. His research interest focuses on quantum information science.

Hosted by Professor Jens Palsberg