Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1   Introduction

The traditional methods of “static” propositional (and first-order) logic dating back to the first part of the last century are limited with respect to their ability to handle physical systems, especially if we focus on their dynamic, spatial and temporal properties, aspects of uncertainty or probabilistic features. In the meantime several new logical methods have been developed, such as modal logics, in particular propositional dynamic logic (PDL) and temporal logic, dynamic epistemic logics, resource-sensitive logics, game-logics and (in)dependence friendly logics to name just a few. In this paper I follow the dynamic modal logic tradition, which ties in nicely with the work on action logics used in computer science. My aim is to show explicitly how a dynamic modal logic approach can provide the adequate tools to deal with quantum physical systems and moreover, I will point out how this setting provides us with a new methodology to talk about quantum behavior. The methodology fits in line with the dynamic view on logic (as it’s practiced by the “Amsterdam school in logic”, see e.g. [7, 8]) by focusing, not so much on the ‘static’ features such as propositions, theories or properties, but on dynamic ones such as: theory change, evaluations, processes, actions, interactions, knowledge updates, communication and observations.

From a more general point of view, the approach adopted in this paper brings together two lines of work: 1) the traditional work on operational quantum logic and 2) a specific information theoretic perspective on quantum systems. As with respect to the first direction, the work on operational quantum logic within the Geneva School on quantum logic originated with [27,18,19,20,29,28,25]. In this work one interprets the logical structure of quantum (and classical) propositions of a physical system by relating it directly to experimental situations. Quantum logic is here not conceived as a “merely” abstract theory (as in [21]) but is provided with an operational dimension which explicitly incorporates features belonging to the realm of “actions and physical dynamics”. The second direction refers to the information theoretic part which lines up with the older tradition in computer science of thinking about information systems in a dynamic manner. In this view, a “state” of a system is being identified with the actions that can be (successfully) performed on that state. In theoretical computer science this has given rise to the study of various semantic (classical) notions of “process” (such as e.g. labeled transition systems, automata and coalgebras). Bringing these two lines of work together, I show in the following sections how one can proceed by analogy with the work on labeled transition systems and present a quantum variant of it.

I start in the next section by introducing the necessary background knowledge on labelled transition systems, which is the standard method used in modal logic and in the applications of computer science to represent processes. To reason about these processes in Section 3, I go over the standard setting of PDL. In Section 4, I give a quantum interpretation to the language of PDL and show how the setting of quantum transition systems can improve on the known theorems in traditional quantum logic. Note that in this paper no new technical results are being introduced, this paper serves the purpose of highlighting how the classical techniques of modal logics and labeled transitions systems can be adapted and applied to obtain a quantum setting.

2   Labeled Transition Systems

Similar as in [16], I take a process to refer to “some object or system whose state changes in time”. Note that the logicians’ use of process does not necessarily fit in line with the so-called school on process philosophy. Broadly viewed, process philosophy relates to the works of Leibniz and Whitehead and is mainly concerned with the ontological nature of processes in the study of metaphysics. One might of course subscribe to the supremacy of processes over other ontological entities, but this is typically not a logician’s first concern. Our concern is to reason about processes, in the sense of modeling their behavior.

In modal logic and its applications in computer science, there is a tradition to represent processes by means of Labeled Transition Systems (LTS for short), also known as multi-modal Kripke models. A LTS is a structure \((S,\{{{ a \atop \rightarrow } \}}_{a\in A},V )\) consisting of a set of states or possible worlds S, a family of binary relations labeled by letters from a given set a ∈ A and a valuation V assigning truth values to atomic sentences (see e.g. [7]). The set A standardly refers to actions, although other interpretations are possible. In a given LTS, defined over a set of actions, the relation \(s{ a \atop \rightarrow } t\) indicates that the process can evolve from input state s to output state t by the execution of action a. As an example, consider the process of getting some money from an ATM modeled as a LTS with basic actions such as “enter your card”; “enter your pin code”; “withdraw 10 euro”, etc. Other standard examples of LTS’s are e.g. those that encode the process of getting a coffee out of a vending machine, making a zerox-copy or performing a specific calculation on a pocket calculator. In the latter case the arrows are labeled by input-actions such as “\(c,+,-,\times,=,0,...9\)” and states will satisfy strings of input symbols (see e.g. [13]).

