Luca Viganò

Marco Volpe

Margherita Zorzi

A Branching Distributed Temporal Logic for Reasoning about Quantum State Transformations

Keywords: Quantum Computing, Quantum State Transformations, Temporal Logic, Distributed Temporal Logic, Natural Deduction 1

The Distributed Temporal Logic DTL allows one to reason about temporal properties of a distributed system from the local point of view of the system's agents, which are assumed to execute independently and to interact by means of event sharing. In this paper, we introduce the Quantum Branching Distributed Temporal Logic QBDTL, a variant of DTL able to represent quantum state transformations in an abstract, qualitative way. In QBDTL, each agent represents a distinct quantum bit (the unit of quantum information theory), which evolves by means of quantum transformations and possibly interacts with other agents, and n-ary quantum operators act as communication/synchronization points between agents. We endow QBDTL with a DTL-style semantics, which fits the intrinsically distributed nature of quantum computing, we formalize a labeled deduction system for QBDTL, and we prove the soundness and completeness of this deduction system with respect to the given semantics. We give a number of examples and, finally, we discuss possible extensions of our logic in order to reason about entanglement phenomena.

Introduction

Background and motivation

The Distributed Temporal Logic DTL [START_REF] Ehrich | Specifying communication in distributed information systems[END_REF][START_REF] Basin | Labelled tableaux for distributed temporal logic[END_REF][START_REF] Basin | Distributed Temporal Logic for the Analysis of Security Protocol Models[END_REF] allows one to reason about temporal properties of a distributed system from the local point of view of the system's agents: each asynchronous agent executes independently, evolves linearly along a time-line built upon some local events, and can interact with the other agents by means of event sharing. Distribution is implicit and properties of an entire system are formulated in terms of the local properties of the system's agents and their interaction. DTL's semantics was inspired by a conflict-free version of Winskel's event structures (see, e.g., [START_REF] Winskel | Event structures[END_REF]), enriched with information about sequential agents.

DTL has been initially proposed as a logic for specifying and reasoning about distributed information [START_REF] Ehrich | Specifying communication in distributed information systems[END_REF], but it has also been used in the context of security protocol analysis to reason about the interplay between protocol models and security properties [START_REF] Basin | Distributed Temporal Logic for the Analysis of Security Protocol Models[END_REF]. In this paper, we show that, after a proper extension of the logic's syntax and semantics, DTL is also able to formally model quantum state transformations in an abstract, qualitative way.

Quantum computing is one of the most promising research fields of computer science as well as a concrete future technology (see [START_REF] Nielsen | Quantum computation and quantum information[END_REF] for a useful introduction to the basic notions of quantum computing as we here only very briefly summarize the notions that are relevant to our work in this paper). However, at least from the point of view of theoretical computer science, a number of foundational aspects are still underdeveloped: quantum complexity, quantum computability, quantum programming theory (and its logical account), quantum cryptography and security are all active but open research areas, which still require the development of ad hoc formal methods. These issues are complex to face since the physical model quantum computing is based on is sophisticated and all basic definitions and formal tools have to be reformulated in a non-standard way.

To illustrate this, and our contributions in this paper, in more detail, let us focus our attention on quantum data, in particular on the unit of quantum information, the quantum bit or qubit, for short. The qubit is the quantum counterpart of the classical bit and, mathematically, it is simply a normalized vector of the Hilbert space C 2 . Qubits can assume both classical values 0 and 1 (as the classical bit) and all their superpositional values, i.e., linear combinations such as α|0 + β|1 , where α, β ∈ C are called amplitudes, |α| 2 + |β| 2 = 1 and |c , for c ∈ {0, 1}, is the so called Dirac Notation, which is simply a denotation of basis states (which corresponds to the classical values a bit can assume).

Intuitively, whereas a classical bit can only be 0 or 1, a quantum bit can assume both the value 0 and the value 1 (with a certain associated probability) at the same time. It is possible to modify a quantum bit in two ways:

• by means of a suitable class of algebraic operators called unitary transformations (that are also called quantum gates and are a class of algebraic operators enjoying some good properties, which represent the pure quantum computational steps) or

• by measuring it, i.e., probabilistically reducing it to 0 or 1.

In this paper, we deal only with unitary transformations, leaving measurement for future work.

The definition of a qubit can, of course, be generalized: a quantum register or quantum state is the representation of a system of n qubits (mathematically, it is a normalized vector of the Hilbert space C 2 n ). As for the single qubit, a quantum state can be modified by means of unitary algebraic operators.

Abstracting from any notion of control and considering only pure quantum transformations (i.e., unitary evolution of quantum states as computational steps), it seems to be interesting to provide a logical account of such a computation. The question then is: what is a logical approach suitable to represent quantum state evolution?

Contributions

The main contribution of this paper is the formalization of a logic and of an associated deduction system that allows one to formally represent and reason about unitary transformations of quantum states from a temporal multi-agent system perspective. More specifically, we view our contributions as two-fold.

First, we define the Quantum Branching Distributed Temporal Logic QBDTL, a significant variant of DTL that we introduce here to represent quantum state transformations in an abstract, qualitative way. In QBDTL, we abstract from the value of the qubits: we are not interested in encoding into our system syntactical and semantical information about amplitudes or basis values 0 and 1 (in this way, we avoid any quantitative information) and we focus instead on the way qubits evolve by means of unitary transformations. Following DTL's central notion, in QBDTL we do not only consider globally quantum states but also, and in particular, the single unit of information, i.e., we maintain the local perspective of the qubit in the quantum computation.

In other words, in QBDTL each agent represents a distinct qubit, which is the object/subject of computation and which evolves in time by means of quantum transformations and possibly interacts with other agents/qubits.

There is a crucial difference between our QBDTL and the original DTL formulation. DTL is based on linear time life-cycles for agents. In QBDTL (and this provides an additional contribution of our work), we go beyond linearity and consider branching time since we want to be as general as possible: at each step of the temporal evolution of an agent/qubit, the accessibility relation between worlds in the subtended Kripke-style model aims to capture each possible unitary transformation that can be applied to the qubit. A world (a state in the temporal life-cycle of an agent) represents (an abstraction of) a 1-qubit quantum state. n-ary quantum operators, which act simultaneously on more than one qubit (such as control operators, which play a crucial role in quantum computing), act as communication/synchronization points between agents/qubits.

Second, we give a deduction system N(QBDTL) for QBDTL. In order to deal with all the semantical notions (temporal, quantum and synchronization information), we follow the style of labeled deduction [START_REF] Gabbay | Labelled Deductive Systems[END_REF][START_REF] Simpson | The Proof Theory and Semantics of Intuitionistic Modal Logic[END_REF][START_REF] Viganò | Labelled Non-Classical Logics[END_REF], a framework for giving uniform presentations of different non-classical logics, where labels allow one to explicitly encode in the syntax additional information, of a semantic or proof-theoretical nature, that is otherwise implicit in the logic one wants to capture.

In addition to the works on DTL, and in particular the labeled tableaux system given in [START_REF] Basin | Labelled tableaux for distributed temporal logic[END_REF], our starting points for N(QBDTL) are the labeled natural deduction system for the logic UB (i.e., the until-free fragment of CTL) given in [START_REF] Caleiro | A labeled deduction system for the logic UB[END_REF] and the approach developed in [START_REF] Masini | A qualitative modal representation of quantum state transformations[END_REF][START_REF] Masini | Modal Deduction Systems for Quantum State Transformations[END_REF], where a labeled modal deduction system with specific modalities able to describe quantum state transformations is given. Fittingly, in N(QBDTL), we consider composed labels (i, x, q) that represent an agent/qubit i, a time instant x, and the quantum information q in the underlying semantics. A further class of labels is used to represent paths in the life-cycles of the agents.

The rules of N(QBDTL) can then be divided into rules that formalize the local temporal evolution of an agent/qubit, and synchronization rules that are, in a sense, global as they lift the reasoning from the local perspective of the agent to the distributed perspective induced by agent's synchronizations.

Related Work

It is important to observe that our QBDTL is not a quantum logic. Since the work of Birkhoff and von Neumann [START_REF] Birkhoff | The logic of quantum mechanics[END_REF], various logics have been investigated as a means to formalize reasoning about propositions taking into account the principles of quantum theory, e.g., [START_REF] Dalla Chiara | Quantum logic[END_REF]. In general, it is possible to view quantum logic as a logical axiomatization of quantum theory, which provides an adequate foundation for a theory of reversible quantum processes, e.g., [START_REF] Mittelstaedt | The modal logic of quantum logic[END_REF][START_REF] Abramsky | A categorical quantum logic[END_REF][START_REF] Baltag | The logic of quantum programs[END_REF][START_REF] Baltag | LQP: the dynamic logic of quantum information[END_REF][START_REF] Baltag | Quantum logic as a dynamic logic[END_REF][START_REF] Engesser | A New Approach to Quantum Logic[END_REF][START_REF] Engesser | Handbook of Quantum Logic and Quantum Structures[END_REF]. Research has focused also on automated reasoning (e.g., model checking for quantum systems as considered in [START_REF] Gay | QMC: A Model Checker for Quantum Systems[END_REF]) and on formal analysis of quantum protocols (e.g., [START_REF] Kouvaros | Automatic verification of parameterised multiagent systems[END_REF]). Our work moves from quite a different point of view, which, to reiterate, is the wish to provide a deduction system able to represent and reason about unitary transformations of quantum states from a temporal multi-agent system perspective and, as will become clear below, thereby provide a basis to reason about other, more complex properties of quantum states such as entanglement.

This paper extends and supersedes our preliminary account of QBDTL given in [START_REF] Viganò | Quantum state transformations and branching distributed temporal logic[END_REF].

Organization

We proceed as follows. In Section 2, we give a brief overview of the basic notions of quantum computing that are relevant for this paper. Then, after a discussion about aims and motivations of our approach (Section 3), in Section 4 we introduce the logic QBDTL and a DTL-style semantics, along with some examples. In Section 5 we define the natural deduction system N(QBDTL), providing some example derivations. In Section 6 and Section 7 we state and prove the Soundness Theorem and the Completeness Theorem (of N(QBDTL) with respect to the semantics), respectively. Section 8 is devoted to discussions about our ongoing and future works.

Quantum Computing in a Nutshell

The aim of this section is to expand on what we already discussed in the introduction and provide to the non-expert reader an overview of the basic notions of quantum computing, focusing on those that are relevant for this paper and our approach in general (in particular, the quantum meaning of unitary relations and the interpretation of propositional symbols, but also what future challenges lie ahead of us, such as the formalization of entanglement). Readers familiar with quantum computing are welcome to skip this section.

The most simple quantum system is a two-dimensional state space whose elements are called quantum bits or qubits for short. The qubit is thus the unit of quantum information. The most direct way to represent a quantum bit is as a unitary vector in the 2-dimensional Hilbert space 2 ({0, 1}), which is isomorphic to C 2 . We denote with |0 and |1 the elements of the computational basis of 2 ({0, 1}). The states |0 and |1 of a qubit correspond to the Boolean constants 0 and 1, which are the only possible values of a classical bit.

A qubit, however, can assume other values, different from |0 and |1 . In fact, every linear combination |ψ = α|0 + β|1 where α, β ∈ C and |α| 2 + |β| 2 = 1, represents a possible qubit state. These states are said to be superposed, and the two values α and β are called amplitudes. The amplitudes α and β univocally represent the qubit with respect to the computational basis. Given a qubit |ψ = α|0 + β|1 , we can thus also denote it by the vectorial notation (α β) , where denotes the transposition of the vector. In particular, the vectorial representation of the elements of the computational basis |0 and |1 is: (1 0) represents |0 and (0 1) represents |1 .

