BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Mingsheng Ying

Mingsheng Ying appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
quant-phLogic in Computer ScienceProgramming LanguagesArtificial IntelligenceCryptography and SecuritySoftware EngineeringComputation and LanguageDatabasesDiscrete MathematicsDistributed, Parallel, and Cluster ComputingEmerging TechnologiesFormal Languages and Automata TheoryMachine Learning

Catalog footprint

What is connected

54works
13topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

54 published item(s)

preprint2022arXiv

Algebraic Reasoning of Quantum Programs via Non-idempotent Kleene Algebra

We investigate the algebraic reasoning of quantum programs inspired by the success of classical program analysis based on Kleene algebra. One prominent example of such is the famous Kleene Algebra with Tests (KAT), which has furnished both theoretical insights and practical tools. The succinctness of algebraic reasoning would be especially desirable for scalable analysis of quantum programs, given the involvement of exponential-size matrices in most of the existing methods. A few key features of KAT including the idempotent law and the nice properties of classical tests, however, fail to hold in the context of quantum programs due to their unique quantum features, especially in branching. We propose Non-idempotent Kleene Algebra (NKA) as a natural alternative and identify complete and sound semantic models for NKA as well as their quantum interpretations. In light of applications of KAT, we demonstrate algebraic proofs in NKA of quantum compiler optimization and the normal form of quantum while-programs. Moreover, we extend NKA with Tests (i.e., NKAT), where tests model quantum predicates following effect algebra, and illustrate how to encode propositional quantum Hoare logic as NKAT theorems.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs

A first-order logic with quantum variables is needed as an assertion language for specifying and reasoning about various properties (e.g. correctness) of quantum programs. Surprisingly, such a logic is missing in the literature, and the existing first-order Birkhoff-von Neumann quantum logic deals with only classical variables and quantifications over them. In this paper, we fill in this gap by introducing a first-order extension of Birkhoff-von Neumann quantum logic with universal and existential quantifiers over quantum variables. Examples are presented to show our logic is particularly suitable for specifying some important properties studied in quantum computation and quantum information. We further incorporate this logic into quantum Hoare logic as an assertion logic so that it can play a role similar to that of first-order logic for classical Hoare logic and BI-logic for separation logic. In particular, we show how it can be used to define and derive quantum generalisations of some adaptation rules that have been applied to significantly simplify verification of classical programs. It is expected that the assertion logic defined in this paper - first-order quantum logic with quantum variables - can be combined with various quantum program logics to serve as a solid logical foundation upon which verification tools can be built using proof assistants such as Coq and Isabelle/HOL.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Equivalence Checking of Quantum Finite-State Machines

In this paper, we introduce the model of quantum Mealy machines and study the equivalence checking and minimisation problems of them. Two efficient algorithms are developed for checking equivalence of two states in the same machine and for checking equivalence of two machines. As an application, they are used in equivalence checking of quantum circuits. Moreover, the minimisation problem is proved to be in $\textbf{PSPACE}$.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Equivalence Checking of Sequential Quantum Circuits

We define a formal framework for equivalence checking of sequential quantum circuits. The model we adopt is a quantum state machine, which is a natural quantum generalisation of Mealy machines. A major difficulty in checking quantum circuits (but not present in checking classical circuits) is that the state spaces of quantum circuits are continuums. This difficulty is resolved by our main theorem showing that equivalence checking of two quantum Mealy machines can be done with input sequences that are taken from some chosen basis (which are finite) and have a length quadratic in the dimensions of the state Hilbert spaces of the machines. Based on this theoretical result, we develop an (and to the best of our knowledge, the first) algorithm for checking equivalence of sequential quantum circuits with running time $\mathcal{O}(2^{3m+5l}(2^{3m}+2^{3l}))$, where $m$ and $l$ denote the numbers of input and internal qubits, respectively. The complexity of our algorithm is comparable with that of the known algorithms for checking classical sequential circuits in the sense that both are exponential in the number of (qu)bits. Several case studies and experiments are presented.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Quantum Algorithm for Fidelity Estimation

For two unknown mixed quantum states $ρ$ and $σ$ in an $N$-dimensional Hilbert space, computing their fidelity $F(ρ,σ)$ is a basic problem with many important applications in quantum computing and quantum information, for example verification and characterization of the outputs of a quantum computer, and design and analysis of quantum algorithms. In this paper, we propose a quantum algorithm that solves this problem in $\operatorname{poly}(\log (N), r, 1/\varepsilon)$ time, where $r$ is the lower rank of $ρ$ and $σ$, and $\varepsilon$ is the desired precision, provided that the purifications of $ρ$ and $σ$ are prepared by quantum oracles. This algorithm exhibits an exponential speedup over the best known algorithm (based on quantum state tomography) which has time complexity polynomial in $N$.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Quantum Random Access Stored-Program Machines