It is customary to think of actions as simple, “basic” programs having an input state and an output state. These input and output states represent the internal states of the process. Note that external observers (who push buttons on a pocket calculator) might have no access at all to the internal states that are not visible from the outset. The best picture here is that of a “black box” of which we (the observers/users) only experience its behavior in response to our available actions (see [17, 26]). As explained in [26], the black box picture encodes the difference between an LTS and a finite state automaton. In a finite state automaton one first has to provide an input list and then one lets the automaton run to decide if it accepts or rejects the input. Contrary to an LTS, in an automaton one does not see immediately whether each action (that provides an input-item) is rejected or not, one has to wait until the automaton eventually stops running. Further, LTS’s can have an infinite amount of states and hence they differ in an obvious way from finite state automata.

Several types of processes can be represented by the formalism of LTS. Nondeterministic processes can be captured by using branching relations to represent “arbitrary choice”. Similarly, the LTS-formalism can capture the concatenation and iteration of processes by using the composition of transition relations.

Stochastic processes are essentially probabilistic and can be represented by probabilistic versions of labeled transition systems. In the case of a discrete state space, the study of probabilistic transition systems was initiated by Larsen and Skou in [23]. They define a probabilistic transition system (S, {μ s, a }) as a structure consisting of a set of states S and a family of probability distributions μ s, a , one for each action a ∈ A and each input-state s ∈ S. Here, μ s, a : S↦[0, 1] gives the possible next states (and their probabilities) after action a is performed on input-state s. Informally, μ s, a (s′) = x says that action a can be performed in state s and with probability x reaches the state s′ afterwards [23]. Note that the probabilities have to add up: ∑ s′  μ s, a (s′) = 1.

Larsen and Skou’s investigation was first extended to the case of continuous state spaces in [10]. As explained in [11], this means that “we cannot ask for the transition probability [from an input-state] to any [specific output-state, or some arbitrary] set of states - we need to restrict ourselves to measurable sets”. In such a setting, one can model the complex continuous real-time stochastic systems such as the flight management system of an aircraft or the Brownian motion of some molecules [12].

I briefly note here the existence of a general abstract mathematical framework encompassing and unifying all the above-mentioned types of processes and many others: the theory of coalgebras (see e.g. [17, 22]). Coalgebra is a rather new domain of research, drawing mainly upon the mathematical language of Category Theory. A coalgebra, in its most rudimentary form, consists of a state space S endowed with a transition map S → F(S), where F is a functor. By varying the functor, one can accommodate many possible notions of processes: transition systems, deterministic systems, discrete probabilistic systems, continuous stochastic systems etc. For the purpose of this paper, I will not go further into the general framework of coalgebras, restricting myself to the simplest example above (non-probabilistic labeled transition systems). But it is important to stress that, from a general coalgebraic perspective, the above discussion can be extended to other types of processes.

3  Propositional Dynamic Logic

One of the logical systems that provides an axiomatic proof theory to reason about the actions in a LTS is Propositional Dynamic Logic (PDL). PDL and its fragment the Hoare Logic (see e.g. [15]) have been mainly used in the context of program verification in computer science, i.e. when verifying that a given (classical) action or program meets a required specification. In its syntax, PDL uses dynamic formulas to express these actions or programs. Besides the basic actions that were introduced in the previous section, PDL also considers some special kind of actions, called “tests”. Each classical property \(P \in \mathcal{P}(S)\) gives rise to a “test” denoted as P ? . Hence, the actions of PDL could be classified in two types: tests P ? and basic actions A. Semantically this means that I slightly generalize the above given semantic setting to incorporate the two types of actions as follows:

A dynamic frame is a structure \(\mathcal{F} = (S,\{{{ P? \atop \rightarrow } \}}_{P\in \mathcal{L}},\{{{ a \atop \rightarrow } \}}_{a\in A})\), consisting of a set S of states; a family of binary “transition” relations \({ P? \atop \rightarrow } \subseteq S \times S\), which are labeled by “test” actions P ? ; a family of binary “transition” relations \({ a \atop \rightarrow } \subseteq S \times S\), labeled by basic “actions” a ∈ A. Note that the labels for the tests come from a given family \(\mathcal{L}\subseteq \mathcal{P}(S)\) of subsets P ⊆ S, which are called testable properties.

As noted in [1–3], Kripke frames for standard PDL are a special case of dynamic frames, namely those in which one takes \(\mathcal{L} =: \mathcal{P}(S)\), and the transition relation for a test to be given by \(s{ P \atop \rightarrow } t\,\mbox{ iff }\,s = t \in P\). Semantically this is encodes as the diagonal {(w, w) : w ∈ P} of the set P. As noted in [2], intuitively P ? can be thought of as a “purely epistemic” action by a (external) observer who “tests” property P, without affecting the state of the system. The transitions \({ a \atop \rightarrow }\) are binary relations on S.

