Some formal tools for analyzing quantum automata

Andris Ambainis, Martin Beaudry, Marats Golovkins +3 more

René Bødker Christensen, Nikolaj Rossander Kristensen, Kim G. Larsen +3 more

Abstract We introduce a formal modeling methodology to analyze quantum communication protocols in the tool Uppaal . Our approach encodes quantum states, operations, and measurements into Uppaal timed automata with data extensions and external function calls, enabling both exhaustive verification in the ideal (noiseless) case and statistical model checking for realistic noisy scenarios. We apply our framework to the Beyond Superdense Coding protocol—a time-slotted variant of superdense coding—combined with quantum entanglement distillation, and demonstrate that Uppaal can deal with these protocols even under complex timing and decoherence constraints.

Robert J. Irwin, Howard A. Blair

We show how to construct quantum cellular automata (QCA) based on the formalism introduced by Watrous but without that formalism's "quiescent states," by using shift-invariant Lebesgue measure on Cantor space. Although QCA's with quiescent states are strictly sufficient for computational purposes, removing quiescent states as a requirement allows global QCA states with infinite support that allows the state space of the QCA to be identified with the class of interpretations of logic-based formalism in a formal methods approach to proving the correctness correctness of QCAs with respect to formal specifications.

Andris Ambainis, Martin Beaudry, Marats Golovkins +3 more

Andris Ambainis, Martin Beaudry, Marats Golovkins +3 more

Andrea Pizzi, Norman Y. Yao

Information theoretic measures have helped to sharpen our understanding of many-body quantum states. As perhaps the most well-known example, the entanglement entropy (or more generally, the bipartite mutual information) has become a powerful tool for characterizing the dynamical growth of quantum correlations. By contrast, although computable, the bipartite mutual information (MI) is almost never explored in classical many particle systems; this owes in part to the fact that computing the MI requires keeping track of the evolution of the full probability distribution, a feat which is rarely done (or thought to be needed) in classical many-body simulations. Here, we utilize the MI to analyze the spreading of information in 1D elementary cellular automata (CA). Broadly speaking, we find that the behavior of the MI in these dynamical systems exhibits a few different types of scaling that roughly correspond to known CA universality classes. Of particular note is that we observe a set of automata for which the MI converges parametrically slowly to its thermodynamic value. We develop a microscopic understanding of this behavior by analyzing a two-species model of annihilating particles moving in opposite directions. Our work suggests the possibility that information theoretic tools such as the MI might enable a more fine-grained characterization of classical many-body states and dynamics.