Random access machines (RAMs) and random access stored-program machines (RASPs) are models of computing that are closer to the architecture of real-world computers than Turing machines (TMs). They are also convenient in complexity analysis of algorithms. The relationships between RAMs, RASPs and TMs are well-studied. However, clear relationships between their quantum counterparts are still missing in the literature. We fill in this gap by formally defining the models of quantum random access machines (QRAMs) and quantum random access stored-program machines (QRASPs) and clarifying the relationships between QRAMs, QRASPs and quantum Turing machines (QTMs). In particular, we show that $\textbf{P} \subseteq \textbf{EQRAMP} \subseteq \textbf{EQP} \subseteq \textbf{BQP} = \textbf{BQRAMP}$, where $\textbf{EQRAMP}$ and $\textbf{BQRAMP}$ stand for the sets of problems that can be solved by polynomial-time QRAMs with certainty and bounded-error, respectively. At the heart of our proof, is a standardisation of QTM with an extended halting scheme, which is of independent interest.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs (Extended Version)

We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition. Then, we show that the expected runtime of a quantum program can be represented as the expectation of an observable (in physics). A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method, including computing the expected runtime of quantum Bernoulli Factory -- a quantum algorithm for generating random numbers. In particular, using our new method, an open problem of computing the expected runtime of quantum random walks introduced by Ambainis et al. (STOC 2001) is solved.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

VeriQBench: A Benchmark for Multiple Types of Quantum Circuits

In this paper, we introduce VeriQBench -- an open source benchmark for quantum circuits. It offers high-level quantum circuit abstractions of various circuit types, including 1) combinational, 2) dynamic, 3) sequential, and 4) variational quantum circuits, which cover almost all existing types of quantum circuits in the literature. Meanwhile, VeriQBench is a versatile benchmark which can be used in verifying quantum software for different applications, as is evidenced by the existing works including quantum circuit verification (e.g., equivalence checking [Hon+21a; WLY21] and model checking [Yin21]), simulation (e.g., fault simulation), testing (e.g., test pattern generation [CY22]) and debugging (e.g., runtime assertions [Li+20b]). All the circuits are described in OpenQASM and are validated on Qiskit and QCOR simulators. With the hope that it can be used by other researchers, VeriQBench is released at: https://github.com/Veri-Q/Benchmark.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

A Quantum Interpretation of Bunched Logic for Quantum Separation Logic

We propose a model of the substructural logic of Bunched Implications (BI) that is suitable for reasoning about quantum states. In our model, the separating conjunction of BI describes separable quantum states. We develop a program logic where pre- and post-conditions are BI formulas describing quantum states -- the program logic can be seen as a counterpart of separation logic for imperative quantum programs. We exercise the logic for proving the security of quantum one-time pad and secret sharing, and we show how the program logic can be used to discover a flaw in Google Cirq's tutorial on the Variational Quantum Algorithm (VQA).

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

An HHL-Based Algorithm for Computing Hitting Probabilities of Quantum Random Walks

We present a novel application of the HHL (Harrow-Hassidim-Lloyd) algorithm -- a quantum algorithm solving systems of linear equations -- in solving an open problem about quantum random walks, namely computing hitting (or absorption) probabilities of a general (not only Hadamard) one-dimensional quantum random walks with two absorbing boundaries. This is achieved by a simple observation that the problem of computing hitting probabilities of quantum random walks can be reduced to inverting a matrix. Then a quantum algorithm with the HHL algorithm as a subroutine is developed for solving the problem, which is faster than the known classical algorithms by numerical experiments.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Quantum Hoare logic with classical variables

Hoare logic provides a syntax-oriented method to reason about program correctness and has been proven effective in the verification of classical and probabilistic programs. Existing proposals for quantum Hoare logic either lack completeness or support only quantum variables, thus limiting their capability in practical use. In this paper, we propose a quantum Hoare logic for a simple while language which involves both classical and quantum variables. Its soundness and relative completeness are proven for both partial and total correctness of quantum programs written in the language. Remarkably, with novel definitions of classical-quantum states and corresponding assertions, the logic system is quite simple and similar to the traditional Hoare logic for classical programs. Furthermore, to simplify reasoning in real applications, auxiliary proof rules are provided which support standard logical operation in the classical part of assertions, and of super-operator application in the quantum part. Finally, a series of practical quantum algorithms, in particular the whole algorithm of Shor's factorisation, are formally verified to show the effectiveness of the logic.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Verification of Distributed Quantum Programs

Distributed quantum systems and especially the Quantum Internet have the ever-increasing potential to fully demonstrate the power of quantum computation. This is particularly true given that developing a general-purpose quantum computer is much more difficult than connecting many small quantum devices. One major challenge of implementing distributed quantum systems is programming them and verifying their correctness. In this paper, we propose a CSP-like distributed programming language to facilitate the specification and verification of such systems. After presenting its operational and denotational semantics, we develop a Hoare-style logic for distributed quantum programs and establish its soundness and (relative) completeness with respect to both partial and total correctness. The effectiveness of the logic is demonstrated by its applications in the verification of quantum teleportation and local implementation of non-local CNOT gates, two important algorithms widely used in distributed quantum systems.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Proq: Projection-based Runtime Assertions for Debugging on a Quantum Computer