While we can determine the state of a classical bit, for a qubit we cannot establish with the same precision the values α and β: quantum mechanics says that a measurement of a qubit with state α|0 + β|1 has the effect of changing the state to |0 with probability |α| 2 and to |1 with probability |β| 2 . For example

, if |ψ = 1 √ 2 |0 + 1 √ 2 |1 , one can fairly observe 0 or 1 with the same probability | 1 √ 2 | 2 = 1 2 .
Note, however, that in this brief survey on quantum computing, we will not enter into the details about the measurement/observation of the qubit(s), since in QBDTL we do not model agent evolution by measurement of quantum states; for a complete overview of measurement of qubits and the relationships between different kinds of measurement, see [START_REF] Nielsen | Quantum computation and quantum information[END_REF].

In order to define arbitrary sets of quantum data, we need a generalization of the notion of qubit, called quantum register or, more commonly, quantum state [START_REF] Selinger | A lambda calculus for quantum computation with classical control[END_REF][START_REF] Nishimura | Perfect computational equivalence between quantum turing machines and finitely generated uniform quantum circuit families[END_REF][START_REF] Lago | On a measurement-free quantum lambda calculus with classical control[END_REF]. A quantum register can be viewed as a system of n qubits and, mathematically, it is a normalized vector in the Hilbert space 2 ({0, 1} n ), where {0, 1} n is a compact notation to represent any binary sequence of length n. The standard computational basis for 2 ({0, 1} n ) is B = {|i | i is a binary string of length n}.

As notation, for b i ∈ {0, 1}, we write |b 1 . . . b k for |b 1 ⊗ . . . ⊗ |b k , where ⊗ is the tensor product (see below). With a little abuse of language, we say that the number of qubits n corresponds to the dimension of the space. Note that if the dimension is n, then the basis B contains 2 n elements, and each quantum state is a normalized linear combination of these elements:

α 1 |00 . . . 0 n + α 2 |00 . . . 1 + . . . + α 2 n |11 . . . 1 Example 1.
Let us consider a system of two qubits. Each 2-qubit quantum register is a normalized vector in 2 ({0, 1} 2 ) and the computational basis is {|00 , |01 , |10 , |11 }. For example, 1

√ 2 |00 + 1 √ 4 |01 + 1 √ 8 |10 + 1 √ 8 |11
is a quantum register of two qubits and we can represent it as ( 1

√ 2 1 √ 4 1 √ 8 1 √ 8 ) .
A Hilbert space of dimension n can be built from smaller Hilbert spaces by means of the tensor product ⊗. If H 1 is a Hilbert space of dimension k and H 2 is a Hilbert space of dimension m, then H 3 = H 1 ⊗ H 2 is a Hilbert space of dimension km (each element is a vector of km coordinates obtained by "hooking" a vector in H 2 to a vector in H 1 ). In other words, an n-qubit quantum register with n ≥ 2 can be viewed as a composite system and, in general, it is possible to combine two (or more) distinct physical systems into a composite one. If the first system is in the state |φ 1 (a vector in a Hilbert space H 1 ) and the second system is in the state |φ 2 (a vector in a Hilbert space H 2 ), then the state of the combined system is |φ 1 ⊗ |φ 2 (a vector in a Hilbert space H 1 ⊗ H 2 ). We will often omit the ⊗ symbol and write the joint state as |ψ 1 |ψ 2 or as |ψ 1 ψ 2 .

Not all quantum states can be viewed as composite systems: this case occurs in presence of entanglement phenomena (to which we return below). Since normalized vectors of quantum data represent physical systems, the (discrete) evolution of systems can be viewed as a suitable transformation on Hilbert spaces. The evolution of a quantum register is linear and unitary. Giving an initial state |ψ 1 , for each evolution to a state |ψ 2 , there exists a unitary operator U such that |ψ 2 = U(|ψ 1 ). Informally, "unitary" referred to an algebraic operator on a suitable space means that the normalization constraint of the amplitudes ( i |α i | 2 = 1) is preserved during the transformation. Thus, a quantum physical system can be described in terms of linear operators and in a deterministic way.

In quantum computing, we refer to a unitary operator U acting on a n-qubit quantum register as an n-qubit quantum gate. One can represent operators on the 2 ndimensional Hilbert space 2 ({0, 1} n ) with respect to the standard basis of C 2 n also as 2 n × 2 n matrices, and it is possible to prove that to each unitary operator on a Hilbert space we can associate unequivocally an algebraic representation. Matrices that represent unitary operators enjoy some important properties: for example, they are easily invertible (invertibility, also called reversibility, is one of the peculiar features of quantum computing). The application of quantum gates to quantum registers thus represents the pure quantum computational step and captures the internal evolution of quantum systems.

From a computer science viewpoint, it is common to reason about quantum state transformations in terms of quantum circuits (see, e.g., [START_REF] Nielsen | Quantum computation and quantum information[END_REF][START_REF] Nakahara | Quantum Computing -From Linear Algebra to Physical Realizations[END_REF]). We have introduced qubits to store quantum information, in analogy with the classical case. We have also introduced operations acting on them, i.e., quantum gates, and we can think about quantum gates in analogy with gates in classical logic circuits. A quantum circuit on n qubits implements a unitary operator on a Hilbert space of dimension C 2 n as a primitive collection of quantum gates, each implementing a unitary operator on k (small) qubits. It is useful to represent quantum circuits graphically in terms of sequential and parallel composition of quantum gates and wires, as for Boolean circuits (still, in the quantum case, the graphical representation does not reflect the physical realization of the circuit).

The most simple quantum gates act on a single qubit: they are operators on the space 2 ({0, 1}), represented in C 2 by 2 × 2 complex matrices. For example, the quantum gate X is the unitary operator that represents the quantum counterpart of the complementation gate. Being a linear operator, X maps a linear combination of inputs to the corresponding linear combination of outputs, i.e., X maps the general qubit state α|0 + β|1 into the state α|1 + β|0 .

Another fundamental unitary gate is the Hadamard gate H, which acts on the computational basis in the following way:

|0 → 1 √ 2 (|0 + |1 ) and |1 → 1 √ 2 (|0 -|1 ).
The Hadamard gate is useful when we want to create a superposition starting from a classical state. It also holds that H(H(|c )) = |c for c = {0, 1}.

1-qubit quantum gates can be used to build gates acting on n-qubit quantum states. If we have a 2-qubit quantum system, we can apply a 1-qubit quantum gate only to one component of the system, and we implicitly apply the identity operator (the identity matrix) I to the other one. For example, suppose we want to apply X to the first qubit. The 2-qubits input

|ψ 1 ⊗ |ψ 2 gets mapped to X|ψ 1 ⊗ I|ψ 2 = (X ⊗ I)|ψ 1 ⊗ |ψ 2 .
The controlled-not (cnot) is one of the most important quantum operators, usually represented graphically in the following way:

i • j
Intuitively, it takes two distinct quantum bits i and j as input and complements the target bit (the second one, j) if the control bit (the first one, i) is different from 0, and does not perform any action otherwise. Hence, its behavior on the computational basis is:

cnot|00 = |00 cnot|10 = |11 cnot|01 = |01 cnot|11 = |10
We can of course apply the cnot to superpositional states. For instance, if we apply cnot to the outcome of Hadamard gates applied to combinations of basis states |0 and |1 , i.e. i H • j H then we have:

cnot(H(|0 ), H(|0 )) = 1 2 (|00 + |01 + |10 + |11 ) cnot(H(|0 ), H(|1 )) = 1 2 (|00 -|01 -|10 + |11 ) cnot(H(|1 ), H(|0 )) = 1 2 (|00 + |01 -|11 -|10 ) cnot(H(|1 ), H(|1 )) = 1 2 (|00 -|01 -|11 + |10 )
Note that the control qubit is a "master" agent as its evolution is independent of the evolution of the target bit (if the first input of the cnot is |φ , then the output is the same), whereas the target qubit is a "slave" agent as its evolution is controlled by the value of the first qubit. In some sense, a communication between the agents is required and the quantum circuit is a simple distributed system. By adopting this perspective, controlled operators like cnot act as "synchronization points" between agents, and this is indeed one of the main ideas we followed during the development of QBDTL.

Not all quantum states can be viewed as composite systems. In other words, if |ψ is a state of a tensor product space H 1 ⊗ H 2 , it is not generally true that there exist |ψ 1 ∈ H 1 and |ψ 2 ∈ H 2 such that |ψ = |ψ 1 ⊗ |ψ 2 . In general, it is not always possible to decompose an n-qubit register as the tensorial product of n qubits. These non-decomposable registers are called entangled and enjoy properties that we cannot find in any object of classical physics (and therefore in classical data). If n qubits are entangled, they behave as if connected, independently of the real physical distance. The strength of quantum computation is essentially based on the existence of entangled states (see, for example, the teleportation protocol [START_REF] Nielsen | Quantum computation and quantum information[END_REF]).

Example 2. The 2-qubit states

|ψ 1 = 1 √ 2 |00 + 1 √ 2 |11 and |ψ 2 = 1 √ 2 |01 + 1 √ 2 |10
are entangled. The 2-qubit state |φ = α|00 + β|01 is not entangled; rather, note that it is possible to rewrite it in the mathematically equivalent form |φ = |0 ⊗ (α|0 + β|1 ).

A simple way to create an entangled state is to feed a cnot gate with a target qubit |c and a particular control qubit, more precisely the output of the Hadamard gate applied to a base qubit, therefore a superposition 1

√ 2 |0 + 1 √ 2 |1 or 1 √ 2 |0 -1 √ 2 |1 . If, instead,
we fed a cnot gate with two fair superpositional states (as above), that would not create an entangled state.

As we remarked above, in this paper we assume that no entanglement phenomena occur during the computation. Still, we have discussed entanglement here as it is a fundamental feature of quantum states and it has been one of the motivations for our approach in the first place. We believe that QBDTL will provide a suitable logic to formalize entanglement and we plan to explicitly model it in the future developments of our work (see also the discussion in Section 8).

Why Branching Temporal Logic and Synchronization?

In this section, we describe how it is possible to use temporal logic and synchronization rules (the core of the DTL approach) to reason in a simple way about quantum state transformations, whenever one is not interested in the encoding of the mathematical object that represents a quantum state (i.e., a vector in a suitable Hilbert space) but in the evolution itself as a sequence of transformations and in a notion of synchronization between different quantum bits.

Modal logics are a flexible instrument to describe qualitatively state transformations as they allow one to put the emphasis on the underlying "transition system" (the set of possible worlds of the Kripke semantics and the properties of the accessibility relations between them, which model the dynamical behavior of the system) rather than on the concrete meaning of the internal structures of possible worlds. This intuition was followed in [START_REF] Masini | A qualitative modal representation of quantum state transformations[END_REF][START_REF] Masini | Modal Deduction Systems for Quantum State Transformations[END_REF], where two pure modal systems were introduced and studied. In such systems, a world represents the abstraction of a quantum state and modal operators reflect general properties of quantum state transformations, since the subtended models are S5-models. The accessibility relation between worlds is therefore an equivalence relation, i.e., it enjoys reflexivity, symmetry and transitivity. This captures, in an abstract way, key properties of unary quantum operators: roughly speaking, reflexivity says that the class of the unitary operators includes the identity transformation; symmetry captures reversibility (it is always possible to reverse a quantum transformation, since the inverse operator is easily definable and is unitary); finally, transitivity models algebraic compositionality, i.e., the composition of two or more unitary operators is always a unitary operator [START_REF] Nielsen | Quantum computation and quantum information[END_REF].