The logical language of standard (star-free) PDL consists of two levels: a level of propositional sentences φ (expressing properties) and a level of programs or actions π which are defined by mutual induction:

$$\begin{array}{l} \varphi \quad ::= \quad p\vert \quad \neg \varphi \vert \quad \varphi \wedge \varphi \vert \quad [\pi ]\varphi \\ \pi \quad ::= \quad a\vert \quad \varphi ?\vert \quad \pi \cup \pi \vert \quad \pi ;\pi \end{array}$$

Here I take p ∈ Ω and Ω to be a given set of basic (elementary) propositions. The set of basic action labels A is given with a ∈ A. I use ¬to denote classical negation and ∧ for classical conjunction. The modal operators [π] are labeled by actions π and in this I allow for complex action or program constructions such as the non-deterministic choice of actions π ∪π and relational composition π; π. I use labeled modal operators to build a particular type of formulas [π]φ, which construct a new formula from a given program π and formula φ. Here [π]φ is used to express weakest preconditions, which means that if program π would be performed on the current state of the system then the output state will necessarily satisfy φ. The PDL test φ ? denotes the action of testing for φ in the way as is defined in the above semantics for standard PDL. Hence the test action φ ? is successful if and only if φ is true and testing for φ leaves the state of the system unchanged, in all other cases the test fails. In line with [6], we note that all these complex program constructors make PDL particularly well fit for the task of program verification as it becomes easy in this setting to express programming constructs such as if then else or do while-loops (see [15]). In a way this indicates the importance of lifting this setting to a quantum framework, precisely because of the contributions it can offer to the work on quantum program (or quantum protocol) verification (as in [1, 3]).

4  Dynamic Quantum Logic

In this section, I show how the ideas presented in the previous sections can be extended to a quantum framework. I don’t present new technical results here but provide an overview of the main ideas of Dynamic Quantum Logic as presented in a series of papers [2,1,3,4,5,6,30].

In [2] it was first shown how Hilbert spaces can be structured as non-classical relational models. These models are a quantum version of the LTS’s introduced above. I call a Quantum Transition Systems (or QTS) a dynamic frame \((S,\{{{ P? \atop \rightarrow } \}}_{P\in \mathcal{L}},\{{{ a \atop \rightarrow } \}}_{a\in A})\) satisfying a set of ten abstract semantic conditions. In this case the states in S are meant to represent the possible states of a quantum physical system and the transition relations describe the changes of state induced by the possible actions that may be performed on that quantum system. As before I use the notation \(\mathcal{L}\) to denote the set of testable properties. Any such QTS can be equipped with a so-called measurement relation, which allows for the existential quantification over tests as follows: \(s\rightarrow t\,\mbox{ iff }\,s{ P? \atop \rightarrow } t\,\mbox{ for some }\,P \in \mathcal{L}\). The negation of the measurement relation gives rise to an orthogonality relation, so I write s ⊥ t iff s ↛ t. For any set P ⊆ S, I write t ⊥ P iff t ⊥ sfor alls ∈ P and the orthogonal (or orthocomplement) of the set P is defined as follows: ∼ P : = {t ∈ S : t ⊥ P}. The biorthogonal closure of a setP is given by the set ∼ ∼ P =  ∼ ( ∼ P).

In the following list of semantic frame conditions in a QTS, I take the variables P, Q to range over testable properties in \(\mathcal{L}\), the variables s, t, s′, t′, v, w range over states in S and a ranges over basic actions (which are also called “unitary evolutions”) [2]:

Frame Conditions

  1. 1.

    Closure under arbitrary conjunctions: \(\mbox{ if }\mathcal{L}\prime\subseteq \mathcal{L}\mbox{ then }\bigcap \nolimits \mathcal{L}\prime\in \mathcal{L}\)

  2. 2.

    Atomicity. States are testable, i.e. \(\{s\} \in \mathcal{L}\). This is equivalent to requiring that “states can be distinguished by tests”, i.e. \(\mbox{ if }s\not =t\mbox{ then }\exists P \in \mathcal{L} :\,\,\, s \perp P,\,t\not\perp P\)

  3. 3.

    Adequacy. Testing a true property does not change the state:\(\mbox{ if }s \in P\mbox{ then }s{ P? \atop \rightarrow } s\)

  4. 4.

    Repeatability. Any property holds after it has been successfully tested:\(\mbox{ if }s{ P? \atop \rightarrow } t\mbox{ then }t \in P\)

  5. 5.

    “Covering Law”. If \(s{ P \atop \rightarrow } w\not =t \in P\), then there exists some v ∈ P such that t → v ↛ s.

  6. 6.

    Self-Adjointness Axiom: if \(s{ P? \atop \rightarrow } w\rightarrow t\) then there exists some element v ∈ S such that \(t{ P? \atop \rightarrow } v\rightarrow s\)

  7. 7.

    Proper Superposition Axiom. Every two states of a quantum system can be properly superposed into a new state: ∀s, t ∈ S  ∃w ∈ S s → w → t

  8. 8.

    Reversibility and Totality Axioms. Basic unitary evolutions are total bijective functions: \(\forall t \in S\,\,\exists !s\,s{ a \atop \rightarrow } t\) and \(\forall s \in S\,\,\exists !t\,s{ a \atop \rightarrow } t\)

  9. 9.

    Orthogonality Preservation. Basic unitary evolutions preserve (non) orthogonality: Let s, t, s′, t′ ∈ S be such that \(s{ a \atop \rightarrow } s\prime\)and \(t{ a \atop \rightarrow } t\prime\). Then: s → t iff s′ → t′.

  10. 10.

    Mayet’s Condition: Orthogonal Fixed Points. There exists some unitary evolution a ∈ A and some property \(P \in \mathcal{L}\),such that a maps P into a proper subset of itself; and moreover the set of fixed-point states of a has dimension ≥ 2. In other words: \(\exists a \in A\exists P \in \mathcal{L}\exists t,w \in S\forall s \in \sim \sim \{ t,w\} :\) a(P) ⊆ P, a(P) ≠ P, t ⊥ w, a(s) = s.

As shown in [2], these 10 conditions imply that \(\mathcal{L}\), with set-inclusion as partial order, forms an orthomodular lattice of infinite height satisfying all the necessary conditions for the representation theorem of Piron, Solèr and Mayet to hold (see [24, 28, 31]). To understand this result, let us first call a concrete QTS a QTS which is given by an infinite-dimensional Hilbert space H. In the concrete case, the “states” in S are taken to the one-dimensional closed linear subspaces of H, \(\mathcal{L}\) is then given by the family of closed linear subspaces of H and the relations that are labeled by testable properties \({ P? \atop \rightarrow }\) will correspond to (successful) quantum tests (given by the projectors onto the closed linear subspace corresponding to property P). The relations \({ a \atop \rightarrow }\) correspond to linear maps (expressing the so-called “quantum gates”) a on H. The important result for this setting, proved in [2], shows an “Abstract Soundness and Completeness” theorem for the Hilbert-space semantics. In particular, the results in [2] show how every (abstract) QTS can be canonically embedded in the concrete QTS associated to an infinite-dimensional Hilbert space, i.e. every concrete QTS is a QTS and every QTS is isomorphic to a concrete QTS.

We argued in [2, 4–6] for the importance of these results. By moving to the QTS setting it is possible to solve some of the main problems posed in the traditional quantum logic work on orthoframes, such as the problem that orthomodularity could not be captured by a first-order frame condition (as shown in [14]). In contrast, in a QTS this problem is solved: orthomodularity now does correspond to a first-order frame condition and receives a natural dynamic interpretation. In a similar fashion we refrased the “Mayet condition”, which previously could only be stated using the second-order notion of a lattice isomorphism. The “Mayet condition” has now been “internalized” in the setting via the use of quantum actions. Hence from a logical perspective, the QTS formalism yields an improvement of the traditional quantum logic setting.

The QTS structures provide us with the models for a propositional logical system that is different but still close to traditional PDL. The logic is called the Logic of Quantum Actions (LQA) in [2, 4–6] and has the same syntactic language as (star-free) PDL. Let us restrict our quantum setting to the language without classical negation ¬in this paper. This (star-free and classical negation-free) language of PDL can be interpreted in a QTS. All the actions are now interpreted as quantum actions, in particular the test operation will correspond to a quantum test and a basic action is interpreted as a quantum gate. The complex program expressions can now be interpreted as quantum programs.Footnote 1

Note that traditional orthomodular quantum logic (in the tradition of work by [9]) can be re-interpreted inside LQA. This can be done by defining the orthocomplement of a property as the impossibility of a successful test, i.e. ∼ φ : = [φ ? ] ⊥ . Note that the operation of “quantum join” is definable via de Morgan law as φ ⊔ ψ : = ∼ ( ∼ φ ∧ ∼ ψ) and the traditional “quantum implication (or so-called Sasaki hook) is given by the weakest precondition φ → ψ : = [φ ? ]ψ. This re-interpretation provides us with a dynamic and operational characterization of all the non-classical connectives of traditional quantum logic.