In this paper, we propose Proq, a runtime assertion scheme for testing and debugging quantum programs on a quantum computer. The predicates in Proq are represented by projections (or equivalently, closed subspaces of the state space), following Birkhoff-von Neumann quantum logic. The satisfaction of a projection by a quantum state can be directly checked upon a small number of projective measurements rather than a large number of repeated executions. On the theory side, we rigorously prove that checking projection-based assertions can help locate bugs or statistically assure that the semantic function of the tested program is close to what we expect, for both exact and approximate quantum programs. On the practice side, we consider hardware constraints and introduce several techniques to transform the assertions, making them directly executable on the measurement-restricted quantum computers. We also propose to achieve simplified assertion implementation using local projection technique with soundness guaranteed. We compare Proq with existing quantum program assertions and demonstrate the effectiveness and efficiency of Proq by its applications to assert two ingenious quantum algorithms, the Harrow-Hassidim-Lloyd algorithm and Shor's algorithm.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

A Theorem Prover for Quantum Hoare Logic and Its Applications

Quantum Hoare Logic (QHL) was introduced in Ying's work to specify and reason about quantum programs. In this paper, we implement a theorem prover for QHL based on Isabelle/HOL. By applying the theorem prover, verifying a quantum program against a specification is transformed equivalently into an order relation between matrices. Due to the limitation of Isabelle/HOL, the calculation of the order relation is solved by calling an outside oracle written in Python. To the best of our knowledge, this is the first theorem prover for quantum programs. To demonstrate its power, the correctness of two well-known quantum algorithms, i.e., Grover Quantum Search and Quantum Phase Estimation (the key step in Shor's quantum algorithm of factoring in polynomial time) are proved using the theorem prover. These are the first mechanized proofs for both of them.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Quantum Privacy-Preserving Data Mining

Data mining is a key technology in big data analytics and it can discover understandable knowledge (patterns) hidden in large data sets. Association rule is one of the most useful knowledge patterns, and a large number of algorithms have been developed in the data mining literature to generate association rules corresponding to different problems and situations. Privacy becomes a vital issue when data mining is used to sensitive data sets like medical records, commercial data sets and national security. In this Letter, we present a quantum protocol for mining association rules on vertically partitioned databases. The quantum protocol can improve the privacy level preserved by known classical protocols and at the same time it can exponentially reduce the computational complexity and communication cost.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Toward automatic verification of quantum cryptographic protocols

Several quantum process algebras have been proposed and successfully applied in verification of quantum cryptographic protocols. All of the bisimulations proposed so far for quantum processes in these process algebras are state-based, implying that they only compare individual quantum states, but not a combination of them. This paper remedies this problem by introducing a novel notion of distribution-based bisimulation for quantum processes. We further propose an approximate version of this bisimulation that enables us to prove more sophisticated security properties of quantum protocols which cannot be verified using the previous bisimulations. In particular, we prove that the quantum key distribution protocol BB84 is sound and (asymptotically) secure against the intercept-resend attacks by showing that the BB84 protocol, when executed with such an attacker concurrently, is approximately bisimilar to an ideal protocol, whose soundness and security are obviously guaranteed, with at most an exponentially decreasing gap.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

(Un)decidable Problems about Reachability of Quantum Systems

We study the reachability problem of a quantum system modelled by a quantum automaton. The reachable sets are chosen to be boolean combinations of (closed) subspaces of the state space of the quantum system. Four different reachability properties are considered: eventually reachable, globally reachable, ultimately forever reachable, and infinitely often reachable. The main result of this paper is that all of the four reachability properties are undecidable in general; however, the last three become decidable if the reachable sets are boolean combinations without negation.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Alternation in Quantum Programming: From Superposition of Data to Superposition of Programs

We extract a novel quantum programming paradigm - superposition of programs - from the design idea of a popular class of quantum algorithms, namely quantum walk-based algorithms. The generality of this paradigm is guaranteed by the universality of quantum walks as a computational model. A new quantum programming language QGCL is then proposed to support the paradigm of superposition of programs. This language can be seen as a quantum extension of Dijkstra's GCL (Guarded Command Language). Surprisingly, alternation in GCL splits into two different notions in the quantum setting: classical alternation (of quantum programs) and quantum alternation, with the latter being introduced in QGCL for the first time. Quantum alternation is the key program construct for realizing the paradigm of superposition of programs. The denotational semantics of QGCL are defined by introducing a new mathematical tool called the guarded composition of operator-valued functions. Then the weakest precondition semantics of QGCL can straightforwardly derived. Another very useful program construct in realizing the quantum programming paradigm of superposition of programs, called quantum choice, can be easily defined in terms of quantum alternation. The relation between quantum choices and probabilistic choices is clarified through defining the notion of local variables. We derive a family of algebraic laws for QGCL programs that can be used in program verification, transformations and compilation. The expressive power of QGCL is illustrated by several examples where various variants and generalizations of quantum walks are conveniently expressed using quantum alternation and quantum choice. We believe that quantum programming with quantum alternation and choice will play an important role in further exploiting the power of quantum computing.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Debugging Quantum Processes Using Monitoring Measurements