The main difference between the modal systems proposed in [START_REF] Masini | A qualitative modal representation of quantum state transformations[END_REF][START_REF] Masini | Modal Deduction Systems for Quantum State Transformations[END_REF] and QBDTL is that whereas in the former case a world represents the abstraction of an arbitrary quantum state (i.e., a state that describes an arbitrary number n of qubits), in the case of QBDTL we focus on the single qubit and on its transformation by means of unary quantum operators and on a notion of local formula built upon a local language. Moreover, we move from a modal to a temporal system: in some sense we "unfold" the accessibility relation between worlds obtaining, for each agent, a tree-like structure that represents the agent's local life-cycle. In this way, we "link" the subtended branching temporal model to the abstract transition system induced by all the unary quantum transformations possibly occurring in each world, which are uniformly modeled in the semantics and in the deduction system by an equivalence relation. Reflexivity, symmetry and transitivity can be plainly expressed in QBDTL: for example, symmetry can be abstractly captured by the labeled formula (i, x, q) : p ⊃ ∃ ∃ p, where p is a propositional symbol, ⊃ is implication and ∃ A expresses that the formula A is true at the next time instant in some possible future.

A licit question at this stage is what is the meaning of the set of propositional symbols that QBDTL formulas are built upon. We maintain an abstract definition of the set (we simply say that it is a set of syntactic objects), following the style of DTL and also in the spirit of modal/temporal logic as we discussed above. Then, working with labeled expressions like (i, x, q) : A, where the formula A is built by temporal operators, synchronization and propositional symbols, it is not actually crucial to say what propositional symbols stand for. 2 Still, it is important to consider what modal/temporal formulas, possible worlds and the accessibility relation stand for.

One could even choose to instantiate the set of propositional symbols to capture quantitative information about quantum states or general properties that permit one to reason about them. Let us provide here a simple example, related to the examples that we will give later. A possible choice (cf. Example 3) is to fix a set of atomic propositions representing mathematical descriptions of the qubit, i.e., a normalized vector in C 2 . In other words, given a qubit |ψ = α|0 + β|1 , the encoding |ψ of this mathematical description is an atomic proposition. Let s i stand for a label (i, x, q), take p as |ψ and consider the labeled formula s i : p ⊃ ∃ p (whose derivation will be given in Figure 5 and where ∃ p expresses that p is true at every time instant in some possible future). This labeled formula can be intuitively interpreted as follows: a (potentially infinite) sequence of identity unitary transformations does not change the mathematical description of the qubit. Now, let p still be the encoding |ψ of a state |ψ = α|0 + β|1 and let us consider again the labeled formula (i, x, q) : p ⊃ ∃ ∃ p, which fits a peculiar feature of quantum computation, i.e., reversibility. This labeled formula says that: if p holds for i in some state x, then there exists a temporal path such that, in two steps, i reaches a new state in which p still holds (i.e., the mathematical description of such a state is again α|0 + β|1 ). This models the fact that if one transforms a qubit state by means of a unitary operator U, then one can obtain again the same state by applying the adjoint U * of U, where, in the class of unitary operators, the adjoint corresponds to the inverse U -1 , and algebraically, one has U * (U(α|0 + β|1 )) = U(U * (α|0 + β|1 )) = α|0 + β|1 , i.e., U * U = UU * = I, where I is the identity operator. Looking for a concrete example, we can take α = 1

√ 3 and β = √ 2 √
3 and instantiate U to X, the complementation gate, which corresponds to an exchange between amplitudes of basis states. Among the temporal states reachable from x there exists, in particular, the successor state in which p and ∃ p hold, where p =

√ 2 √ 3 |0 + 1 √ 3 |1
. We will provide further examples in the following sections.

We conclude this section by recalling that in quantum computing, it is useful to compose small states in order to obtain bigger quantum states (this operation has a precise algebraic meaning, see the previous section and [START_REF] Nielsen | Quantum computation and quantum information[END_REF]). Collecting agents, one can model quantum systems of n qubits. In some sense, we can see a quantum state of n qubits as a global state built upon the local states of the single qubits. Each qubit evolves independently but, in a realistic perspective, different qubits do not always evolve asynchronously, and so sometimes they interact, by means of n-ary quantum gates. This is modeled, in our system, by means of ad hoc "tools", properly adapted from DTL: by a special construct in the local language (an operator c named calling), it is possible to express the fact that an agent/qubit i synchronizes with another agent/qubit j. This choice has a precise quantum meaning. In quantum computing, one can, of course, globally modify a set of n qubits by means of n-ary algebraic operators. We view n-ary quantum gates as synchronization points between states of different lifecycles, i.e., between states of different qubits. The inputs of an n-ary quantum gate may each have previously been subject to a sequence of other transformations, i.e., in DTL terms, a sequence of events, and the gate itself then can be seen as a transformation event that is shared by the inputs. In this paper, we model this synchronization mechanism abstractly (since, as we said, we model unitary transformations by an equivalence relation), but it is possible to plan a concrete research direction based on the further development of this interpretation of n-ary gates as synchronization mechanisms. We will return to this in Section 8, where we give a more detailed discussion of our ongoing and future works.

The logic QBDTL

We introduce the Quantum Branching Distributed Temporal Logic QBDTL by presenting its syntax and semantics. As we mentioned above, QBDTL is a significant variant of DTL, with which it shares, of course, a number of similarities, but with respect to which it also sports several differences. For instance, we do not consider the sets of actions of the agents and, most importantly, in order to reason about quantum state transformations, QBDTL considers branching time as opposed to the linear time typical of DTL.

L i ::= p | ⊥ | L i ⊃ L i | ∃ L i | ∃ L i | ∀ L i | c j L j ,
where p ∈ Prop and j ∈ Id with i j.

Local formulas, as their names suggest, hold locally for the different agents. ⊥ is falsum and ⊃ is implication. As in DTL, the formula c j A means that agent i has just communicated (i.e., synchronized) with agent j, for whom A holds. We follow here the Peircean branching temporal logic UB [START_REF] Ben-Ari | The temporal logic of branching time[END_REF] and only consider the temporal operators that are obtained as a combination of one single linear-time operator immediately preceded by one single path quantifier. More specifically, we consider here the Peircean operators

• ∃ (as we noted previously, ∃ A expresses that the formula A in the scope of this operator is true at the next time instant in some possible future),

• ∃ ("it is true at every time instant in some possible future") and

• ∀ ("it is true at every time instant in every possible future").

For simplicity, in this work we do not consider the temporal operator until, although such an extension would not be problematic. Moreover, as usual, other connectives and temporal operators can be defined as abbreviations and will sometimes be explicitly used in the following.

Definition 2. The global language of QBDTL is defined by the grammar

L ::= @ i 1 L i 1 | . . . | @ i n L i n ,
where i 1 , . . . , i n ∈ Id.

The global formula @ i k A means that A holds for agent i k .

Semantics

The models of QBDTL are inspired by those of DTL and built upon a form of Winskel's event structures (cf. [START_REF] Winskel | Event structures[END_REF], where also the relationship to other concurrency models is discussed). There is, however, a fundamental difference with respect to the semantics that has (actually, with respect to the slightly different semantics that in the literature have) been given for DTL, which is based on distributed families of linear life-cycles local to each agent, i.e., countable, discrete and totally ordered local events. Since our logic QBDTL is inherently branching, we need to define its semantics accordingly, and we thus modify DTL's semantics as follows.

Definition 3. Given an agent i ∈ Id, a branching local life-cycle of i is an ω-tree, i.e., a pair λ i = Ev i , < i , where Ev i is the set of local events of i and < i ⊆ Ev i × Ev i is a binary relation such that: (i) < i is transitive and irreflexive;

(ii) for each e ∈ Ev i , the set {e ∈ Ev i | e < i e} is linearly ordered by < i ; (iii) there is a < i -smallest element 0 i called the root of λ i ; (iv) each maximal linearly < i -ordered subset of Ev i is order-isomorphic to the natural numbers.

We write e → i e to denote the fact that e is an immediate local successor of e, i.e., e < i e and there is no e such that e < i e < i e . A → i -path is a sequence of local events (e 0 , . . . , e n ) such that e k → i e k+1 for 0 ≤ k ≤ n -1. An e-branch b of i is an infinite → i -path b = (e 0 , e 1 , . . .) such that e = e 0 and we write → b i to denote the restriction of → i to b, i.e., e → b i e iff e = e k and e = e k+1 for some k, and denote with B i the set of all such → b i . Further, we denote with → b * i the reflexive and transitive closure of → b i . A local state is a finite set ξ ∈ Ev i down-closed for local causality, i.e., if e < i e and e ∈ ξ then also e ∈ ξ. In general, each non-empty local state ξ is reached by the occurrence of an event that we call last(ξ), from the local state ξ \ {last(ξ)}. Given e ∈ Ev i , the set e↓i = {e ∈ Ev i | e ≤ i e}, where ≤ i denotes the reflexive closure of < i , is always a local state. Moreover, if ξ is non-empty, then last(ξ)↓i = ξ.

A branching distributed life-cycle is a family of local life-cycles

λ = {λ i = Ev i , < i } i∈Id
such that:

(i) ≤ = ( i∈Id ≤ i ) *
defines a partial order of global causality on the set of events Ev = i∈Id Ev i ; (ii) if e, e ∈ Ev i and e ≤ e then e ≤ i e .

Condition (i) ensures that a distributed life-cycle respects global compatibility, i.e., there is no e ∈ Ev i ∩ Ev j such that e < i e but e < j e, while condition (ii) ensures that synchronization ≤-relates two events of an agent i only if there exists a 0 i -branch in which both the events occur. Definition 4. An S5 Kripke frame is a pair Q, U , where Q is a non-empty set of qubit states and U is a binary equivalence relation on Q, i.e., U : Q → Q is reflexive, symmetric and transitive.

An S5 Kripke model is a triple M = Q, U, V , where Q, U is an S5 Kripke frame and V : Q → P(Prop) is a valuation function assigning to each qubit state in Q a set of atomic propositions.

A QBDTL model is a triple µ = λ, M, π , where λ = {λ i } i∈Id is a distributed lifecycle, M = Q, U, V is an S5 Kripke model and π = {π i } i∈Id is a family of local functions associating to each local state a qubit state in Q; for each i ∈ Id and set Ξ i of local states of i, the function

π i : Ξ i → Q is such that: (i) if ξ, ξ ∈ Ξ i , last(ξ) → i last(ξ ), π(ξ) = q
and π(ξ ) = q , then qUq ; (ii) if q, q ∈ Q, qUq and π(ξ) = q, then there exists ξ ∈ Ξ i such that last(ξ) → i last(ξ ) and π(ξ ) = q .

We denote λ i , M, π i by µ i . The global satisfaction relation is defined by:

| = µ @ i A iff | = µ i i A iff | = µ i ,ξ i A for every ξ ∈ Ξ i ,
where the local satisfaction relation at a local state ξ of i is defined by:

| = µ i ,ξ i ⊥ | = µ i ,ξ i p iff p ∈ V(π i (ξ)), for p ∈ Prop | = µ i ,ξ i A ⊃ B iff | = µ i ,ξ i A implies | = µ i ,ξ i B | = µ i ,ξ i ∀ A iff for all ξ , last(ξ) ≤ i last(ξ ) implies | = µ i ,ξ i A | = µ i ,ξ i ∃ A iff there exists a last(ξ)-branch b such that for all ξ , last(ξ) → b * i last(ξ ) implies | = µ i ,ξ i A | = µ i ,ξ i ∃ A iff there exists ξ such that last(ξ) → i last(ξ ) and | = µ i ,ξ i A | = µ i ,ξ i c j A iff last(ξ) ∈ Ev j and | = µ j ,last(ξ)↓ j j A
By extension, we define:

| = µ Γ iff | = µ A for all A ∈ Γ Γ | = µ A iff | = µ Γ implies | = µ A Γ | = A iff Γ | = µ A for each QBDTL model µ 4.
3. An example of QBDTL "in action" Now that we have introduced the syntax and semantics of QBDTL, we can give a first example of QBDTL in action, i.e., how it can be used to formalize reasoning about quantum computations in a qualitative way. As pointed out in [START_REF] Basin | Distributed Temporal Logic for the Analysis of Security Protocol Models[END_REF], one of the main features of distributed temporal logics is their versatility: their abstract and parametric formulation permits a number of heterogeneous "specializations" to capture different agent-oriented systems and applications. As a first concrete example, we follow the ideas sketched in Section 3 and propose a concrete instance of the set Prop of propositional symbols in order to provide a description of the behavior of a simple quantum circuit.

We begin by introducing some notation and assumptions about quantum computations that our examples in this paper rely on. We focus on a universal class of quantum gates: we take into consideration all the unary gates plus the cnot. We call G this class of unitary operators. Given an instance C of the cnot gate, we write C i to denote the restriction of the "action" (in terms of transformations) of C on the qubit i. Note that we are not affirming that the transformations of the two agents (by means of the cnot) are independent of each other (indeed, this would negate the definition of the cnot, at least from the point of view of the target qubit). Rather, we are only observing that, after the control, two distinct unary transformations occur: the identity transformation leaves unchanged the control agent, whereas, the induced operation (eventually) complements the target agent. Following this perspective and assuming (as we do in this paper) that no entanglement phenomena occur, we can then "factorize" global transformations into local transformations and, as a consequence, we can plainly reason about global events in terms of local events of the local life-cycles of the agents.

Example 3 (QBDTL "in action" -I). The first step of any concrete example aiming at showing QBDTL in action is to fix the set Prop. Let us consider the standard algebraic axiomatization of quantum mechanics and the Hilbert space formalism [START_REF] Roman | Advanced linear algebra[END_REF]. As we remarked above, the mathematical state of a single qubit is represented by an element (a normalized vector) of C 2 , the 1-dimensional complex space. Let us call Q the set of all the normalized vectors in C 2 . We assume that each propositional symbol p ∈ Prop is the encoding of a normalized vector in Q: given |φ ∈ Q, we write |φ to denote its encoding into the QBDTL syntax. More formally, for this example, we can define the set Prop of propositional symbols to contain:

• the set of strings of the shape α 1 |0 + α 2 |1 , where α 1 |0 + α 2 |1 is the representation of an element of Q with respect to the standard computational basis, and

• the set of string of the shape U 1 (U 2 (• • • (U n (α 1 |0 + α 2 |1 )) • • •))
, where each U j is either a unary unitary transformation or the restriction of a cnot operator and α 1 |0 + α 2 |1 is defined as above.

Note that, as discussed in [START_REF] Masini | Modal Deduction Systems for Quantum State Transformations[END_REF], different propositional symbols can describe equivalent quantum states. For example, H(|0 ) (where H is the Hadamard gate) and 1 2 (|0 + |1 ) represent the same quantum state. For simplicity, but without loss of generality, in this paper whenever we consider one propositional symbol we actually take it as representative for its equivalence class. Extending our logic to explicitly consider these equivalences would be quite straightforward but fairly tedious and notationally cumbersome.

Note also that, as we remarked above, our central idea is to see event sharing as synchronization points between different agent life cycles, i.e., as controlled gate occurrences. We thus use the operator c to syntactically model synchronization/control. This interpretation has an evidence both in QDTL derivations and at the semantical level. In particular, we will get the evidence that: if no non-unary gate occurs in a computation involving different agents, no synchronizations (and, syntactically, no calling operator c k ) happen.

The simplest quantum circuit (generated by G) acting on two agents is the one built upon a single occurrence of the cnot gate. Consider the following figure

C i t 1 • t 2 j _ _ _ _
and suppose that C is an instance of the cnot gate, and that the control input i and the target input j are set to |1 and |0 , respectively. By definition, the negation of the target qubit is performed. For the sake of illustration, but of course with a slight abuse of notation, the figure shows also two time instants t 1 and t 2 . This allows us to consider a significative set of formulas that are built from the propositional symbols |1 and |0 , and that describe the behavior of C on inputs |1 and |0 during their temporal evolution. at time t 1 : @ i ( |1 ) and @ j ( |0 )

at time t 1 :

@ i ( |1 ∧ ∃ |1 ) (2)
at time t 1 : @ j (( |0 ∧ c i ( |1 )) ⊃ ∃ |1 ) ( 3
)
at time t 2 : @ i ( |1 ) and @ j ( |1 ) (4)
The intuitive meaning of these formulas is as follows. Formulas ( 1) and ( 4) describe the input and output states, respectively. Formula (2) says that the first agent (corresponding in our interpretation to the control qubit) has input value |0 and moreover there exists a successor (temporal) state (along the branch belonging to the computation captured by the circuit among all the possible computations) in which the state remains unchanged (remember that the cnot operator does not act on the control qubit). Formula (3) describes the control/synchronization between agents, corresponding to the occurrence of the binary gate; it is syntactically significative to model synchronization from the target agent's perspective, i.e., by means of a formula of the local language L j where, by means of the calling operator, we can express the mathematical state of the control agent through the suitable propositional symbols). In other words, the formula expresses the fact that a control (a QBDTL calling) and the related operation occur as a consequence of agent synchronization.

In Examples 4 and 5, we will continue this discussion and, moreover, consider a more complex quantum circuit, explaining also how the semantical notions introduced above can be concretely interpreted in quantum computation modeling.

A deduction system for QBDTL

Syntax of the labeled logic

In order to formalize our labeled natural deduction system N(QBDTL), we extend the syntax and semantics of QBDTL by introducing four kinds of labels (that represent agents, states, quantum information and paths in the underlying semantics) and by defining labeled and relational formulas.

First of all, we use the agent identifiers in Id as labels. Further, we assume given two fixed denumerable sets of labels Lab S and Lab Q . Intuitively, the labels x, y, z, . . . in Lab S refer to local states of an agent, whereas the labels q, q , q 1 , . . . in Lab Q refer to the quantum information concerning an agent. Definition 5. A labeled formula is a formula of the form (i, x, q) : A , where (i, x, q) is a composed label with i ∈ Id, x ∈ Lab S and q ∈ Lab Q , and A is a formula in the local language L i of the agent i.

Note that we do not use the operator @ inside labeled formulas as it is implicitly expressed by the first element of the composed label. For instance, in order to show that a global formula @ i A is valid, we will prove that the labeled formula (i, x, q) : A, for arbitrary x and q, is derivable in our system.

In N(QBDTL), we also need formulas modeling the relation between the states referred by the labels. We thus assume given a further set of labels Lab B , whose elements will be denoted by , 1 , 2 , . . ., which intuitively refer to the successor relation between local states in the local life-cycle of an agent i along a given branch. We then define:

Definition 6. Lab + B = Lab B ∪ {r(i, x, A) | i ∈ Id, x ∈ Lab S , ∈ { , }, A ∈ L i }.
The labels in Lab + B \ Lab B are used to refer to successor relations between local states along distinct branches. For instance, the label r(i, x, A) is used to denote a particular branch, in the local life-cycle of i, which starts in the node denoted by x and along which A always holds (provided that such a branch exists). We write R, R 1 , R 2 , . . . to denote generic elements of Lab + B and we use R * to refer to the reflexive and transitive closure of R. Finally, we use the symbol U to refer to the relation modeling unary quantum transformations and the symbol to denote that the local states of two agents are synchronized on a given event. Then, we can define relational formulas as follows: Definition 7. A relational formula is a formula of the form • (i, x, q) R (i, y, q ), or • (i, x, q) R * (i, y, q ), or • (i, x, q) ( j, y, q ), or

• q U q , where i, j ∈ Id, x, y ∈ Lab S , R ∈ Lab + B , q, q ∈ Lab Q . In the following, for simplicity, we sometimes use metavariables of the form s i , possibly superscripted, to refer to composed labels of the form (i, x, q). Example 4 (QBDTL "in action" -II). To illustrate further the power of QBDTL to formalize quantum computations, we consider a more complex quantum circuit Circ

C i t 1 V t 2 • t 3 t 4 j W _ _ _ _
where V and W are quantum gates and C is a cnot. We can interpret Circ as a finite set of paths belonging to a distributed life-cycle for agents i and j; in some sense, Circ can be viewed as a sub-computation of a (potentially) infinite quantum computation involving i and j. Recall, from Definition 3, the notion of e-branch b of an agent i. We write → ↓Circ i to denote the finite restriction of the particular e-branch corresponding to the transformation occurring to i by means of the computation Circ. We write Ev ↓Circ i to denote the (possibly finite) set of events "concerning" the Circ computation. In other words, we focus on the dynamical evolution of the qubit i by means of the transformations corresponding to the quantum gates of Circ. To this end, we interpret each local event either as a pair input, gate where input ∈ C 2 and gate ∈ G, or as an input value (i.e., the quantum state of the agents before the circuit evaluation) that we call |φ in . Note that, in the former case, we describe the outcome of a gate (the current state) by the pair input, gate , whereas in the latter we are fixing the circuit's input value.

Suppose now that, at the time t 1 , the agents i and j are in the states |c and |d (for c, d ∈ {0, 1}), respectively. We can describe the "progress" of the two agents in terms of increasing sets of collected events (which "keeps track" of the subcomputation occurred up to the current time) as follows. For i, we have

∅ → {|c in } → {|c in , |c in , V } → {|c in , |c in , V , V(|c in ), C i }...
and for agent j, we have

∅ → {|d in }) → {|d in , |d in , C j } → {|d in , |d in , C j , C j (|d in ), W }...
We can now consider the set of propositional symbols

{ |c , |d , V(|c ) , C i (V(|c )) , C j (|d ) , W(C j (|d )) }
to build the following labeled formulas to describe the circuit Circ: at time t 1 :

(i, x 1 , q 1 ) : |c and ( j, y 1 , q 1 ) : |d

at time t 1 : (i, x 1 , q 1 ) : |c ∧ ∃ V(|c ) (5)
at time t 2 : (i, x 2 , q 2 ) : V(|c ) ∧ ∃ V(|c ) (6)
at time t 2 : (i, x 2 , q 2 ) : V(|c ) ∧ ∃ [ c j ( d )] (7)
at time t 2 : ( j, y 2 , q 2 ) :

|d ∧ ∃ [ c i (V(|c ))] (9)
at time t 3 : (i, x 3 , q 3 ) : V(|c ) [START_REF] Birkhoff | The logic of quantum mechanics[END_REF] at time t 4 : (i, x 3 , q 3 ) : V(|c ) and ( j, y 3 , q 3 ) : W(C j (|d )) [START_REF] Caleiro | A labeled deduction system for the logic UB[END_REF] We describe the intuitive meaning of some of these formulas. Formulas ( 5) and ( 11) describe the input and output states, respectively. Formula (6) says that the first agent has input value |c (i.e., the propositional symbol |c holds) and moreover there exists a successor temporal state (along the branch belonging to the computation captured by the circuit among all the possible computations) in which V(|c ) holds. Formula [START_REF] Basin | Natural deduction for non-classical logics[END_REF] says that this successor temporal state has a successor in which V(|c ) still holds, i.e., the quantum state remains unchanged (remember that the cnot operator does not act on the control qubit). Formulas ( 8) and ( 9) say that for the agents i and j, for which V(|c ) and |d respectively hold, there exists a successor state in which a synchronization with the other agent occurs.

