Searcharxiv⌕ Search

arXiv subjects

Luís Soares Barbosa

Publications and source records attributed to Luís Soares Barbosa.

6 recordsLinked to original sources

Bridging Resource Theory and Quantum Key Distribution: Geometric Analysis and Statistical Testing

Discerning between quantum and classical correlations is of great importance. Bell polytopes are well established as a fundamental tool. In this paper, we extend this line of inquiry by applying resource theory within the context of Network scenarios, to a Quantum Key Distribution (QKD) protocol. To achieve this, we consider the causal structure $P3$ that can describe the protocol, and we aim to develop useful statistical tests to assess it. More concretely, our objectives are twofold: firstly, to utilise the underlying causal structure of the QKD protocol to obtain a geometrical analysis of the resulting non-convex polytope, with a focus on the classical behaviours. Second, we devise a test within this framework to evaluate the distance between any two behaviours within the generated polytope. This approach offers a unique perspective, linking deviations from expected behaviour directly to the quality of the quantum resource or the residual nonclassicality in protocol execution.

quant-ph↗

Policy Gradients using Variational Quantum Circuits

Variational Quantum Circuits are being used as versatile Quantum Machine Learning models. Some empirical results exhibit an advantage in supervised and generative learning tasks. However, when applied to Reinforcement Learning, less is known. In this work, we considered a Variational Quantum Circuit composed of a low-depth hardware-efficient ansatz as the parameterized policy of a Reinforcement Learning agent. We show that an $ε$-approximation of the policy gradient can be obtained using a logarithmic number of samples concerning the total number of parameters. We empirically verify that such quantum models behave similarly or even outperform typical classical neural networks used in standard benchmarking environments and in quantum control, using only a fraction of the parameters. Moreover, we study the Barren Plateau phenomenon in quantum policy gradients using the Fisher Information Matrix spectrum.

quant-ph↗

A Logic for Paraconsistent Transition Systems

Modelling complex information systems often entails the need for dealing with scenarios of inconsistency in which several requirements either reinforce or contradict each other. In this kind of scenarios, arising e.g. in knowledge representation, simulation of biological systems, or quantum computation, inconsistency has to be addressed in a precise and controlled way. This paper generalises Belnap-Dunn four-valued logic, introducing paraconsistent transition systems (PTS), endowed with positive and negative accessibility relations, and a metric space over the lattice of truth values, and their modal logic.

cs.LO↗

Simulation of non-radiative energy transfer in photosynthetic systems using a quantum computer

Photosynthesis is an important and complex physical process in nature, whose comprehensive understanding would have many relevant industrial applications, for instance in the field of energy production. In this paper we propose a quantum algorithm for the simulation of the excitonic transport of energy, occurring in the first stage of the process of photosynthesis. The algorithm takes in account the quantum and environmental effects (pure-dephasing), influencing the quantum transport. We performed quantum simulations of such phenomena, for a proof of concept scenario, in an actual quantum computer the IBM Q, of 5 qubits. We validate the results with the Haken-Ströbl model and discuss the influence of environmental parameters on the efficiency of the energy transport.

quant-ph↗

Generalising KAT to verify weighted computations

Kleene algebra with tests (KAT) was introduced as an algebraic structure to model and reason about classic imperative programs, i.e. sequences of discrete transitions guarded by Boolean tests. This paper introduces two generalisations of this structure able to express programs as weighted transitions and tests with outcomes in non necessarily bivalent truth spaces: graded Kleene algebra with tests (GKAT) and a variant where tests are also idempotent (I-GKAT). On this context, and in analogy to Kozen's encoding of Propositional Hoare Logic (PHL) in KAT [22], we discuss the encoding of a graded PHL in I-GKAT and of its while-free fragment in GKAT. Moreover, to establish semantics for these structures four new algebras are defined: FSET(T), FREL(K,T) and FLANG(K,T) over complete residuated lattices K and T, and M(n,A) over a GKAT or I-GKAT A. As a final exercise, the paper discusses some program equivalence proofs in a graded context.

cs.LO↗

Bisimilarity and refinement for hybrid(ised) logics

The complexity of modern software systems entails the need for reconfiguration mechanisms gov- erning the dynamic evolution of their execution configurations in response to both external stimulus or internal performance measures. Formally, such systems may be represented by transition systems whose nodes correspond to the different configurations they may assume. Therefore, each node is en- dowed with, for example, an algebra, or a first-order structure, to precisely characterise the semantics of the services provided in the corresponding configuration. Hybrid logics, which add to the modal description of transition structures the ability to refer to specific states, offer a generic framework to approach the specification and design of this sort of systems. Therefore, the quest for suitable notions of equivalence and refinement between models of hybrid logic specifications becomes fundamental to any design discipline adopting this perspective. This paper contributes to this effort from a distinctive point of view: instead of focussing on a specific hybrid logic, the paper introduces notions of bisimilarity and refinement for hybridised logics, i.e. standard specification logics (e.g. propositional, equational, fuzzy, etc) to which modal and hybrid features were added in a systematic way.

cs.LO↗