Since observation on a quantum system may cause the system state collapse, it is usually hard to find a way to monitor a quantum process, which is a quantum system that continuously evolves. We propose a protocol that can debug a quantum process by monitoring, but not disturb the evolution of the system. This protocol consists of an error detector and a debugging strategy. The detector is a projection operator that is orthogonal to the anticipated system state at a sequence of time points, and the strategy is used to specify these time points. As an example, we show how to debug the computational process of quantum search using this protocol. By applying the Skolem--Mahler--Lech theorem in algebraic number theory, we find an algorithm to construct all of the debugging protocols for quantum processes of time independent Hamiltonians.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Distinguishability of Quantum States by Positive Operator-Valued Measures with Positive Partial Transpose

We study the distinguishability of bipartite quantum states by Positive Operator-Valued Measures with positive partial transpose (PPT POVMs). The contributions of this paper include: (1). We give a negative answer to an open problem of [M. Horodecki $et. al$, Phys. Rev. Lett. 90, 047902(2003)] showing a limitation of their method for detecting nondistinguishability. (2). We show that a maximally entangled state and its orthogonal complement, no matter how many copies are supplied, can not be distinguished by PPT POVMs, even unambiguously. This result is much stronger than the previous known ones \cite{DUAN06,BAN11}. (3). We study the entanglement cost of distinguishing quantum states. It is proved that $\sqrt{2/3}\ket{00}+\sqrt{1/3}\ket{11}$ is sufficient and necessary for distinguishing three Bell states by PPT POVMs. An upper bound of entanglement cost of distinguishing a $d\otimes d$ pure state and its orthogonal complement is obtained for separable operations. Based on this bound, we are able to construct two orthogonal quantum states which cannot be distinguished unambiguously by separable POVMs, but finite copies would make them perfectly distinguishable by LOCC. We further observe that a two-qubit maximally entangled state is always enough for distinguishing a $d\otimes d$ pure state and its orthogonal complement by PPT POVMs, no matter the value of $d$. In sharp contrast, an entangled state with Schmidt number at least $d$ is always needed for distinguishing such two states by separable POVMs. As an application, we show that the entanglement cost of distinguishing a $d\otimes d$ maximally entangled state and its orthogonal complement must be a maximally entangled state for $d=2$,which implies that teleportation is optimal; and in general, it could be chosen as $\mathcal{O}(\frac{\log d}{d})$.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Quantum Recursion and Second Quantisation

This paper introduces a new notion of quantum recursion of which the control flow of the computation is quantum rather than classical as in the notions of recursion considered in the previous studies of quantum programming. A typical example is recursive quantum walks, which are obtained by slightly modifying the construction of the ordinary quantum walks. The operational and denotational semantics of quantum recursions are defined by employing the second quantisation method, and they are proved to be equivalent.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Reachability Analysis of Quantum Markov Decision Processes

We introduce the notion of quantum Markov decision process (qMDP) as a semantic model of nondeterministic and concurrent quantum programs. It is shown by examples that qMDPs can be used in analysis of quantum algorithms and protocols. We study various reachability problems of qMDPs both for the finite-horizon and for the infinite-horizon. The (un)decidability and complexity of these problems are settled, or their relationships with certain long-standing open problems are clarified. We also develop an algorithm for finding optimal scheduler that attains the supremum reachability probability.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Bisimulation for quantum processes

In this paper we introduce a novel notion of probabilistic bisimulation for quantum processes and prove that it is congruent with respect to various process algebra combinators including parallel composition even when both classical and quantum communications are present. We also establish some basic algebraic laws for this bisimulation. In particular, we prove uniqueness of the solutions to recursive equations of quantum processes, which provides a powerful proof technique for verifying complex quantum protocols.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Five Two-Qubit Gates Are Necessary for Implementing Toffoli Gate

In this paper, we settle the long-standing open problem of the minimum cost of two-qubit gates for simulating a Toffoli gate. More precisely, we show that five two-qubit gates are necessary. Before our work, it is known that five gates are sufficient and only numerical evidences have been gathered, indicating that the five-gate implementation is necessary. The idea introduced here can also be used to solve the problem of optimal simulation of three-qubit control phase introduced by Deutsch in 1989.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Model checking quantum Markov chains

Although the security of quantum cryptography is provable based on the principles of quantum mechanics, it can be compromised by the flaws in the design of quantum protocols and the noise in their physical implementations. So, it is indispensable to develop techniques of verifying and debugging quantum cryptographic systems. Model-checking has proved to be effective in the verification of classical cryptographic protocols, but an essential difficulty arises when it is applied to quantum systems: the state space of a quantum system is always a continuum even when its dimension is finite. To overcome this difficulty, we introduce a novel notion of quantum Markov chain, specially suited to model quantum cryptographic protocols, in which quantum effects are entirely encoded into super-operators labelling transitions, leaving the location information (nodes) being classical. Then we define a quantum extension of probabilistic computation tree logic (PCTL) and develop a model-checking algorithm for quantum Markov chains.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Optimal simulation of three-qubit gates