The sub-circuit corresponding to the cnot instance C can be described again in terms of synchronization (from the viewpoint of the target qubit/agent) as done in Example 3. By the definition of the cnot operator there are two cases. First, suppose that V(|c ) = |0 , which means that no complementation of the target qubit state occurs. Then, we have ( j, y 2 , q 2 ) : ( |d ∧ c i ( V(|c ))) ⊃ ∃ |d . Second, suppose that V(|c ) |0 (and remember that we are not dealing with entangled states). Then, we have ( j, y 2 , q 2 ) : ( |d ∧ c i ( V(|c ))) ⊃ ∃ |d , where |d denotes the complementation of the state |d .

Semantics of the labeled logic

In order to give a semantics for our labeled system, we need to define explicitly an interpretation of the labels. Definition 8. Given a QBDTL model µ, an interpretation function is a triple I = I S , I Q , I B , where:

• I S = {I i S } i∈Id is a set of functions such that I i S : Lab S → Ξ i for each i ∈ Id; • I Q : Lab Q → Q; • I B = {I i B }
i∈Id is a set of functions such that I i B : Lab + B → B i for each i ∈ Id, and if r(i, x, A) ∈ Lab + B \ Lab B , then:

-I i B (r(i, x, A)) =→ b i for some I i S (x)-branch b; -if | = µ,I i S (x) ∃ A, then for all ξ ∈ Ξ i : * if = , then last(I i S (x)) I i B (r(i, x, A)) last(ξ) implies | = µ,ξ A; * if = , then last(I i S (x)) I i B (r(i, x, A)) * last(ξ) implies | = µ,ξ A.
The notion of interpretation allows us to extend the truth relation to labeled formulas, as well as define truth of relational formulas. Definition 9. Given a QBDTL model µ and an interpretation function I = I S , I Q , I B on it, truth for a labeled or relational formula γ is defined as follows:

| = µ,I (i, x, q) : A iff µ i , I i S (x) | = i A and π i (I i S (x)) = I Q (q) | = µ,I (i, x, q) R (i, y, q ) iff last(I i S (x)) I i B (R) last(I i S (y)), π i (I i S (x)) = I Q (q) and π i (I i S (y)) = I Q (q ) | = µ,I (i, x, q) R * (i, y, q ) iff last(I i S (x)) I i B (R) * last(I i S (y)), π i (I i S (x)) = I Q (q) and π i (I i S (y)) = I Q (q ) | = µ,I (i, x, q) ( j, y, q ) iff last(I i S (x)) = last(I j S (y)), π i (I i S (x)) = I Q (q) and π j (I j S (y)) = I Q (q ) | = µ,I q U q iff I Q (q) U I Q (q )
When | = µ,I γ, for γ a labeled or relational formula, we say that γ is true in µ according to I. By extension:

| = µ,I Γ iff | = µ,I γ for all γ ∈ Γ Γ | = µ,I γ iff | = µ,I Γ implies | = µ,I γ | = µ γ iff
s i : B s i : A ⊃ B ⊃I s i : A ⊃ B s i : A s i : B ⊃E [s i * s i ] . . . . s i : A s i : ∀ A ∀ I s i : ∀ A s i R * s i s i : A ∀ E [s i R * s i ] . . . . s i : A s i Rs i s i : ∃ A ∃ I (i, x, q) : ∃ A (i, x, q) r(i, x, A) * s i s i : A ∃ E [s i Rs i ] . . . . s i : A s i Rs i s i : ∃ A ∃ I (i, x, q) : ∃ A (i, x, q) r(i, x, A) s i s i : A ∃ E [s j s j ] . . . . s i : A s i : A ser [( j, x, q) r( j, x, B) s j ] . . . . s i : A s i : A ser sk s j Rs j [s j R * s j ] . . . . s i : A s i : A base R s i s i s i s i s i : α s i : α lin s j Rs j [s j R * s j ] . . . . s i : A s i : A refl R s j R * s j s j R * s j [s j R * s j ] . . . . s i : A s i : A trans R s j R * 1 s j s j R * 2 s j [s j * s j ] . . . . s i : A s i : A comp R s j R * s j s j : B [s j : B] . . . . s i : A [s j Rs j ] [s j R * s j ] . . . . s i : A s i : A split R s i : A s i R * s i [s i * 1 s i ] [s i 2 s i ] [s i : A] . . . . s i : A s i : A ind∀ (i, x, q) : A (i, x, q) r(i, x, A) * s i
[(i, x, q) * (i, y, q )] [(i, y, q ) r(i, y, A) s i ] [(i, y, q ) : A] . . . .

s i : A s i : A ind∃
In ∀ I, ∃ I and ∃ I, where s i ≡ (i, x, q), the labels x and q are fresh. Moreover, in ∀ I, is fresh.

In ser , where s j ≡ ( j, x, q), the labels x, q and are fresh.

In ser sk , where s j ≡ ( j, y, q ), the labels y and q are fresh.

In comp R , is fresh. In ind∀, where s i ≡ (i, x, q) and s i ≡ (i, y, q ), the labels x, y, q, q , 1 and 2 are fresh.

In ind∃, where s i ≡ (i, z, q ), the labels y, z, q , q and are fresh.

s k : A s k : A c E s j s k [s k s j ] . . . . s i : A s i : A symm s j s k s k s l [s j s l ] . . . . s i : A s i : A trans s i s j 1 s j 1 Rs j 1 s j 1 R * s j 1 s j 1 s j 2 . . . s j n s i [s i s i ][s i * s i ] . . . . s k : A s k : A comp
In c I and c E, i j. In c E, where s j ≡ ( j, x, q), the labels x and q are fresh. In comp , is fresh. [q U q] . . . .

s i : A s i : A refl U q U q [q U q] . . . . s i : A s i : A symm U q U q q U q [q U q ] . . . . s i : A s i : A
trans U (i, x, q) : p γ( j, y, q) ( j, y, q) : p prop

In prop, γ( j, y, q) is a (labeled or relational) formula where ( j, y, q) occurs and p ∈ Prop is an atomic proposition.

The rules of N(QBDTL)

The rules of N(QBDTL) are given in Figures 1234. We can classify them into four categories: (i) local life-cycle rules (inspired to the deduction system for the logic UB given in [START_REF] Caleiro | A labeled deduction system for the logic UB[END_REF]), (ii) distributed life-cycle rules (reminiscent of the global labeled tableaux developed for DTL in [START_REF] Basin | Labelled tableaux for distributed temporal logic[END_REF]), (iii) quantum transformations rules (actually a fragment of the deduction systems studied in [START_REF] Masini | Modal Deduction Systems for Quantum State Transformations[END_REF]) and (iv) interaction rules. q U q γ(i, x, q) [(i, x, q) (i, y, q )] . . . . s j : A s j : A U⇒R (i, x, q) * (i, y, q )

[q U q ] . . . .

s j : A s j : A R⇒U
In U⇒R, γ(i, x, q) is a (labeled or relational) formula where (i, x, q) occurs. Moreover, y is fresh. Local life-cycle rules (Figure 1) These rules all infer formulas "local" to an agent i, i.e., labeled with s i . We can divide them further into rules for classical connectives (⊥ E, ⊃ I and ⊃ E), rules for temporal operators (∀ I, ∀ E, ∃ I, ∃ E, ∃ I and ∃ E), relational rules (ser , ser sk , base R , lin , refl R , trans R and comp R ) and induction rules (ind∀ and ind∃).

Rules for classical connectives. The rule ⊥E is a labeled version of reductio ad absurdum, where we do not enforce Prawitz's side condition that A ⊥ and we do not constrain the "world" in which we derive a contradiction to be the same as in the assumption. The rules ⊃ I and ⊃ E are the labeled version of the standard [START_REF] Prawitz | Natural Deduction: a Proof-Theoretical Study[END_REF] natural deduction rules for implication introduction and elimination.

Rules for temporal operators. The rules for the introduction and the elimination of ∀ , ∃ and ∃ follow the same structure as the rules for introduction and elimination of in labeled systems for modal logics. Let us consider ∀ I; the idea is that the meaning of s i : ∀ A is given by the metalevel implication s i * s i =⇒ s i : A for an arbitrary path denoted by the relation and an arbitrary s i * -accessible from s i . The arbitrariness, i.e., the freshness, of both the path denoted by and s i is ensured by the side-conditions of the rule, e.g., s i must be different from s i and not occur in any assumption on which s i : A depends other than the discharged assumption s i * s i . Introductions of ∃ and ∃ follow the same principle, but relax the freshness condition on the label denoting the relation, thus allowing us to reason on a single specific path. Note that in this case a further premise (s i Rs i ) is required: such a premise works as a "witness", in the sense that it ensures that the relation R considered is indeed a relation passing through the state s i .

For what concerns the elimination rules, the intuition behind ∀ E is that if ∀ A holds in a state s i and s i is accessible from s i (along some path), then it is possible to conclude that A holds in s i . The case of ∃ E and ∃ E is similar but complicated by the fact that the universal linear-time operator ( or ) is preceded by an existential path quantifier (∃), which prevents us from inferring the conclusion for a successor along an arbitrary relation. Our solution is based on the idea (originally proposed in [START_REF] Caleiro | A labeled deduction system for the logic UB[END_REF]) of using Skolem functions as names for particular relations, e.g., r(i, x, A) denotes a relation passing at x and such that if ∃ A holds in x, then A holds at each successor of x along r(x, A).

Relational rules. Relational rules allow for modeling properties of the accessibility relations. 3 The rule base R expresses the fact that for each relation R, R * contains R; i.e., base R says that if (i) s j is such that there is some R-accessible s j and (ii) from the assumption that s j is also R * -accessible from s j we can infer some labeled formula s i : A (where s i might be different from s j and s j ), then we can discharge the assumption s j R * s j and conclude that indeed s i : A holds. refl R and trans R model reflexivity and transitivity of each relation, respectively, whereas comp R states that it is possible to compose two relations, i.e., if s j R * 1 s j and s j R * 2 s j , then there exists a third relation * such that s j * s j . We also have two rules capturing two different aspects of the seriality of the relations. ser captures the fact that, given a state s j , there is at least a relation passing through s j and a successor along that relation. ser sk says that, given a state s j and a Skolem function r( j, x, B), there exists a successor of s j along that relation. Finally, split R states that if s i R * s i holds, then either s i and s i coincide or s i is a proper successor of s i .

Induction rules. Finally, we have two rules that model the induction principle underlying the relation between R and R * . This modeling of the induction principle is inspired to the one proposed in [START_REF] Caleiro | A labeled deduction system for the logic UB[END_REF] and it is reminiscent of deduction systems for Peano Arithmetic. An example of use of the rule ind∃ can be found in Figure 5, as we discuss below.

Distributed life-cycle rules (Figure 2)

The rules for communication ( c I and c E) follow quite closely the semantics. Consider, e.g., c I: if agent i in state s i synchronizes with agent j in state s j , and A holds for j in that state, then i just communicated with agent j. The rules for synchronization are also quite intuitive, except maybe comp . Intuitively, comp models a notion of compatibility between different synchronizations that involves the same agents and reflects condition (ii) in the definition of branching distributed life-cycle. It is a rule schema that can be applied for any finite n.

Quantum transformations rules (Figure 3)

The rules refl U , symm U , trans U formalize, quite straightforwardly, the reflexivity, symmetry and transitivity of the U relation, in order to uniformly model the class of algebraic unitary operators as an equivalence relation. This captures, in an abstract way, key properties of quantum operators. Roughly speaking: reflexivity says that the class of the unitary operators includes the identity transformation; symmetry captures reversibility (it is always possible to reverse a quantum transformation, since the inverse operator is easily definable and is unitary [START_REF] Nielsen | Quantum computation and quantum information[END_REF]); finally, transitivity models algebraic compositionality, i.e., the composition of two or more unitary operators is always a unitary operator.

The rule prop says that the third element in a composed label fully captures the quantum information contained in a state; thus, if two composed labels (i, x, q) and

