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. © 2013 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Baltag, A., Bergfeld, J. M., Kishida, K., Sack, J., Smets, S. J. L., & Zhong, S. (2013). Quantum probabilistic dyadic second-order logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8071 LNCS, pp. 64–80). Springer Verlag. https://doi.org/10.1007/978-3-642-39992-3_9
Mendeley helps you to discover research relevant for your work.