total 3882took 0.11s

Quantum search algorithm by adiabatic evolution under a priori probabilityDec 15 2004Grover's algorithm is one of the most important quantum algorithms, which performs the task of searching an unsorted database without a priori probability. Recently the adiabatic evolution has been used to design and reproduce quantum algorithms, including ... More

Similarity-Based Supervisory Control of Discrete Event SystemsOct 14 2004Mar 31 2005Due to the appearance of uncontrollable events in discrete event systems, one may wish to replace the behavior leading to the uncontrollability of pre-specified language by some quite similar one. To capture this similarity, we introduce metric to traditional ... More

Quantum Privacy-Preserving PerceptronJul 31 2017With the extensive applications of machine learning, the issue of private or sensitive data in the training examples becomes more and more serious: during the training process, personal information or habits may be disclosed to unexpected persons or organisations, ... More

Quantum Privacy-Preserving Data AnalyticsFeb 14 2017Data analytics (such as association rule mining and decision tree mining) can discover useful statistical knowledge from a big data set. But protecting the privacy of the data provider and the data user in the process of analytics is a serious issue. ... More

An Equivalence of Entanglement-Assisted Transformation and Multiple-Copy Entanglement TransformationApr 07 2004Jan 06 2005We examine the powers of entanglement-assisted transformation and multiple-copy entanglement transformation. First, we find a sufficient condition of when a given catalyst is useful in producing another specific target state. As an application of this ... More

The Perfect Distinguishability of Quantum OperationsAug 03 2009We 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 ... More

Majorization in Quantum Adiabatic AlgorithmsJun 01 2006Sep 01 2010The 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 ... More

Comparability of multipartite entanglementJun 30 2004We prove, in a multipartite setting, that it's always feasible to exactly transform a genuinely $m$-partite entangled state with sufficient many copies to any other $m$-partite state via local quantum operation and classical communication. This result ... More

Another Quantum Lovász Local LemmaOct 27 2010Mar 18 2011We define a natural conceptual framework in which a generalization of the Lov\'{a}sz Local Lemma can be established in quantum probability theory.

Hoare Logic for Quantum ProgramsJun 25 2009Hoare logic is a foundation of axiomatic semantics of classical programs and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical ... More

A Theory of Computation Based on Quantum Logic (I)Mar 29 2004The (meta)logic underlying classical theory of computation is Boolean (two-valued) logic. Quantum logic was proposed by Birkhoff and von Neumann as a logic of quantum mechanics more than sixty years ago. The major difference between Boolean logic and ... More

Quantum Recursion and Second QuantisationMay 17 2014Aug 06 2014This 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 ... More

Identification and Distance Measures of Measurement ApparatusJan 13 2006Apr 05 2006We propose simple schemes that can perfectly identify projective measurement apparatus secretly chosen from a finite set. Entanglements are used in these schemes both to make possible the perfect identification and to improve the efficiency significantly. ... More

Quantum operation, quantum Fourier transform and semi-definite programmingApr 22 2003Dec 25 2003We analyze a class of quantum operations based on a geometrical representation of $d-$level quantum system (or qudit for short). A sufficient and necessary condition of complete positivity, expressed in terms of the quantum Fourier transform, is found ... More

Model Checking Applied to Quantum PhysicsFeb 08 2019Model checking has been successfully applied to verification of computer hardware and software, communication systems and even biological systems. In this paper, we further push the boundary of its applications and show that it can be adapted for applications ... More

Coupling Techniques for Reasoning about Quantum ProgramsJan 16 2019Relational verification of quantum programs has many potential applications in security and other domains. We propose a relational program logic for quantum programs. The interpretation of our logic is based on a quantum analogue of probabilistic couplings. ... More

Reachability Analysis of Quantum Markov Decision ProcessesJun 24 2014Jul 09 2014We 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 ... More

(Un)decidable Problems about Reachability of Quantum SystemsJan 24 2014We 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 ... More

Debugging Quantum Processes Using Monitoring MeasurementsMar 18 2014Since 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, ... More

Universal programmable devices for unambiguous discriminationJun 22 2006We discuss the problem of designing unambiguous programmable discriminators for any $n$ unknown quantum states in an $m$-dimensional Hilbert space. The discriminator is a fixed measurement which has two kinds of input registers: the program registers ... More

