Quantum Probabilistic Dyadic Second-Order Logic

We propose an expressive but decidable logic for reasoning about quantum systems. The logic is endowed with tensor operators to capture properties of composite systems, and with probabilistic predication formulas P ^≥ r (s), saying that a quantum system in state s will yield the answer ‘yes’ (i.e. it will collapse to a state satisfying property P) with a probability at least r whenever a binary measurement of property P is performed. Besides first-order quantifiers ranging over quantum states, we have two second-order quantifiers, one ranging over quantum-testable properties, the other over quantum “actions”. We use this formalism to express the correctness of some quantum programs. We prove decidability, via translation into the first-order logic of real numbers.