[s i : p] 1 [s i r(i, x, p) * s a i ] 3 [q Uq ] 5 [(i, y, q ) : p] 4
[(i, y, q ) (i, z, q )] 6 [(i, y, q ) s d i ] 7

[(i, y, q ) : p] 4 [(i, y, q ) (i, z, q )] 6 (i, z, q ) : p prop

s d i : p lin [(i, y, q ) (i, z, q )] 6 (i, y, q ) : ∃ p ∃ I 7 (i, y, q ) : ∃ p U⇒R 6 (i, y, q ) : ∃ p refl 5 U [(i, y, q ) r(i, y, p)s c i ] 4 s c i : p ∃ E s a i : p ind∃ 4 [s i r(i, x, p)s b i ] 2 s i : ∃ p ∃ I 3 s i : ∃ p ser sk 2 s i : p ⊃ ∃ p ⊃I 1 [s i : c j ] 2 [s j : c i ] 5 [s i s j ] 3 [s j * s j ] 4 [s j s i ] 6 [s i : ∀ p] 1 [s i * 1 s i ] 7 s i : p ∀ E s i : p comp 7 [s j s i ] 6 s j : c i p c I s j : c i p c E 6 s j : c i ⊃ c i p ⊃I 5 s j : ∀ ( c i ⊃ c i p) ∀ I 4 [s i s j ] 3 s i : c j ∀ ( c i ⊃ c i p) c I s i : c j ∀ ( c i ⊃ c i p) c E 3 s i : c j ⊃ c j ∀ ( c i ⊃ c i p) ⊃I 2 s i : ∀ p ⊃ ( c j ⊃ c j ∀ ( c i ⊃ c i p)) ⊃I 1
Figure 5: Example derivations ( j, y, q) share the same q, each atomic proposition holding in (i, x, q) must also hold in ( j, y, q). Interaction rules (Figure 4)

The rules U⇒R and R⇒U model the interaction between U and R and express respectively the conditions (i) and (ii) in the definition of function π i of QBDTL models. More specifically, U⇒R says that if qUq and the label (i, x, q) occurs in the labeled or relational formula γ( j, x, q), then (i, x, q) has a -successor (i, y, q ); this means that the local state labeled by y is an immediate successor of the state labeled by x in local life-cycle of the agent i, along a given branch. The rule R⇒U captures the fact that if (i, y, q ) is a * -successor of (i, x, q) then also the quantum labels q and q have to be related by U.

Derivations

Given the rules in Figure 1234, the notions of derivation, conclusion, open and discharged assumption are the standard ones for natural deduction systems (see, e.g., [START_REF] Girard | Proof theory and logical complexity[END_REF], pp. 127-129).

Definition 10. We write Γ N(QBDTL) (i, x, q) : A to say that there exists a derivation of (i, x, q) : A in the system N(QBDTL) whose open assumptions are all contained in the set of (labeled and relational) formulas Γ. A derivation of (i, x, q) : A in N(QBDTL) where all the assumptions are discharged is a proof of (i, x, q) : A in N(QBDTL) and we then say that (i, x, q) : A is a theorem of N(QBDTL) and write N(QBDTL) (i, x, q) : A.

Figure 5 contains two examples of derivations (actually, proofs

). The first is based on the fact that it is always possible to apply the identity transformation to a qubit. It follows that if a qubit is in a state where an atomic proposition p holds, then there exists a path along which p always holds.

The formula derived in the second example describes a property of the synchronization between qubits and can be read as a consequence of condition (ii) in the definition of a distributed life-cycle. If the qubit i is in a state from which a proposition p always holds in the future, then if i synchronizes with j, i.e., the two qubits are combined by means of some n-ary quantum operator, and after that, j synchronizes with i again, we end up in a state of i where p still holds. Note that in this derivation we use the verum as an abbreviation for ⊥⊃⊥.

Example 5 (QBDTL "in action" -III). We now give a derivation that describes the circuit of Example 3. The aim of this example is to show that our interpretation of synchronizations as controlled operations is significative also at level of deduction. Let us consider the following formula, which describes the circuit's behavior from the perspective of agent j:

( j, x, q) : ∀ (( |0 ∧ c i |1 ) ⊃ ∃ ( |1 ∧ ( c i |1 ))) (12)
where we suppose that x is the starting temporal state that belongs to the path corresponding to the circuit. Intuitively, the antecedent and the consequent of the implication describe the input-output behavior of the circuit; the "action" of the controlled gate can be read as the sharing of a time instant by the agents involved in the calling. We need also to specify a further set of assumptions, in order to model the required input conditions. This will be explicitly done by the following labelled and relational formulas:

( j, x, q) * ( j, x 1 j , q 1 j ) ( 13
) ( j, x 1 j , q 1 j ) : |0 (14)
( j, x 1 j , q 1 j ) (i, x 1 i , q 1 i ) ( 15
) (i, x 1 i , q 1 i ) : |1 (16)
Informally, we are expressing the following notions: starting from the current state x, we focus on a state in the future [START_REF] Dalla Chiara | Quantum logic[END_REF] in which |0 holds for j [START_REF] Ehrich | Specifying communication in distributed information systems[END_REF]; moreover, at the same instant, j is synchronized with the agent i (15) and |1 holds for i [START_REF] Emerson | Decision procedures and expressiveness in the temporal logic of branching time[END_REF].

Starting from these assumptions, we are able to derive the labeled formula ( j, x, q) : ∃ |1 , which actually says that there exists a successor temporal state (among all the possible immediate successors) that corresponds to evaluation by means of cnot:

s j : ∀ (( |0 ∧ c i |1 ) ⊃ ∃ ( |1 ∧ ( c i |1 ))) s j * s 1 j s 1 j : ( |0 ∧ c i |1 ) ⊃ ∃ ( |1 ∧ ( c i |1 )) ∀ E s 1 j : |0 s 1 i : |1 s 1 j s 1 i s 1 j : c i |1 c I s 1 j : |0 ∧ c i |1 ∧I s 1 j : ∃ ( |1 ∧ c i |1 ) ⊃E [s 1 j r( j, x 1 j , A)s 2 j ] 2 s 2 j : |1 ∧ c i |1 ∃ E s 2 j : |1 ∧E [s 1 j r( j, x 1 j , A)s n j ] 1 s 1 j : ∃ |1 ∃ I 2 s 1 j : ∃ |1
ser sk

1
where s j ≡ ( j, x, q), s 1 j ≡ ( j, x 1 j , q 1 j ), s 2 j ≡ ( j, x 2 j , q 2 j ),

s 1 i ≡ (i, x 1 i , q 1 i ) and A ≡ ( |1 ∧ c i |1 ).
Note that it would not be possible to derive the conclusion s 1 j : ∃ |1 only by means of the assumptions describing the input conditions ( 13), ( 14), ( 15) and ( 16), i.e., without a further premise specifying the behavior of cnot.

This example suggests a possible use of QBDTL and of the associated deduction system. While some basic properties of quantum transformations, e.g., reversibility, are embodied in the logic, it is also possible to use the formalism provided by QBDTL in order to model the existence and the behavior of specific gates, as we did here in the case of cnot. By adding the representation of such gates as assumptions, a modeler is allowed to consider (and to use the deduction system to reason about) more specific scenarios.

Soundness

The system N(QBDTL) is sound with respect to the given semantics, as can be shown by adapting standard proof techniques for labeled natural deduction systems [START_REF] Basin | Natural deduction for non-classical logics[END_REF][START_REF] Viganò | Labelled Non-Classical Logics[END_REF].

Theorem 1 (Soundness). For every set Γ of labeled and relational formulas and every labeled formula (i, x, q) : A, it holds that Γ N(QBDTL) (i, x, q) : A ⇒ Γ | = (i, x, q) : A.

Proof. The proof proceeds by induction on the structure of the derivation of (i, x, q) : A. The base case is when (i, x, q) : A ∈ Γ and is trivial. There is one step case for every rule (where, for what concerns local life-cycle rules, we refer to [START_REF] Caleiro | A labeled deduction system for the logic UB[END_REF], whose treatment can be quite easily adapted to work here). We show a few representative step cases.

Consider the case when the last rule applied is prop:

Π 1 (i, x, q) : p Π 2 γ( j, y, q) ( j, y, q) : p prop where Π 1 is a proof of (i, x, q) : p from hypotheses in Γ 1 and Π 2 is a proof of γ( j, y, q) from hypotheses in Γ 2 , for some sets Γ 1 , Γ 2 of formulas. By the induction hypothesis, for each model µ = λ, M, π and interpretation function I, if | = µ,I Γ 1 then 7.1. A semantic tableau for QBDTL

Hintikka structures

We define a structure as a pair (S, S ), where S is a set of triples { S i , R i , P i } i∈Id specifying for each agent i a set S i of states, an assignment P i of formulas to states and a binary relation R i on S i , and S is a binary relation on {s ∈ S i | i ∈ Id}, used in the construction to connect states of distinct agents. We require that there exists a subset Prop of Prop such that each P i is complete with respect to Prop , i.e., for each atomic proposition p ∈ Prop and state s ∈ S i , either p ∈ P i (s) or ¬p ∈ P i (s), and such that all the formulas assigned to states by P i are built over atoms in Prop . Finally, we require that a structure respects the following conditions:

• for each i and s ∈ S i , there exists a t ∈ S i such that sR i t;

• there exists an S5 model M = Q, U, V , where V is defined from Q to P(Prop ), such that for each i and each s ∈ S i , a world q s ∈ Q is assigned to s, and this assignment is such that: (i) for each p ∈ Prop , p ∈ P i (s) iff p ∈ V(q s ), and (ii) sR i t iff q s Uq t .

We define R = i∈Id R i as the union of the R i and, for simplicity, given s ∈ S i , we will often write A ∈ s to denote A ∈ P i (s) and s ∈ S if s ∈ S i for some i.

As in [START_REF] Ben-Ari | The temporal logic of branching time[END_REF], we implicitly reduce possible double negations and replace negated modalities by their duals. We define α-formulas and β-formulas as the following local formulas:4

α α 1 α 2 A 1 ∧ A 2 A 1 A 2 ∀ A A ∀ ∀ A ∃ A A ∃ ∃ A β β 1 β 2 A 1 ∨ A 2 A 1 A 2 ∀ A A ∀ ∀ A ∃ A A ∃ ∃ A
Given a local formula A, let At(A) = {p 1 , . . . , p n } be the set of atomic propositions occurring in A (for simplicity, we can assume such a set to be ordered). We call an atomic configuration for A any formula of the form p1 ∧ . . . ∧ pn , where each pi is either p i or ¬p i . Let ∆ A = {B | B is an atomic configuration for A}. Then, we define

In A = ∀ ∃ ∧ (∀ B∈∆ A B) ∧ B∈∆ A (∃ B ⊃ ∀ (∃ B)) .
The formula In A will be used to ensure that: (first conjunct) the construction of a tableau for A gives rise to models where seriality is satisfied; (second conjunct) the set of atomic propositions in At(A) holding in each node is specified during the tableau construction; and (third conjunct) the assignments of atomic propositions to worlds is ruled by an underlying S5-model. We say that (S, S ) is a Hintikka structure for a global formula @ i A if (A ∧ In A ) ∈ s for some s ∈ S i .

Theorem 2. A global formula @ j A is satisfiable iff there is a Hintikka structure for @ j A.

Proof. (⇒) For each agent i, the branching distributed local life-cycle can be easily turned into a local structure S i , R i , P i and the sharing of events between agents can be used to define the relation S . For this direction, just observe that the conditions defining a Hintikka structure are less restrictive than those defining a QBDTL model.

