Classical Reasoning About Quantum Systems

Rohit Chadha, Paulo Mateus, Amı́lcar Sernadas +1 more

Hartmann Römer

From a general abstract system theoretical perspective, a quantum-like system description in the spirit of a generalized Quantum Theory may appear to be simpler and more natural than a classically inspired description. We investigate the reasons why we nevertheless conceive ourselves embedded into a classically structured world. Categorial, physical and pragmatic reasons are proposed as explanations.

Paulo Mateus, Amı́lcar Sernadas

Paulo Mateus, Jaime Ramos, Amı́lcar Sernadas +1 more

Reasoning about quantum systems has gained prominence due to a big potential in applications such as information processing, security, distributed systems, and randomized algorithms. This fact has attracted research in formal reasoning about quantum states, programs, and processes. On the other hand, temporal logics have proved to be successful in the verification of classical distributed systems and security protocols. In this chapter we extend exogenous quantum propositional logic with temporal modalities, considering both linear and branching time. We provide a weakly complete Hilbert calculi for the proposed quantum temporal logics and study their SAT and model-checking problems. 10.1 Introduction Reasoning about quantum systems has gained prominence due to their potential applications in information processing, security, distributed systems and randomized algorithms. This has attracted research in formal reasoning about quantum states (see for instance van der Meyden and Patra 2003b, a; Mateus and Sernadas 2006; Chadha et al. 2009; Caleiro et al. 2006) and quantum programs (cf. Knill 1996; Sanders and Zuliani 2000; Abramsky and Coecke 2004; D'Hondt and Panangaden 2004; Altenkirch and Grattage 2005; Selinger and Valiron 2005; Baltag and Smets 2006; Baltazar et al. 2007; Chadha et al. 2006, 2007; Baltazar et al. 2008). On the other hand, formal methods have proved to be successful in design and verification of classical distributed systems and security protocols (e.g., Clarke and Wing 1996; Meadows 2003). Herein, we present branching and linear temporal logics for reasoning about evolution of quantum systems composed of a fixed finite set of qubits.

Pedro Baltazar, Rohit Chadha, Paulo Mateus +1 more

Logics for reasoning about quantum states have been given in the literature. In this paper, we extend one such logic with temporal constructs mimicking the standard computational tree logic used to reason about classical transition systems. We investigate the model-checking problem for this temporal quantum logic and illustrate its use by reasoning about the BB84 key distribution protocol.

M. Dalla Chiara, Roberto Giuntini, Richard J. Greechie