scholarly journals Relations among quantum processes: bisimilarity and congruence

2006 ◽  
Vol 16 (3) ◽  
pp. 407-428 ◽  
Author(s):  
MARIE LALIRE
Keyword(s):  
Quantum Communication ◽  
Operational Semantics ◽  
Parallel Composition ◽  
Quantum Processes ◽  
Algebraic Notation ◽  
Distributed Computations ◽  
Quantum Objects ◽  
Branching Bisimulation ◽  
Classical Computing ◽  
Process Algebraic

Full formal descriptions of algorithms making use of quantum principles must take into account both quantum and classical computing components, as well as communications between these components. Moreover, to model concurrent and distributed quantum computations and quantum communication protocols, communications over quantum channels that move qubits physically from one place to another must also be taken into account.Inspired by classical process algebras, which provide a framework for modelling cooperating computations, a process algebraic notation is defined. This notation provides a homogeneous style for formal descriptions of concurrent and distributed computations comprising both quantum and classical parts. Based upon an operational semantics that makes sure that quantum objects, operations and communications operate according to the postulates of quantum mechanics, an equivalence is defined among process states considered as having the same behaviour. This equivalence is a probabilistic branching bisimulation. From this relation, an equivalence on processes is defined. However, it is not a congruence because it is not preserved by parallel composition.

Types and typechecking for Communicating Quantum Processes

2006 ◽  
Vol 16 (3) ◽  
pp. 375-406 ◽  
Author(s):  
SIMON J. GAY ◽  
RAJAGOPAL NAGARAJAN
Keyword(s):  
Communication Systems ◽  
Quantum Communication ◽  
Formal Analysis ◽  
Operational Semantics ◽  
Type System ◽  
Quantum Processes ◽  
Classical Communication ◽  
Quantum Bits ◽  
Classical Systems ◽  
Pi Calculus

We define a language CQP (Communicating Quantum Processes) for modelling systems that combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and transformation of the quantum state; in particular, quantum bits (qubits) can be transmitted from process to process along communication channels. CQP has a static type system, which classifies channels, distinguishes between quantum and classical data, and controls the use of quantum states. We formally define the syntax, operational semantics and type system of CQP, prove that the semantics preserves typing, and prove that typing guarantees that each qubit is owned by a unique process within a system. We also define a typechecking algorithm and prove that it is sound and complete with respect to the type system. We illustrate CQP by defining models of several quantum communication systems, and outline our plans for using CQP as the foundation for formal analysis and verification of combined quantum and classical systems.

scholarly journals Verifying Quantum Communication Protocols with Ground Bisimulation

2020 ◽  
pp. 21-38
Author(s):  
Xudong Qin ◽  
Yuxin Deng ◽  
Wenjie Du
Keyword(s):  
Quantum Communication ◽  
Communication Protocols ◽  
Important Application ◽  
Process Algebras ◽  
Proof Technique ◽  
Quantum Processes ◽  
Quantum Process ◽  
Decision Method ◽  
Quantum Protocols ◽  
Suitable Notion

Abstract One important application of quantum process algebras is to formally verify quantum communication protocols. With a suitable notion of behavioural equivalence and a decision method, one can determine if an implementation of a protocol is consistent with its specification. Ground bisimulation is a convenient behavioural equivalence for quantum processes because of its associated coinduction proof technique. We exploit this technique to design and implement two on-the-fly algorithms for the strong and weak versions of ground bisimulation to check if two given processes in quantum CCS are equivalent. We then develop a tool that can verify interesting quantum protocols such as the BB84 quantum key distribution scheme.

scholarly journals Congruence from the operator’s point of view

2019 ◽  
Vol 57 (3-5) ◽  
pp. 329-351 ◽  
Author(s):  
Maciej Gazda ◽  
Wan Fokkink ◽  
Vittorio Massaro
Keyword(s):  
Operational Semantics ◽  
Point Of View ◽  
Parallel Composition ◽  
Standard Process ◽  
Specific Process ◽  
Weak Process ◽  
Congruence Relations ◽  
Syntactic Restrictions