(⇐) Let (S, S ), where S is a set of triples { S i , R i , P i } i∈Id , be a Hintikka structure. By definition, there is an associated S5 model M = Q, U, V defined over a subset Prop of the set Prop of atomic propositions. We can extend M by defining p ∈ V(q) for each q ∈ Q and for each p ∈ Prop \ Prop . Now we define a QBDTL model µ = λ, M, π , where λ = {λ i } i∈Id and each λ i is obtained by unwinding the corresponding local structure S i , R i , P i . π is simply defined by using the mapping between states in S and worlds in M. Finally, the sharing of events in λ is induced by the relation S . The proof that the model µ obtained is indeed a model for @ j A is quite standard and proceeds by induction on the length of the formula. The only new case is the one concerning communication formulas and is handled by using condition 8 of Definition 11.

Tableau construction

Here we will first describe a procedure for constructing a semantic tableau, and then show how to obtain a Hintikka structure from the tableau.

Given i, j ∈ Id with i j, an agent formula is a formula of the form i : A, where A is a formula in the local language of i; a communication formula is a formula of the form [i : A] j and a synchronization formula is a formula of the form i j. A tableau formula is an agent formula, a communication formula or a synchronization formula. We will sometimes refer to agent and communication formulas concerning an agent i as i-formulas.

The tableau consists of a set of nodes and oriented edges between nodes, where each node is labelled with a set of tableau formulas. Given a node n, we will denote by L n the set of formulas labeling n, and, for simplicity, often write ϕ ∈ n for ϕ ∈ L n . We say that an agent i occurs in n if at least one tableau formula labeled with i occurs in n. An agent i is blocked in n if there exists a synchronization formula [ j : A] i ∈ L n . We denote with Cl (n) the symmetric and transitive closure of the relation induced by the synchronization formulas in L n , e.g., if (i j), ( j k) ∈ L n , then (i k) ∈ Cl (n).

The tableau T for a global formula @ i A 0 is constructed inductively by labeling a root node n 0 with i : A 0 ∧ In A 0 and by applying the following rules to nodes n that are leaves of T :

• R α : if i : α ∈ L n , then create a son n 1 of n and define L n 1 = L n ∪ {i : α 1 , i : α 2 }; • R β : if i : β ∈ L n , then create two sons n 1 and n 2 of n and define L n l = L n ∪ {i : β l } for l ∈ {1, 2}; • R : if [i : ∃ A] j ∈ L n , then:
create a son n 1 of n and define L n 1 = L n ∪ {i : A, i j};

if (i j) Cl (L n ), then also create a second son n 2 of n and define

L n 2 = L n ∪ {[i : ∃ ∃ A] j }. • R c : if i : c j A ∈ L n ,
then create a son n 1 of n and define:

-L n 1 = L n ∪ { j : A ∧ In A 0 , i j} if j does not occur in n; -L n 1 = L n ∪ { j : A} if (i j) ∈ Cl (L n ); -L n 1 = L n ∪ {[ j : ∃ A] i } otherwise;
• R : this rule is applied only when applications of R α , R β and R c would not generate a new node. Let Γ i be the set of formulas in L n that do not involve i.

For each agent i occurring in n and not blocked, such that

V i = {i : ∃ A 1 , . . . , i : ∃ A k , [i : ∃ B 1 ] j 1 , . . . , [i : ∃ B h ] j h , i : ∀ C 1 , . . . , i : ∀ C m } is the set of i- nexttime formulas in L n , we create:
k sons n l of n, for 1 ≤ l ≤ k, and define L n l = {i : A l , i : C 1 , . . . , i : C m } ∪ Γ i ; and

h sons n l of n, for 1 ≤ l ≤ h, and define

L n l = {[i : B l ] j l , i : C 1 , . . . , i : C m } ∪ Γ i ;
we will refer to the k + h nodes created in this step as i-sons of n.

With respect to the construction in [START_REF] Ben-Ari | The temporal logic of branching time[END_REF], we note that here we need some further rules. R can be seen as a special case of R β , where the creation of a witness for the formula expressing an eventuality also adds to the node a synchronization formula stating that the two agents have just communicated. R c is a special case of R α that forces a communication to happen if the two agents are currently synchronized or postpones such a synchronization to some future node otherwise. Finally, we note that in our case R embodies also a β-step that represents the choice of the agent to be reactivated next.

We have two termination rules in the construction of a tableau:

2. Apply the ranking algorithm described below to the structure obtained and mark each node containing an unranked occurrence of a future formula. If the resulting structure is such that the rules in step 1 become applicable again, then go back to step 1.

Ranking algorithm

The application of step 1 in the marking algorithm given above generates a structure that does not necessarily satisfy conditions 6 and 7 of Definition 11. This is due to the fact that, in the presence of cycles, the creation of a witness for a future eventuality could be postponed indefinitely.

Here we define a ranking algorithm aimed at facing this issue. Let T be a tableau obtained by applying step 1 of the marking algorithm above and let N be the set of unmarked nodes in T . The following algorithm will assign a positive rank ρ(q, n) to some of the occurrences q of future formulas in n. Intuitively, ρ(q, n) represents the distance between n and the node where a witness for the future formula q occurs. Let q ∈ L n be a not ranked future formula. The ranking algorithm consists of the following rules:

• R 1 : If n is a β-node or a -node for q and n 1 ∈ N, then ρ(q, n) = 1;

• R 2 : If n is a β-node or a -node for q, q is the formula occurrence generated for the node n 2 and ρ(q , n 2 ) is defined, then ρ(q, n) = ρ(q, n 2 ) + 1;

• R 3 : If n is a β-node or a -node not for q and ρ(q, n k ) is defined for some k ∈ {1, 2}, then ρ(q, n) = ρ(q, n k ) + 1;

• R 4 : If n is an α-node or a c -node and ρ(q, n 1 ) is defined, then ρ(q, n) = ρ(q, n 1 ) + 1;

• R 5 : If n is a -node and q = i : ∀ ∀ A, then:

-if ρ(i : ∀ A, n k ) is defined for all i-sons n k of n, then ρ(q, n) = max{ρ(i : ∀ A, n k )} k + 1;
otherwise, if for some j occurring and not blocked in n, ρ(i : ∀ ∀ A, n k ) is defined for all j-sons n k of n, then ρ(q, n) = max{ρ(i :

∀ ∀ A, n k )} k + 1. • R 6 : If n is a -node and q = i : ∃ ∃ A/[i : ∃ ∃ A] j , then: -if ρ(i : ∃ A/[i : ∃ A] j , n k ) is defined for some i-son n k of n, then ρ(q, n) = ρ(i : ∃ A/[i : ∃ A] j , n k ) + 1;
otherwise, if for some agent h occurring and not blocked in n, ρ(i :

∃ ∃ A/[i : ∃ ∃ A] j , n k ) is defined for some h-son n k of n, then ρ(q, n) = ρ(i : ∃ ∃ A/[i : ∃ ∃ A] j , n k ) + 1.
The ranking algorithm terminates since the set of future formulas in N is finite and each formula is ranked at most once.

From tableaux to Hintikka structures

Here we show how a tableau constructed as described above for a satisfiable formula can be turned into a Hintikka structure. Theorem 3. Let T be a tableau for @ i A. If the root of T is not marked, then there exists a Hintikka structure for @ i A.

Proof. The proof of this theorem mirrors the one of the analogous theorem in [START_REF] Ben-Ari | The temporal logic of branching time[END_REF]; here we will just give a sketch of it and highlight some differences arising in our setting. Given a tableau for @ i A, a structure can be constructed as described in step 1 of the marking algorithm. Some care needs to be taken in order to deal with β-nodes. It may happen that, when unwinding a cycle of the tableau, some future formula is not fulfilled. This can be avoided by adopting a "fair" policy, which in the presence of a β-node alternates the choice between the two sons in such a way that if there is a branch containing an infinite number of occurrences of a β-node, then each of its sons occurs infinitely many times in the branch. Such a construction, the details of which can be found in [START_REF] Ben-Ari | The temporal logic of branching time[END_REF], guarantees that conditions 6 and 7 of Definition 11 are satisfied. Finally, we note that the formula In A , added as a conjunct to the root of the tableau, ensures that the valuation of atomic propositions meets the requirement of being determined by an underlying S5 model.

Completeness of N(QBDTL) via tableaux

Here we will first prove a result concerning the relation between the formulas contained in a marked node of a tableau, built according to the procedure described in Section 7.1, and the formulas derivable in N(QBDTL). Then we will use such a result in order to prove the weak completeness of N(QBDTL).

Given a tableau T and a node n of T , the N(QBDTL) translation L * n of L n is obtained from L n by replacing, for each agent i, each i-formula i : A or [i : A] j with the formula (i, x i , q i ) : A for some x i and q i . We say that a node n of T is inconsistent if

L * n N(QBDTL) ⊥. Lemma 2.
If n is a marked node of a tableau, then n is inconsistent.

Proof. The structure of this proof also follows quite closely the one given in [START_REF] Ben-Ari | The temporal logic of branching time[END_REF] with respect to a Hilbert-style axiomatization for the logic UB. Here we recall the general structure and add some remarks concerning our case. We notice that N(QBDTL) includes a subsystem that has been proved complete for UB [START_REF] Caleiro | A labeled deduction system for the logic UB[END_REF]; thus for what concerns branching-time reasoning in the proof, we can just rely on the fact that the axioms used in [START_REF] Ben-Ari | The temporal logic of branching time[END_REF] can be derived by using the rules of N(QBDTL).

The proof proceeds by showing that the marked leaves of the tableau are inconsistent nodes (this is trivial as a leaf must contain both A and ¬A for some A) and by proving that the property of being inconsistent is propagated at each step when one moves towards the root. In particular, this is easily shown for those nodes that are marked through the step 1 of the marking algorithm. We just notice, as a peculiarity of our setting, that in the case of a c -node n, if the son is generated by adding a formula of the form [ j : ∃ A] i , then for proving that n is inconsistent we need to refer to the node, possibly lower in the tableau than the son of n, where the synchronization between i and j actually occurs.

When nodes are marked through step 2 of the marking algorithm, a more complex construction is needed in order to show that there is a cycle that never fulfills an eventuality. This requires the definition of an invariant formula as a disjunction of the formulas characterizing each of the nodes in the cycle. In this case, inconsistency of the nodes is proved by using the induction rules ind∀ and ind∃.

Finally, we note that formulas of the form (i, x, q) : In A for any A are derivable in our system by using the rule ser for seriality, the quantum transformation rules refl U , symm U , trans U and prop, together with the interaction rules U⇒R and R⇒U. This is used for proving that the initial node is inconsistent as well as in the case of c -nodes that introduce new agents.

The following theorem states that the converse of Theorem 3 holds, thus establishing the fact that the tableau procedure given in Section 7.1 is a decision procedure for QBDTL. Theorem 4. Let @ i A be a satisfiable formula. Then the root n 0 of the tableau for @ i A is not marked.

Proof. Assume @ i A is satisfiable, i.e., @ i ¬A is not valid. By the soundness of N(QBDTL), it follows N(QBDTL) (i, x, q) : A, for arbitrary x and q. Then, by Lemma 2, the root of the tableau for @ i A is not marked.

Theorem 5 (Weak completeness). For every QBDTL formula A and composed label (i, x, q), if | = (i, x, q) : A, then N(QBDTL) (i, x, q) : A.

Proof. Let | = (i, x, q) : A. Then (i, x, q) : ¬A is unsatisfiable. By Theorems 2 and 3, the root of any tableau for @ i ¬A is marked. By Lemma 2, we conclude N(QBDTL) (i, x, q) : A.

Concluding Remarks

We have given the syntax and semantics of our Quantum Branching Distributed Temporal Logic QBDTL along with the deduction system N(QBDTL) and examples of its application. Moreover, we have proved that N(QBDTL) is sound and complete with respect to the given semantics. The proof of soundness is a standard induction, whereas the proof of the completeness theorem required a non-trivial refinement and extension of the complex proof, based on the definition of a tableau system, proposed in [START_REF] Ben-Ari | The temporal logic of branching time[END_REF] for the branching-time logic UB.