In this paper, we study the optimal simulation of three-qubit unitary by using two-qubit gates. First, we give a lower bound on the two-qubit gates cost of simulating a multi-qubit gate. Secondly, we completely characterize the two-qubit gate cost of simulating a three-qubit controlled controlled gate by generalizing our result on the cost of Toffoli gate. The function of controlled controlled gate is simply a three-qubit controlled unitary gate and can be intuitively explained as follows: the gate will output the states of the two control qubit directly, and apply the given one-qubit unitary $u$ on the target qubit only if both the states of the control are $\ket{1}$. Previously, it is only known that five two-qubit gates is sufficient for implementing such a gate [Sleator and Weinfurter, Phys. Rev. Lett. 74, 4087 (1995)]. Our result shows that if the determinant of $u$ is 1, four two-qubit gates is achievable optimal. Otherwise, five is optimal. Thirdly, we show that five two-qubit gates are necessary and sufficient for implementing the Fredkin gate(the controlled swap gate), which settles the open problem introduced in [Smolin and DiVincenzo, Phys. Rev. A, 53, 2855 (1996)]. The Fredkin gate is one of the most important quantum logic gates because it is universal alone for classical reversible computation, and thus with little help, universal for quantum computation. Before our work, a five two-qubit gates decomposition of the Fredkin gate was already known, and numerical evidence of showing five is optimal is found.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Probabilistic bisimilarities between quantum processes

Modeling and reasoning about concurrent quantum systems is very important both for distributed quantum computing and for quantum protocol verification. As a consequence, a general framework describing formally the communication and concurrency in complex quantum systems is necessary. For this purpose, we propose a model qCCS which is a natural quantum extension of classical value-passing CCS with the input and output of quantum states, and unitary transformations and measurements on quantum systems. The operational semantics of qCCS is given based on probabilistic labeled transition system. This semantics has many different features compared with the proposals in literature in order to describe input and output of quantum systems which are possibly correlated with other components. Based on this operational semantics, we introduce the notions of strong probabilistic bisimilarity and weak probabilistic bisimilarity between quantum processes and discuss some properties of them, such as congruence under various combinators.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Quantum Information-Flow Security: Noninterference and Access Control

Quantum cryptography has been extensively studied in the last twenty years, but information-flow security of quantum computing and communication systems has been almost untouched in the previous research. Duo to the essential difference between classical and quantum systems, formal methods developed for classical systems, including probabilistic systems, cannot be directly applied to quantum systems. This paper defines an automata model in which we can rigorously reason about information-flow security of quantum systems. The model is a quantum generalisation of Goguen and Meseguer's noninterference. The unwinding proof technique for quantum noninterference is developed, and a certain compositionality of security for quantum systems is established. The proposed formalism is then used to prove security of access control in quantum systems.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Reachability Probabilities of Quantum Markov Chains

This paper studies three kinds of long-term behaviours, namely reachability, repeated reachability and persistence, of quantum Markov chains (qMCs). As a stepping-stone, we introduce the notion of bottom strongly connected component (BSCC) of a qMC and develop an algorithm for finding BSCC decompositions of the state space of a qMC. As the major contribution, several (classical) algorithms for computing the reachability, repeated reachability and persistence probabilities of a qMC are presented, and their complexities are analysed.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Defining Quantum Control Flow