AbstractA basic sanity property of a process semantics is that it constitutes a congruence with respect to standard process operators. This issue has been traditionally addressed by developing, for a specific process semantics, a syntactic format for operational semantics specifications. We suggest a novel, orthogonal approach, which focuses on a specific process operator and determines a class of congruence relations for this operator. To this end, we impose syntactic restrictions on Hennessy–Milner logic, so that a process semantics whose modal characterization satisfies those criteria is guaranteed to be a congruence with respect to the operator in question. We investigate alternative composition, action prefix, projection, encapsulation, renaming, and parallel composition with communication, in the context of both concrete and weak process semantics.

scholarly journals Domain Theory for Concurrency

2003 ◽  
Vol 10 (43) ◽  
Author(s):  
Mikkel Nygaard ◽  
Glynn Winskel
Keyword(s):  
Linear Logic ◽  
Operational Semantics ◽  
Denotational Semantics ◽  
Higher Order ◽  
The Other ◽  
Domain Theory ◽  
Parallel Composition ◽  
Concurrent Computation ◽  
Contextual Equivalence

A simple domain theory for concurrency is presented. Based on a categorical model of linear logic and associated comonads, it highlights the role of linearity in concurrent computation. Two choices of comonad yield two expressive metalanguages for higher-order processes, both arising from canonical constructions in the model. Their denotational semantics are fully abstract with respect to contextual equivalence. One language derives from an exponential of linear logic; it supports a straightforward operational semantics with simple proofs of soundness and adequacy. The other choice of comonad yields a model of affine-linear logic, and a process language with a tensor operation to be understood as a parallel composition of independent processes. The domain theory can be generalised to presheaf models, providing a more refined treatment of nondeterministic branching. The article concludes with a discussion of a broader programme of research, towards a fully fledged domain theory for concurrency.

scholarly journals Quantum-enhanced secure delegated classical computing

2016 ◽  
pp. 61-86
Author(s):  
Vedran Dunjko ◽  
Theodoros Kapourniotis ◽  
Elham Kashefi
Keyword(s):  
Quantum Computing ◽  
Quantum Communication ◽  
Quantum Correlations ◽  
Computational Power ◽  
Classical Computing ◽  
Computing Capacity

We present a family of quantumly-enhanced protocols to achieve unconditionally secure delegated classical computation where the client and the server have both their classical and quantum computing capacity limited. We prove the same task cannot be achieved using only classical protocols. This extends the work of Anders and Browne on the computational power of correlations to a security setting. In doing so we are able to highlight the power of online quantum communication as we prove the same task could not be achieved using pre-shared (offline) quantum correlations.

scholarly journals Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types

2020 ◽  
pp. 251-279 ◽  
Author(s):  
Sung-Shik Jongmans ◽  
Nobuko Yoshida
Keyword(s):  
Parallel Composition ◽  
Model Checker ◽  
Practical Result ◽  
Session Types ◽  
Deadlock Freedom ◽  
Algebraic Framework ◽  
A New Technique ◽  
Global Type ◽  
Existential Quantification ◽  
Process Algebraic

AbstractA key open problem with multiparty session types (MPST) concerns their expressiveness: current MPST have inflexible choice, no existential quantification over participants, and limited parallel composition. This precludes many real protocols to be represented by MPST. To overcome these bottlenecks of MPST, we explore a new technique using weak bisimilarity between global types and endpoint types, which guarantees deadlock-freedom and absence of protocol violations. Based on a process algebraic framework, we present well-formed conditions for global types that guarantee weak bisimilarity between a global type and its endpoint types and prove their check is decidable. Our main practical result, obtained through benchmarks, is that our well-formedness conditions can be checked orders of magnitude faster than directly checking weak bisimilarity using a state-of-the-art model checker.

scholarly journals Communication complexity and the reality of the wave function