In this paper, we have modeled quantum state transformations from an abstract perspective: in QBDTL, no reference to a specific quantum computation or to a notion of input/output of values is required. This allowed us to design a manageable high-level formalization oriented to modeling the behavior of quantum systems, but it is probably not enough if one wants to capture more complex properties such as entanglement. This does not mean that one has to completely convert the qualitative approach into a quantitative one (following the "philosophy" of quantum logic, cf. the discussion in the introduction and the following sections). We believe that a distributed logic is a promising tool not only for the simple description of quantum states, but also to model the correct amount of quantitative information needed to capture properties like entanglement. In some sense, we aim at integrating into the QBDTL high-level perspective, able to model the "control" of quantum computation (which treats qubits and quantum gates as black-boxes), more detailed information about quantum data, so that it is possible to "look inside" the qubits and specifically model the quantitative behavior of some interesting unitary operators.

In QBDTL, we are as general as possible with respect to the application of transformations: in a local-life cycle the subtended temporal transition tree represents at each step all the possible unary gates that can be applied to the current state, while the synchronization mechanism between agents models all possible n-ary operators. It is well known that one can fix a complete computational basis (finite or infinite) of unitary operators and represent other operators in terms of the elements of such a basis. An infinite complete basis can be defined by taking all unary operators and the binary quantum gate cnot. As we remarked above, when the control qubit assumes some specific superpositional value (e.g., 1

√ 2 |0 + 1 √ 2 |1
), the output of the cnot is an entangled state. This suggests that restricting our perspective about arbitrary n-ary gates as synchronization operators to a single binary gate, the cnot, and lifting syntax and semantics to capture its behavior would provide us with all the ingredients needed to model entanglement. Following this standpoint, one can now view synchronizations exactly as control operators: a target qubit has to synchronize (by sharing an event) with the control qubit in order to perform its own, controlled evolution. Moreover, we observe that the notion of synchronization, in presence of entanglement, assumes a non-local (with respect to time) meaning: a synchronization that creates entanglement does not only represent the sharing of local events, but it also influences the subsequent events in the local life cycle of the involved agents. We thus aim to make the connection between agent synchronization and (possible) entanglement of qubits explicit.

More specifically, if an agent/qubit belongs to an entangled state, it is not possible to "keep out" its individual mathematical description, since the global mathematical description of an entangled state cannot be expressed in terms of local descriptions. Hence, in order to speak about entanglement, we need new syntactical constructs. A side effect is that also the interpretation of propositional symbols provided in Section 3 and in the examples has to be lifted in order to deal with the impossibility to express a local mathematical status. We are working at extending the logic with ad hoc propositional symbol of the shape entg i , which models exactly the information that the agent i is momentarily entangled and no local information about its quantum states can be provided. This is why we believe that this extension will have an interesting impact also on the notion of synchronization.

Finally, we are considering the explicit modeling inside QBDTL of measurement steps, which can be seen as a further class of transformations. We believe that these extensions will also enable the use of our approach for the analysis of quantum security protocols, which are based on entanglement phenomena [START_REF] Bennett | Quantum cryptography: Public key distribution and coin tossing[END_REF], along the lines of what has been done with respect to classical security protocols by using DTL [START_REF] Basin | Distributed Temporal Logic for the Analysis of Security Protocol Models[END_REF].

4. 1

 1 . Syntax Definition 1. Given a finite set Id = {i, j, . . .} of agent identifiers and a set Prop = {p, p 1 , p 2 , . . .} of atomic propositions (which characterize the current local states of the agents), we define the local language of an agent i ∈ Id by the grammar

  for every interpretation function I, | = µ,I γ | = µ Γ iff for every interpretation function I, | = µ,I Γ Γ | = γ iff for every QBDTL model M and interpretation function I, Γ | = µ,I γ [s i : A ⊃⊥] . . . . s j :⊥ s i : A ⊥E [s i : A] . . . .

Figure 1 :

 1 Figure 1: The rules of N(QBDTL): local life-cycle rules

Figure 2 :

 2 Figure 2: The rules of N(QBDTL): distributed life-cycle rules

Figure 3 :

 3 Figure 3: The rules of N(QBDTL): quantum transformation rules

Figure 4 :

 4 Figure 4: The rules of N(QBDTL): interaction rules

  Definition 11. A Hintikka structure is a structure (S, S ) such that for each state s ∈ S in it:1. ¬A ∈ s ⇒ A s; 2. α ∈ s ⇒ α 1 ∈ s and α 2 ∈ s; 3. β ∈ s ⇒ β 1 ∈ s or β 2 ∈ s; 4. ∀ A ∈ s ⇒for all t such that sRt, A ∈ t; 5. ∃ A ∈ s ⇒ for some t such that sRt, A ∈ t; 6. ∃ A ∈ s ⇒ there exists an s-branch b and for some t ∈ b, A ∈ t; 7. ∀ A ∈ s ⇒ for each s-branch b there exists t ∈ b such that A ∈ t; 8. c j A ∈ s ⇒ there exists t ∈ S j such that s S t and A ∈ t.

In analogy, note, e.g., that temporal logics developed to deal with concurrent systems do not possess any concurrent feature.

Note that in these rules we use relational formulas as auxiliary formulas in order to derive labeled formulas. Rules treating relational formulas as full-fledged first class formulas, which can be assumed and derived in the rules, could also be defined in the style of[START_REF] Viganò | Labelled Non-Classical Logics[END_REF].

We are aware of the clash with the amplitudes, but we prefer to overload α and β in order to keep the standard terminologies of both quantum computing and tableaux.

The work presented in this paper was partially supported by the EU FP7 Marie Curie PIRSES-GA-2012-318986 project "GeTFun: Generalizing Truth-Functionality". Part of this work was carried out while Luca

| = µ,I (i, x, q) : p and if | = µ,I Γ 2 then | = µ,I γ( j, y, q). We consider an I and a µ such that | = µ,I Γ = Γ 1 ∪ Γ 2 , and show that | = µ,I ( j, y, q) : p. As a consequence of the induction hypothesis, we get: (i) | = µ i ,I i S (x) i p; (ii) π i (I i S (x)) = I Q (q); and (iii) π j (I j S (y)) = I Q (q). It follows from (i) that p ∈ V(π i (I i S (x))), i.e., by (ii), p ∈ V(I Q (q)) and, by (iii), p ∈ V(π j (I j S (y))). By definition, we have | = µ,I j S (y) p, from which we infer | = µ,I ( j, y, q) : p. Now consider the case of an application of c I:

where Π is a proof of ( j, y, q ) : A from hypotheses in Γ 1 . By the induction hypothesis, we have Γ 1 | = ( j, y, q ) : A. We want to show that Γ = Γ 1 ∪ {(i, x, q) ( j, y, q )} | = (i, x, q) : c j A. Let us consider an arbitrary QBDTL model µ = λ, M, π and an interpretation function I, and assume that | = µ,I Γ holds. This implies last(I i S (x)) = last(I j S (y)) and π i (I i S (x)) = I Q (q). By the induction hypothesis, we also obtain | = µ,I ( j, y, q ) : A, which yields | = µ j ,I j S (y) j A. By the definition of local satisfaction relation, we infer | = µ i ,I i S (x) i c j A and then | = µ,I (i, x, q) : c j A. Since µ and I are arbitrary, we can conclude Γ | = (i, x, q) : c j A.

Finally, consider the case of an application of R⇒U:

where Π is a proof of ( j, x, q) : A from hypotheses in Γ 1 ∪ {q Uq } for some set Γ 1 of formulas. By the induction hypothesis, we have Γ 1 ∪ {q Uq } | = ( j, x, q) : A. We want to show that Γ = Γ 1 ∪ {(i, y, q ) * (i, z, q )} | = ( j, x, q) : A. Let us consider arbitrary µ = λ, M, π and I, and assume that | = µ,I Γ holds. This implies | = µ,I (i, y, q ) * (i, z, q ), from which we infer: last(I i S (y))

. By condition (i) in the definition of a QBDTL model and the property of universality behind connected components of S5 models, this yields I Q (q )UI Q (q ) and thus | = µ,I q Uq . By the induction hypothesis, we obtain | = µ,I ( j, x, q) : A. Since µ and I are arbitrary, we can conclude Γ | = ( j, x, q) : A.

Completeness

Completeness of N(QBDTL) is proved (i) by defining a decision procedure based on semantic tableaux and (ii) by showing a relation between the "closure" conditions in the tableaux and derivability of formulas in N(QBDTL). The structure of the proof is inspired mainly to the one given in [START_REF] Ben-Ari | The temporal logic of branching time[END_REF] for an Hilbert-style axiomatization of the logic UB. Similar proofs are presented in [START_REF] Emerson | Decision procedures and expressiveness in the temporal logic of branching time[END_REF][START_REF] Emerson | Temporal and Modal Logic[END_REF] for the logic CTL. In our setting, adaptations are required in order to deal with labeled formulas, with the synchronization mechanisms and operators and with the S5-like modal logic that determines the valuation of atomic propositions.

• Cl 1 : if A ∈ L n and ¬A ∈ L n , then n is a closed node and no further rules are applied to it;

• Cl 2 : if a node n 1 is being created by an application of R to n and there exists an ancestor n (also generated by R ) of n such that L n = L n 1 then do not create n 1 but create an edge oriented from n to n .

Lemma 1. The construction of a tableau T for a tableau formula ϕ terminates.

Proof. Just observe that the set of formulas that can occur in nodes of T is finite and then the closure rule Cl 2 will eventually prevent the creation of new nodes. In fact, each logical formula is a subformula of ϕ, a negation of a subformula or a dual of a subformula (possibly prefixed by ∀ or ∃ and possibly in the form of a communication formula). Since the set of agent labels occurring in ϕ is finite, the set of synchronization formulas is also finite.

Marking algorithm

In the following, we will refer to a node n as an α/β/ c / / -node if a rule R α /R β /R c /R /R has been applied to such a node during the tableau construction. In particular, in the case of a -node n, we can be more specific and say that it is a i -node for any agent i that occurs in n and is not blocked. Moreover, we say that a formula is a future formula if it has the form i : ∀ A, i :

The possible presence of cycles in a tableau T makes it not trivial to determine whether it is closed or not. Here we will define a two-step algorithm for marking the nodes of T . In the end of the process, we will have that it is possible to extract from T a Hintikka structure for the root formula iff the root of T is not marked.

1. Apply iteratively the following rules as long as possible:

• M Cl : Mark every closed leaf.

• M α : If n is an α-node and its son is marked, then mark n.

• M β : If n is a β-node and both its sons are marked, then mark n.

• M c : If n is a c -node and its son is marked, then mark n.

• M : If n is a -node and all its sons are marked, then mark n.

• M : If n is a -node and for each agent i occurring in n and not blocked, at least one of the i-sons of n is marked, then mark n.

We can define a structure (S, S ) as follows. For each i ∈ Id, S contains a triple {S i , R i , P i } such that:

• for each unmarked i -node n in T , there is a state n i in S i ;

• given n i ∈ S i , A ∈ P i (n i ) iff A ∈ L n ;

• given n i 1 , n i 2 ∈ S i , n i 1 R i n i 2 if there is a path (n 1 , m 0 , . . . , m k , n 2 ) in T such that m 0 , . . . , m k are not i -nodes.

Finally, given n i 1 ∈ S i and n j 2 ∈ S j , we say that (n i 1 , n j 2 ) ∈ S iff n 1 n 2 ∈ Cl (n 1 ) or n 1 n 2 ∈ Cl (n 2 ).