A remarkable difference between quantum and classical programs is that the control flow of the former can be either classical or quantum. One of the key issues in the theory of quantum programming languages is defining and understanding quantum control flow. A functional language with quantum control flow was defined by Altenkirch and Grattage [\textit{Proc. LICS'05}, pp. 249-258]. This paper extends their work, and we introduce a general quantum control structure by defining three new quantum program constructs, namely quantum guarded command, quantum choice and quantum recursion. We clarify the relation between quantum choices and probabilistic choices. An interesting difference between quantum recursions with classical control flows and with quantum control flows is revealed.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Four Locally Indistinguishable Ququad-Ququad Orthogonal Maximally Entangled States

We explicitly exhibit a set of four ququad-ququad orthogonal maximally entangled states that cannot be perfectly distinguished by means of local operations and classical communication. Before our work, it was unknown whether there is a set of $d$ locally indistinguishable $d\otimes d$ orthogonal maximally entangled states for some positive integer $d$. We further show that a $2\otimes 2$ maximally entangled state can be used to locally distinguish this set of states without being consumed, thus demonstrate a novel phenomenon of "Entanglement Discrimination Catalysis". Based on this set of states, we construct a new set $\mathrm{K}$ consisting of four locally indistinguishable states such that $\mathrm{K}^{\otimes m}$ (with $4^m$ members) is locally distinguishable for some $m$ greater than one. As an immediate application, we construct a noisy quantum channel with one sender and two receivers whose local zero-error classical capacity can achieve the full dimension of the input space but only with a multi-shot protocol.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Session Communication and Integration

The scenario-based specification of a large distributed system is usually naturally decomposed into various modules. The integration of specification modules contrasts to the parallel composition of program components, and includes various ways such as scenario concatenation, choice, and nesting. The recent development of multiparty session types for process calculi provides useful techniques to accommodate the protocol modularisation, by encoding fragments of communication protocols in the usage of private channels for a class of agents. In this paper, we extend forgoing session type theories by enhancing the session integration mechanism. More specifically, we propose a novel synchronous multiparty session type theory, in which sessions are separated into the communicating and integrating levels. Communicating sessions record the message-based communications between multiple agents, whilst integrating sessions describe the integration of communicating ones. A two-level session type system is developed for pi-calculus with syntactic primitives for session establishment, and several key properties of the type system are studied. Applying the theory to system description, we show that a channel safety property and a session conformance property can be analysed. Also, to improve the utility of the theory, a process slicing method is used to help identify the violated sessions in the type checking.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Symbolic bisimulation for quantum processes

With the previous notions of bisimulation presented in literature, to check if two quantum processes are bisimilar, we have to instantiate the free quantum variables of them with arbitrary quantum states, and verify the bisimilarity of resultant configurations. This makes checking bisimilarity infeasible from an algorithmic point of view because quantum states constitute a continuum. In this paper, we introduce a symbolic operational semantics for quantum processes directly at the quantum operation level, which allows us to describe the bisimulation between quantum processes without resorting to quantum states. We show that the symbolic bisimulation defined here is equivalent to the open bisimulation for quantum processes in the previous work, when strong bisimulations are considered. An algorithm for checking symbolic ground bisimilarity is presented. We also give a modal logical characterisation for quantum bisimilarity based on an extension of Hennessy-Milner logic to quantum processes.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Termination of Nondeterministic Quantum Programs

We define a language-independent model of nondeterministic quantum programs in which a quantum program consists of a finite set of quantum processes. These processes are represented by quantum Markov chains over the common state space. An execution of a nondeterministic quantum program is modeled by a sequence of actions of individual processes. These actions are described by super-operators on the state Hilbert space. At each step of an execution, a process is chosen nondeterministically to perform the next action. A characterization of reachable space and a characterization of diverging states of a nondeterministic quantum program are presented. We establish a zero-one law for termination probability of the states in the reachable space of a nondeterministic quantum program. A combination of these results leads to a necessary and sufficient condition for termination of nondeterministic quantum programs. Based on this condition, an algorithm is found for checking termination of nondeterministic quantum programs within a fixed finite-dimensional state space. A striking difference between nondeterministic classical and quantum programs is shown by example: it is possible that each of several quantum programs simulates the same classical program which terminates with probability 1, but the nondeterministic program consisting of them terminates with probability 0 due to the interference carried in the execution of them.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Verification of Quantum Programs

This paper develops verification methodology for quantum programs, and the contribution of the paper is two-fold: 1. Sharir, Pnueli and Hart [SIAM J. Comput. 13(1984)292-314] presented a general method for proving properties of probabilistic programs, in which a probabilistic program is modeled by a Markov chain and an assertion on the output distribution is extended into an invariant assertion on all intermediate distributions. Their method is essentially a probabilistic generalization of the classical Floyd inductive assertion method. In this paper, we consider quantum programs modeled by quantum Markov chains which are defined by super-operators. It is shown that the Sharir-Pnueli-Hart method can be elegantly generalized to quantum programs by exploiting the Schrödinger-Heisenberg duality between quantum states and observables. In particular, a completeness theorem for the Sharir-Pnueli-Hart verification method of quantum programs is established. 2. As indicated by the completeness theorem, the Sharir-Pnueli-Hart method is in principle effective for verifying all properties of quantum programs that can be expressed in terms of Hermitian operators (observables). But it is not feasible for many practical applications because of the complicated calculation involved in the verification. For the case of finite-dimensional state spaces, we find a method for verification of quantum programs much simpler than the Sharir-Pnueli-Hart method by employing the matrix representation of super-operators and Jordan decomposition of matrices. In particular, this method enables us to compute easily the average running time and even to analyze some interesting long-run behaviors of quantum programs in a finite-dimensional state space.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

An Algebra of Quantum Processes

We introduce an algebra qCCS of pure quantum processes in which no classical data is involved, communications by moving quantum states physically are allowed, and computations is modeled by super-operators. An operational semantics of qCCS is presented in terms of (non-probabilistic) labeled transition systems. Strong bisimulation between processes modeled in qCCS is defined, and its fundamental algebraic properties are established, including uniqueness of the solutions of recursive equations. To model sequential computation in qCCS, a reduction relation between processes is defined. By combining reduction relation and strong bisimulation we introduce the notion of strong reduction-bisimulation, which is a device for observing interaction of computation and communication in quantum systems. Finally, a notion of strong approximate bisimulation (equivalently, strong bisimulation distance) and its reduction counterpart are introduced. It is proved that both approximate bisimilarity and approximate reduction-bisimilarity are preserved by various constructors of quantum processes. This provides us with a formal tool for observing robustness of quantum processes against inaccuracy in the implementation of its elementary gates.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Any $2\otimes n$ subspace is locally distinguishable

A subspace of a multipartite Hilbert space is called \textit{locally indistinguishable} if any orthogonal basis of this subspace cannot be perfectly distinguished by local operations and classical communication. Previously it was shown that any $m\otimes n$ bipartite system such that $m>2$ and $n>2$ has a locally indistinguishable subspace. However, it has been an open problem since 2005 whether there is a locally indistinguishable bipartite subspace with a qubit subsystem. We settle this problem by showing that any $2\otimes n$ bipartite subspace is locally distinguishable in the sense it contains a basis perfectly distinguishable by LOCC. As an interesting application, we show that any quantum channel with two Kraus operations has optimal environment-assisted classical capacity.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Majorization in Quantum Adiabatic Algorithms

The majorization theory has been applied to analyze the mathematical structure of quantum algorithms. An empirical conclusion by numerical simulations obtained in the previous literature indicates that step-by-step majorization seems to appear universally in quantum adiabatic algorithms. In this paper, a rigorous analysis of the majorization arrow in a special class of quantum adiabatic algorithms is carried out. In particular, we prove that for any adiabatic algorithm of this class, step-by-step majorization of the ground state holds exactly. For the actual state, we show that step-by-step majorization holds approximately, and furthermore that the longer the running time of the algorithm, the better the approximation.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Model-Checking Linear-Time Properties of Quantum Systems

We define a formal framework for reasoning about linear-time properties of quantum systems in which quantum automata are employed in the modeling of systems and certain closed subspaces of state (Hilbert) spaces are used as the atomic propositions about the behavior of systems. We provide an algorithm for verifying invariants of quantum automata. Then automata-based model-checking technique is generalized for the verification of safety properties recognizable by reversible automata and omega-properties recognizable by reversible Buechi automata.

0 citations0 reviewsNo code linkedOpen access
preprint2009arXiv

Local Unambiguous Discrimination with Remaining Entanglement

A bipartite state which is secretly chosen from a finite set of known entangled pure states cannot be immediately useful in standard quantum information processing tasks. To effectively make use of the entanglement contained in this unknown state, we introduce a new way to locally manipulate the original quantum system: either identify the state successfully or distill some pure entanglement. Remarkably, if many copies are available, we show that any finite set of entangled pure states, whatever orthogonal or not, can be locally distinguished in this way, which further implies that pure entanglement can be deterministically extracted from unknown pure entanglement. These results make it clear why a large class of entangled bipartite quantum operations including unitary operations and measurements that are globally distinguishable can also be locally distinguishable: they can generate pure entanglement consistently.

0 citations0 reviewsNo code linkedOpen access
preprint2009arXiv

Optimal Simulation of a Perfect Entangler

A $2\otimes 2$ unitary operation is called a perfect entangler if it can generate a maximally entangled state from some unentangled input. We study the following question: How many runs of a given two-qubit entangling unitary operation is required to simulate some perfect entangler with one-qubit unitary operations as free resources? We completely solve this problem by presenting an analytical formula for the optimal number of runs of the entangling operation. Our result reveals an entanglement strength of two-qubit unitary operations.

0 citations0 reviewsNo code linkedOpen access
preprint2009arXiv

Reasoning about Cardinal Directions between Extended Objects

Direction relations between extended spatial objects are important commonsense knowledge. Recently, Goyal and Egenhofer proposed a formal model, known as Cardinal Direction Calculus (CDC), for representing direction relations between connected plane regions. CDC is perhaps the most expressive qualitative calculus for directional information, and has attracted increasing interest from areas such as artificial intelligence, geographical information science, and image retrieval. Given a network of CDC constraints, the consistency problem is deciding if the network is realizable by connected regions in the real plane. This paper provides a cubic algorithm for checking consistency of basic CDC constraint networks, and proves that reasoning with CDC is in general an NP-Complete problem. For a consistent network of basic CDC constraints, our algorithm also returns a 'canonical' solution in cubic time. This cubic algorithm is also adapted to cope with cardinal directions between possibly disconnected regions, in which case currently the best algorithm is of time complexity O(n^5).

0 citations0 reviewsNo code linkedOpen access
preprint2009arXiv

The Perfect Distinguishability of Quantum Operations

We provide a feasible necessary and sufficient condition for when an unknown quantum operation (quantum device) secretely selected from a set of known quantum operations can be identified perfectly within a finite number of queries, and thus complete the characterization of the perfect distinguishability of quantum operations. We further design an optimal protocol which can achieve the perfect discrimination between two quantum operations by a minimal number of queries. Interestingly, employing the techniques from the theory of $q$-numerical range we find that an optimal perfect discrimination between two isometries is always achievable without using auxiliary systems or entanglement.

0 citations0 reviewsNo code linkedOpen access
preprint2008arXiv

The LU-LC conjecture is false

The LU-LC conjecture is an important open problem concerning the structure of entanglement of states described in the stabilizer formalism. It states that two local unitary equivalent stabilizer states are also local Clifford equivalent. If this conjecture were true, the local equivalence of stabilizer states would be extremely easy to characterize. Unfortunately, however, based on the recent progress made by Gross and Van den Nest, we find that the conjecture is false.

0 citations0 reviewsNo code linkedOpen access
preprint2007arXiv

Deterministic distributed dense coding with stabilizer states

We consider the possibility of using stabilizer states to perform deterministic dense coding among multiple senders and a single receiver. In the model we studied, the utilized stabilizer state is partitioned into several subsystems and then each subsystem is held by a distinct party. We present a sufficient condition for a stabilizer state to be useful for deterministic distributed dense coding with respect to a given partition plan. The corresponding protocol is also constructed. Furthermore, we propose a method to partially solve a more general problem of finding the set of achievable alphabet sizes for an arbitrary stabilizer state with respect to an arbitrary partition plan. Finally, our work provides a new perspective from the stabilizer formalism to view the standard dense coding protocol and also unifies several previous results in a single framework.

0 citations0 reviewsNo code linkedOpen access
preprint2007arXiv

Local Distinguishability of Multipartite Unitary Operations

We show that any two different unitary operations acting on an arbitrary multipartite quantum system can be perfectly distinguishable by local operations and classical communication when a finite number of runs is allowed. We then directly extend this result into the case when the number of unitary operations to be discriminated is more than two. Intuitively, our result means that the lost identity of a nonlocal (entangled) unitary operation can be recovered locally, without any use of entanglement or joint quantum operations.

0 citations0 reviewsNo code linkedOpen access
preprint2007arXiv

Parameter estimation of quantum channels

The efficiency of parameter estimation of quantum channels is studied in this paper. We introduce the concept of programmable parameters to the theory of estimation. It is found that programmable parameters obey the standard quantum limit strictly; hence no speedup is possible in its estimation. We also construct a class of non-unitary quantum channels whose parameter can be estimated in a way that the standard quantum limit is broken. The study of estimation of general quantum channels also enables an investigation of the effect of noises on quantum estimation.

0 citations0 reviewsNo code linkedOpen access
preprint2007arXiv

Perfect many-to-one teleportation with stabilizer states

We study the possibility of performing perfect teleportation of unknown quantum states from multiple senders to a single receiver with a previously shared stabilizer state. In the model we considered, the utilized stabilizer state is partitioned into several subsystems and then each subsystem is distributed to a distinct party. We present two sufficient conditions for a stabilizer state to achieve a given nonzero teleportation capacity with respect to a given partition plan. The corresponding teleportation protocols are also explicitly given. Interestingly, we find that even mixed stabilizer states are also useful for perfect many-to-one teleportation. Finally, our work provides a new perspective from stabilizer formalism to view the standard teleportation protocol and also suggests a new technique for analyzing teleportation capability of multipartite entangled states.

0 citations0 reviewsNo code linkedOpen access
preprint2007arXiv

Soft constraint abstraction based on semiring homomorphism

The semiring-based constraint satisfaction problems (semiring CSPs), proposed by Bistarelli, Montanari and Rossi \cite{BMR97}, is a very general framework of soft constraints. In this paper we propose an abstraction scheme for soft constraints that uses semiring homomorphism. To find optimal solutions of the concrete problem, the idea is, first working in the abstract problem and finding its optimal solutions, then using them to solve the concrete problem. In particular, we show that a mapping preserves optimal solutions if and only if it is an order-reflecting semiring homomorphism. Moreover, for a semiring homomorphism $α$ and a problem $P$ over $S$, if $t$ is optimal in $α(P)$, then there is an optimal solution $\bar{t}$ of $P$ such that $\bar{t}$ has the same value as $t$ in $α(P)$.

0 citations0 reviewsNo code linkedOpen access
preprint2006arXiv

Retraction and Generalized Extension of Computing with Words

Fuzzy automata, whose input alphabet is a set of numbers or symbols, are a formal model of computing with values. Motivated by Zadeh's paradigm of computing with words rather than numbers, Ying proposed a kind of fuzzy automata, whose input alphabet consists of all fuzzy subsets of a set of symbols, as a formal model of computing with all words. In this paper, we introduce a somewhat general formal model of computing with (some special) words. The new features of the model are that the input alphabet only comprises some (not necessarily all) fuzzy subsets of a set of symbols and the fuzzy transition function can be specified arbitrarily. By employing the methodology of fuzzy control, we establish a retraction principle from computing with words to computing with values for handling crisp inputs and a generalized extension principle from computing with words to computing with all words for handling fuzzy inputs. These principles show that computing with values and computing with all words can be respectively implemented by computing with words. Some algebraic properties of retractions and generalized extensions are addressed as well.

0 citations0 reviewsNo code linkedOpen access
preprint2006arXiv

State-Based Control of Fuzzy Discrete Event Systems

To effectively represent possibility arising from states and dynamics of a system, fuzzy discrete event systems as a generalization of conventional discrete event systems have been introduced recently. Supervisory control theory based on event feedback has been well established for such systems. Noting that the system state description, from the viewpoint of specification, seems more convenient, we investigate the state-based control of fuzzy discrete event systems in this paper. We first present an approach to finding all fuzzy states that are reachable by controlling the system. After introducing the notion of controllability for fuzzy states, we then provide a necessary and sufficient condition for a set of fuzzy states to be controllable. We also find that event-based control and state-based control are not equivalent and further discuss the relationship between them. Finally, we examine the possibility of driving a fuzzy discrete event system under control from a given initial state to a prescribed set of fuzzy states and then keeping it there indefinitely.

0 citations0 reviewsNo code linkedOpen access
preprint2005arXiv

Catalyst-assisted Probabilistic Entanglement Transformation

We are concerned with catalyst-assisted probabilistic entanglement transformations. A necessary and sufficient condition is presented under which there exist partial catalysts that can increase the maximal transforming probability of a given entanglement transformation. We also design an algorithm which leads to an efficient method for finding the most economical partial catalysts with minimal dimension. The mathematical structure of catalyst-assisted probabilistic transformation is carefully investigated.

0 citations0 reviewsNo code linkedOpen access