2015 ◽  
Vol 30 (01) ◽  
pp. 1530001 ◽  
Author(s):  
Alberto Montina
Keyword(s):  
Quantum State ◽  
Communication Complexity ◽  
Quantum Communication ◽  
Communication Process ◽  
Minimal Amount ◽  
Quantum Processes ◽  
Independence Property ◽  
Classical Communication ◽  
Asymptotic Equipartition Property ◽  
Quantum Communication Complexity

In this review, we discuss a relation between quantum communication complexity and a long-standing debate in quantum foundation concerning the interpretation of the quantum state. Is the quantum state a physical element of reality as originally interpreted by Schrödinger? Or is it an abstract mathematical object containing statistical information about the outcome of measurements as interpreted by Born? Although these questions sound philosophical and pointless, they can be made precise in the framework of what we call classical theories of quantum processes, which are a reword of quantum phenomena in the language of classical probability theory. In 2012, Pusey, Barrett and Rudolph (PBR) proved, under an assumption of preparation independence, a theorem supporting the original interpretation of Schrödinger in the classical framework. The PBR theorem has attracted considerable interest revitalizing the debate and motivating other proofs with alternative hypotheses. Recently, we showed that these questions are related to a practical problem in quantum communication complexity, namely, quantifying the minimal amount of classical communication required in the classical simulation of a two-party quantum communication process. In particular, we argued that the statement of the PBR theorem can be proved if the classical communication cost of simulating the communication of n qubits grows more than exponentially in n. Our argument is based on an assumption that we call probability equipartition property. This property is somehow weaker than the preparation independence property used in the PBR theorem, as the former can be justified by the latter and the asymptotic equipartition property of independent stochastic sources. The probability equipartition property is a general and natural hypothesis that can be assumed even if the preparation independence hypothesis is dropped. In this review, we further develop our argument into the form of a theorem.

scholarly journals Mente Quântica / Problema Cérebro Classical

1969 ◽  
Vol 3 (1) ◽  
Author(s):  
Alfredo Pereira Júnior
Keyword(s):  
Quantum Coherence ◽  
Quantum Communication ◽  
Quantum Processes ◽  
Macroscopic System ◽  
Cold Temperatures ◽  
Physical Support ◽  
Neuronal Protein ◽  
The Mind ◽  
The Brain

The quantum theory of mind allows a shift from the Mind/Brain metaphysical problem to the Quantum Mind/Classical Brain scientific problem: how could systematic and coherent quantum processes - assumed to be the physical support of our conscious experiences - occur in a macroscopic system as the brain? I discuss a solution based on a neurobiological model that attributes to quantum computation in intra -neuronal protein networks the role of directly supporting phenomenal experience. In this model, quantum coherence is created or prepared by classical mechanisms as recurrent neuronal networks, oscillatory synchrony and gated membrane channels, thus avoiding common theoretical constraints for the existence of quantum communication and computation (ultra-cold temperatures and quasi-isolation from the environment).

scholarly journals Putting logic-based distributed systems on stable grounds

2015 ◽  
Vol 16 (4) ◽  
pp. 378-417
Author(s):  
TOM J. AMELOOT ◽  
JAN VAN DEN BUSSCHE ◽  
WILLIAM R. MARCZAK ◽  
PETER ALVARO ◽  
JOSEPH M. HELLERSTEIN
Keyword(s):  
Distributed Systems ◽  
Operational Semantics ◽  
Asynchronous Communication ◽  
Stable Model ◽  
Model Based ◽  
Distributed Computations ◽  
Declarative Semantics

AbstractIn the Declarative Networking paradigm, Datalog-like languages are used to express distributed computations. Whereas recently formal operational semantics for these languages have been developed, a corresponding declarative semantics has been lacking so far. The challenge is to capture precisely the amount of nondeterminism that is inherent to distributed computations due to concurrency, networking delays, and asynchronous communication. This paper shows how a declarative, model-based semantics can be obtained by simply using the well-known stable model semantics for Datalog with negation. We show that the model-based semantics matches previously proposed formal operational semantics.

Sign in / Sign up

Export Citation Format

Share Document