Reasoning about Parallel Quantum ProgramsOct 26 2018We initiate the study of parallel quantum programming by defining the operational and denotational semantics of parallel quantum programs. The technical contributions of this paper include: (1) find a series of useful proof rules for reasoning about correctness ... More

Toward automatic verification of quantum cryptographic protocolsJul 19 2015Several 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 ... More

Multipartite unlockable bound entanglement in the stabilizer formalismMar 05 2007May 31 2007We find an interesting relationship between multipartite bound entangled states and the stabilizer formalism. We prove that if a set of commuting operators from the generalized Pauli group on $n$ qudits satisfy certain constraints, then the maximally ... More

Optimal simulation of three-qubit gatesJan 16 2013In 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 ... More

Equivalence Checking of Sequential Quantum CircuitsNov 16 2018We define a formal framework for equivalence checking of sequential quantum circuits. The model we adopted is a quantum state machine, which is a natural quantum generalisation of Mealy machines. A major difficulty in checking quantum circuits (but not ... More

Soft constraint abstraction based on semiring homomorphismMay 05 2007The 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 ... More

Quantum adiabatic evolutions that can't be used to design efficient algorithmsApr 11 2006Apr 12 2006Quantum adiabatic computation is a novel paradigm for the design of quantum algorithms, which is usually used to find the minimum of a classical function. In this paper, we show that if the initial hamiltonian of a quantum adiabatic evolution with a interpolation ... More

A modified quantum adiabatic evolution for the Deutsch-Jozsa problemDec 01 2005Dec 04 2005Deutsch-Jozsa algorithm has been implemented via a quantum adiabatic evolution by S. Das et al. [Phys. Rev. A 65, 062310 (2002)]. This adiabatic algorithm gives rise to a quadratic speed up over classical algorithms. We show that a modified version of ... More

Quantum Büchi AutomataApr 24 2018This paper defines a notion of quantum B\"uchi automaton (QBA for short) with two different acceptance conditions for {\omega}-words: non-disturbing and disturbing. Several pumping lemmas are established for QBAs. The relationship between the {\omega}-languages ... More

$Q|SI\rangle$: A Quantum Programming EnvironmentOct 26 2017This paper describes a quantum programming environment, named $Q|SI\rangle$. It is a platform embedded in the .Net language that supports quantum programming using a quantum extension of the $\mathbf{while}$-language. The framework of the platform includes ... More

Quantum loop programsMay 25 2006Jan 04 2007Loop is a powerful program construct in classical computation, but its power is still not exploited fully in quantum computation. The exploitation of such power definitely requires a deep understanding of the mechanism of quantum loop programs. In this ... More

Ancilla-Assisted Discrimination of Quantum GatesSep 02 2008The intrinsic idea of superdense coding is to find as many gates as possible such that they can be perfectly discriminated. In this paper, we consider a new scheme of discrimination of quantum gates, called ancilla-assisted discrimination, in which a ... More

Unambiguous discrimination among quantum operationsDec 18 2005Apr 24 2006We address the problem of unambiguous discrimination among a given set of quantum operations. The necessary and sufficient condition for them to be unambiguously distinguishable is derived in the cases of single use and multiple uses respectively. For ... More

Reachability and Termination Analysis of Concurrent Quantum ProgramsJun 09 2012We introduce a Markov chain model of concurrent quantum programs. This model is a quantum generalization of Hart, Sharir and Pnueli's probabilistic concurrent programs. Some characterizations of the reachable space, uniformly repeatedly reachable space ... More

Non-Additivity of Minimum Output p-$\mathbf{R\acute{e}nyi}$ EntropyJun 09 2010Dec 24 2012Hastings disproved additivity conjecture for minimum output entropy by using random unitary channels. In this note, we employ his approach to show that minimum output $p-$R\'{e}nyi entropy is non-additive for $p\in(0,p_0)\cup(1-p_0,1)$ where $p_0\approx ... More

Linearity and Quantum Adiabatic TheoremJan 19 2007Feb 17 2007We show that in a quantum adiabatic evolution, even though the adiabatic approximation is valid, the total phase of the final state indicated by the adiabatic theorem may evidently differ from the actual total phase. This invalidates the application of ... More

A relation between fidelity and quantum adiabatic evolutionApr 15 2005Dec 01 2005Recently, some quantum algorithms have been implemented by quantum adiabatic evolutions. In this paper, we discuss the accurate relation between the running time and the distance of the initial state and the final state of a kind of quantum adiabatic ... More

Observability and Decentralized Control of Fuzzy Discrete Event SystemsMay 20 2004Oct 18 2005Fuzzy discrete event systems as a generalization of (crisp) discrete event systems have been introduced in order that it is possible to effectively represent uncertainty, imprecision, and vagueness arising from the dynamic of systems. A fuzzy discrete ... More

Model Checking Quantum Systems --- A SurveyJul 25 2018This article discusses the essential difficulties in developing model-checking techniques for quantum systems that are never present in model checking classical systems. It further reviews some early researches on checking quantum communication protocols ... More

Perfect many-to-one teleportation with stabilizer statesNov 04 2007We 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 ... More

Deterministic distributed dense coding with stabilizer statesOct 24 2007Nov 04 2007We 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 ... More

Realization of positive-operator-valued measures by projective measurements without introducing ancillary dimensionsAug 30 2006Sep 12 2006We propose a scheme that can realize a class of positive-operator-valued measures (POVMs) by performing a sequence of projective measurements on the original system, in the sense that for an arbitrary input state the probability distribution of the measurement ... More

Supervisory Control of Fuzzy Discrete Event SystemsMay 12 2004In order to cope with situations in which a plant's dynamics are not precisely known, we consider the problem of supervisory control for a class of discrete event systems modelled by fuzzy automata. The behavior of such discrete event systems is described ... More

Quantum Privacy-Preserving Data MiningDec 13 2015Jan 14 2016Data 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 ... More

The Existence of Quantum Entanglement CatalystsNov 19 2003Jan 18 2005Without additional resources, it is often impossible to transform one entangled quantum state into another with local quantum operations and classical communication. Jonathan and Plenio [Phys. Rev. Lett. 83, 3566(1999)] presented an interesting example ... More

Model checking quantum Markov chainsMay 10 2012Nov 14 2013Although 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 ... More

Local Distinguishability of Multipartite Unitary OperationsMay 10 2007We 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 ... More

Catalyst-assisted Probabilistic Entanglement TransformationApr 27 2004Mar 04 2005We 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 ... More

Decomposition of Quantum Markov Chains and Zero-error CapacityAug 22 2016Markov chains have been widely applied in information theory and various areas of its applications. Quantum Markov chains are a natural quantum extension of Markov chains. This paper studies irreducibility and periodicity of (discrete time) quantum Markov ... More

Distinguishability of Quantum States by Positive Operator-Valued Measures with Positive Partial TransposeSep 19 2012Apr 01 2014We 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. ... More

Optimal conclusive discrimination of two states can be achieved locallyJul 15 2004This paper constructs a LOCC protocol that achieves the global optimality in conclusive discrimination of any two states with arbitrary a priori probability. This can be interpreted that there is no ``non-locality'' in the conclusive discrimination of ... More

Local Unambiguous Discrimination with Remaining EntanglementDec 28 2009A 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 ... More

Equivalence Checking of Quantum Finite-State MachinesJan 08 2019In 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 ... More

The Structure of Decoherence-free SubsystemsFeb 14 2018Decoherence-free subsystems have been successfully developed as a tool to preserve fragile quantum information against noises. In this letter, we develop a structure theory for decoherence-free subsystems. Based on it, we present an effective algorithm ... More

Super-activating Quantum Memory with EntanglementAug 02 2017Nov 21 2018Noiseless subsystems were proved to be an efficient and faithful approach to preserve fragile information against decoherence in quantum information processing and quantum computation. They were employed to design a general (hybrid) quantum memory cell ... More

Symbolic bisimulation for quantum processesFeb 16 2012Feb 21 2012With 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. ... More

Locally undetermined states, generalized Schmidt decomposition, and an application in distributed computingAug 21 2008Aug 29 2008Multipartite quantum states that cannot be uniquely determined by their reduced states of all proper subsets of the parties exhibit some inherit `high-order' correlation. This paper elaborates this issue by giving necessary and sufficient conditions for ... More

Entanglement-assisted transformation is asymptotically equivalent to multiple-copy transformationDec 10 2004Aug 31 2005We show that two ways of manipulation of quantum entanglement, namely, entanglement-assisted local transformation [D. Jonathan and M. B. Plenio, Phys. Rev. Lett. {\bf 83}, 3566 (1999)] and multiple-copy transformation [S. Bandyopadhyay, V. Roychowdhury, ... More

Local cloning of two product statesJan 17 2005Mar 23 2005Local quantum operations and classical communication (LOCC) put considerable constraints on many quantum information processing tasks such as cloning and discrimination. Surprisingly however, discrimination of any two pure states survives such constraints ... More

When Catalysis is Useful for Probabilistic Entanglement TransformationMar 24 2004Mar 04 2005We determine all $2\times 2$ quantum states that can serve as useful catalysts for a given probabilistic entanglement transformation, in the sense that they can increase the maximal transformation probability. When higher-dimensional catalysts are considered, ... More

Termination of Nondeterministic Quantum ProgramsJan 04 2012We 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 ... More

Four Locally Indistinguishable Ququad-Ququad Orthogonal Maximally Entangled StatesJul 16 2011Jul 15 2012We 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 ... More

Any $2\otimes n$ subspace is locally distinguishableOct 13 2010A 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 ... More

Optimal Simulation of a Perfect EntanglerJul 16 2009Aug 28 2009A $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 ... More

Session Communication and IntegrationOct 08 2012The 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 ... More

Probabilistic Automata for Computing with WordsApr 23 2006Usually, probabilistic automata and probabilistic grammars have crisp symbols as inputs, which can be viewed as the formal models of computing with values. In this paper, we first introduce probabilistic automata and probabilistic grammars for computing ... More

State-Based Control of Fuzzy Discrete Event SystemsSep 30 2005Nov 28 2006To 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 ... More

Retraction and Generalized Extension of Computing with WordsApr 19 2006Nov 28 2006Fuzzy 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 ... More

Alternation in Quantum Programming: From Superposition of Data to Superposition of ProgramsFeb 20 2014We 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 ... More

Partial Recovery of Quantum EntanglementApr 07 2004Feb 09 2007Suppose Alice and Bob try to transform an entangled state shared between them into another one by local operations and classical communications. Then in general a certain amount of entanglement contained in the initial state will decrease in the process ... More

Unambiguous discrimination between quantum mixed statesMar 20 2004Apr 07 2005We prove that the states secretly chosen from a mixed state set can be perfectly discriminated if and only if these states are orthogonal. The sufficient and necessary condition when nonorthogonal quantum mixed states can be unambiguously discriminated ... More

Relation Between Catalyst-assisted Entanglement Transformation and Multiple-copy TransformationDec 12 2003Oct 17 2006We show that in some cases, catalyst-assisted entanglement transformation cannot be implemented by multiple-copy transformation for pure states. This fact, together with the result we obtained in [R. Y. Duan, Y. Feng, X. Li, and M. S. Ying, Phys. Rev. ... More

Optimal universal programmable detectors for unambiguous discriminationDec 04 2005Oct 16 2006We discuss the problem of designing unambiguous programmable discriminators for any n unknown quantum states in an m-dimensional Hilbert space. The discriminator is a fixed measurement that has two kinds of input registers: the program registers and the ... More

Discrimination between pure states and mixed statesNov 11 2006Feb 09 2007In this paper, we discuss the problem of determining whether a quantum system is in a pure state, or in a mixed state. We apply two strategies to settle this problem: the unambiguous discrimination and the maximum confidence discrimination. We also proved ... More

Relational reasoning in the region connection calculusMay 14 2005This paper is mainly concerned with the relation-algebraical aspects of the well-known Region Connection Calculus (RCC). We show that the contact relation algebra (CRA) of certain RCC model is not atomic complete and hence infinite. So in general an extensional ... More

Locally Indistinguishable Subspaces Spanned by Three-Qubit Unextendible Product BasesAug 27 2007Sep 25 2008We study the local distinguishability of general multi-qubit states and show that local projective measurements and classical communication are as powerful as the most general local measurements and classical communication. Remarkably, this indicates ... More

Five Two-Qubit Gates Are Necessary for Implementing Toffoli GateJan 15 2013In 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 ... More

Decomposition of Quantum Markov Chains and Its ApplicationsAug 22 2016Feb 14 2018Markov chains have been widely employed as a fundamental model in the studies of probabilistic and stochastic communicating and concurrent systems. It is well-understood that decomposition techniques play a key role in reachability analysis and model-checking ... More

Quantum Information-Flow Security: Noninterference and Access ControlJan 28 2013Quantum 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 ... More

Defining Quantum Control FlowSep 19 2012A 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 ... More

Bisimulation for quantum processesJul 15 2010Nov 14 2013In 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 ... More

Entanglement Is Not Necessary for Perfect Discrimination between Unitary OperationsJan 22 2006Mar 26 2007We show that a unitary operation (quantum circuit) secretely chosen from a finite set of unitary operations can be determined with certainty by sequentially applying only a finite amount of runs of the unknown circuit. No entanglement or joint quantum ... More

Reachability Probabilities of Quantum Markov ChainsMar 30 2013Jun 07 2013This 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 ... More

Quantum Coupling and Strassen TheoremMar 28 2018We introduce a quantum generalisation of the notion of coupling in probability theory. Several interesting examples and basic properties of quantum couplings are presented. In particular, we prove a quantum extension of Strassen theorem for probabilistic ... More

Quantum Earth mover's distance, No-go Quantum Kantorovich-Rubinstein theorem, and Quantum Marginal ProblemMar 01 2018Mar 14 2019The earth mover's distance is a measure of the distance between two probabilistic measures. It plays a fundamental role in mathematics and computer science. The Kantorovich-Rubinstein theorem provides a formula for the earth mover's distance on the space ... More

Multiple-copy entanglement transformation and entanglement catalysisApr 26 2004Apr 13 2005We prove that any multiple-copy entanglement transformation [S. Bandyopadhyay, V. Roychowdhury, and U. Sen, Phys. Rev. A \textbf{65}, 052315 (2002)] can be implemented by a suitable entanglement-assisted local transformation [D. Jonathan and M. B. Plenio, ... More

Verification of Quantum ProgramsJun 21 2011This 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, ... More

A Theorem Prover for Quantum Hoare Logic and Its ApplicationsJan 15 2016Quantum 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 ... More

Existence of Universal EntanglerApr 11 2007May 11 2007A gate is called entangler if it transforms some (pure) product states to entangled states. A universal entangler is a gate which transforms all product states to entangled states. In practice, a universal entangler is a very powerful device for generating ... More

Quantum Supremacy Circuit Simulation on Sunway TaihuLightApr 13 2018Aug 13 2018With the rapid progress made by industry and academia, quantum computers with dozens of qubits or even larger size are being realized. However, the fidelity of existing quantum computers often sharply decreases as the circuit depth increases. Thus, an ... More

Model-Checking Linear-Time Properties of Quantum SystemsDec 31 2010We 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 ... More

Probabilistic bisimilarities between quantum processesJan 06 2006Nov 14 2013Modeling 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 ... More

Trade-off between multiple-copy transformation and entanglement catalysisDec 01 2003Jul 16 2005We demonstrate that multiple copies of a bipartite entangled pure state may serve as a catalyst for certain entanglement transformations while a single copy cannot. Such a state is termed a "multiple-copy catalyst" for the transformations. A trade-off ... More

The LU-LC conjecture is falseSep 09 2007Jun 30 2008The 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 ... More

An Algebra of Quantum ProcessesJul 03 2007Sep 06 2010We 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 ... More

Distinguishability of Quantum States by Separable OperationsMay 06 2007Oct 08 2007We study the distinguishability of multipartite quantum states by separable operations. We first present a necessary and sufficient condition for a finite set of orthogonal quantum states to be distinguishable by separable operations. An analytical version ... More

Boundary effect of deterministic dense codingJan 20 2006We present a rigorous proof of an interesting boundary effect of deterministic dense coding first observed by Mozes et al. [Phys. Rev. A 71, 012311 (2005)]. Namely, it is shown that $d^2-1$ cannot be the maximal alphabet size of any isometric deterministic ... More

Proof rules for purely quantum programsJul 18 2005Mar 16 2006We apply the notion of quantum predicate proposed by D'Hondt and Panangaden to analyze a purely quantum language fragment which describes the quantum part of a future quantum computer in Knill's architecture. The denotational semantics, weakest precondition ... More

Reasoning about Cardinal Directions between Extended ObjectsSep 01 2009Direction 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. ... More

Distinguishing Arbitrary Multipartite Basis Unambiguously Using Local Operations and Classical CommunicationDec 05 2006Jun 11 2007We show that an arbitrary basis of a multipartite quantum state space consisting of $K$ distant parties such that the $k$th party has local dimension $d_k$ always contains at least $N=\sum_{k=1}^K (d_k-1)+1$ members that are unambiguously distinguishable ... More