# Reasoning about Quantum Information: An Overview of Quantum Dynamic Logic
## 1 Introduction  
A number of different dynamic-logical systems [1, 2, 3, 4, 5, 6, 7, 8] were developed over the course of the last decade to model the flow of quantum information, each focusing on a specific feature or type of quantum system. In this paper, we bring these different pieces of the puzzle together and provide a guideline through the development of these various logics and their applications. The first design of the main framework of dynamic quantum logic was introduced in [1, 2, 3] by combining two rather different traditions in logic. On the one hand, it uses input from the work on operational quantum logic and in particular the line work on the logical foundations of Quantum Mechanics that was pioneered by [PERSON] and [PERSON] in the 1960s and 1970s in Geneva [9, 10, 11, 12]. On the other hand, it ties in with the \"dynamic turn\" in logic, as pursued (mainly but not exclusively) by the Dutch school in modal logic [13, 14]. A cross-fertilization between these two lines of inquiry has proven to be very fruitful. From the work of [PERSON] and [PERSON], we incorporated features in our mathematical framework which belong to the realm of \"actions and physical dynamics\", stressing the importance of an action-based operational approach to reason about physical properties. From the modal logicians, we borrowed the tools of modeling the dynamics of processes. The standard setting in modal logic makes use of (multi-modal) Kripke models or so-called labeled transition systems, in which the basic ingredients are labeled binary relations on a set of states [14]. In the context of modeling quantum systems, these relations represent actions on the state of a physical system, leading from input states to output states. By combining the Geneva approach and the modal logic approach, one obtains a setting for quantum dynamic logic that is fit to model quantum computational processes. The power of this cross-fertilization comes from the observation that the tools used to model classicalcomputational processes can indeed be adapted to model quantum information flow. We introduced in 2004 first the dynamic version of quantum logic to model the behavior of a single quantum system [2]. Then, we extended in 2004-2006 our framework to model multi-partite (or compound) systems [1; 3]. In our follow-up work, we addressed the issue of providing a probabilistic extension of the framework in [7; 8]. In this paper, we will take the reader through this development, gradually introducing our logical setting in several stages. In the first stage, we will focus on the logical analysis of quantum actions, following the work in [2; 4]. This fragment of our quantum dynamic logic allows us to fully model the global quantum behavior of any quantum system. In the next stage, we zoom in on the local information that is linked to a quantum system, allowing us to express the properties of separability, entanglement, and (non)-locality [1; 3]. Such aspects of (non)-locality appear when we focus on local properties of quantum (sub)systems, and their analysis requires specific logical features that come from spatial or epistemic logics. To proceed in this second stage, we explain the epistemic parts of dynamic quantum logic, following the presentation in [5; 6]. Via the use of epistemic logical features, we can describe the information that is potentially available at a specific location or stored in a specific quantum (sub)system. We further show how our framework provides a characterization of entanglement and separability in pure epistemic terms. In the third stage of this paper, we focus on the probabilistic features of quantum mechanics and incorporate an operator that allows us to express the fact that quantum measurements are inherently non-deterministic [7; 8]. Thus, even if we knew the original state of the system, we may still be unable to predict with certainty the result of the measurement (except in very special cases), yet we can give a probabilistic estimate.