Quantum state transformations and branching distributed temporal logic (Invited paper)

Abstract

The Distributed Temporal Logic DTL allows one to reason about temporal properties of a distributed system from the local point of view of the system's agents, which are assumed to execute independently and to interact by means of event sharing. In this paper, we introduce the Quantum Branching Distributed Temporal Logic , a variant of DTL able to represent quantum state transformations in an abstract, qualitative way. In , each agent represents a distinct quantum bit (the unit of quantum information theory), which evolves by means of quantum transformations and possibly interacts with other agents, and n-ary quantum operators act as communication/synchronization points between agents. We endow with a DTL-style semantics, which fits the intrinsically distributed nature of quantum computing, we formalize a labeled deduction system for , and we prove the soundness of this deduction system with respect to the given semantics. Finally, we discuss possible extensions of our system in order to reason about entanglement phenomena. © 2014 Springer-Verlag.