UTS site search

# Professor Mingsheng Ying

Distinguished Professor, A/DRsch Ctr Quantum Computat'n & Intelligent Systs
Core Member, QCIS - Quantum Computation and Intelligent Systems

Phone
+61 2 9514 1873
ORCID

## Books

Ying, M. 2016, Foundations of Quantum Programming, Morgan Kaufmann Publishers.
Drawing upon years of experience and research in quantum computing research and using numerous examples and illustrations, Mingsheng Ying has created a very useful reference on quantum programming languages and important tools and ...
Ying, M. 2001, Topology in process calculus : approximate correctness and infinite evolution of concurrent programs, Springer, New York.
Chen, G., Ying, M. & Kai-Yuan, C. 1999, Fuzzy logic and soft computing, Kluwer Academic Publishers, Boston.

## Chapters

Ying, M. 2016, 'Prospects' in Foundations of Quantum Programming, Morgan Kaufmann, pp. 325-336.
Early research on quantum programming focused on the design of quantum programming languages. Several high-level quantum programming languages have been defined in the later 1990s and early 2000s; for example, the first quantum&nbsp;...
Ying, M., Duan, R., Feng, Y. & Ji, Z. 2010, 'Predicate Transformer Semantics of Quantum Programs' in Gay, S. & Mackie, I. (eds), Semantic Techniques in Quantum Computation, Cambridge University Press, Cambridge, pp. 311-360.
This chapter presents a systematic exposition of predicate transformer semantics for quantum programs. It is divided into two parts: The first part reviews the state transformer (forward) semantics of quantum programs according to Selinger&acirc;s suggestion of representing quantum programs by superoperators and elucidates D&acirc;Hondt-Panangaden&acirc;s theory of quantum weakest preconditions in detail. In the second part, we develop a quite complete predicate transformer semantics of quantum programs based on Birkhoff&acirc;von Neumann quantum logic by considering only quantum predicates expressed by projection operators. In particular, the universal coujunctivity and termination law of quantum programs are proved, and Hoare&acirc;s induction rule is established in the quantum setting.
Su, G., Ying, M. & Zhang, C. 2010, 'An ADL-Approach to Specifying and Analyzing Centralized-Mode Architectural Connection' in Babar, M.A. & Gorton, I. (eds), Lecture Notes in Computer Science 6285 - Software Architecture, Springer, Germany, pp. 8-23.
A rigorous paradigm coordinating components is important in the design stage of large-scale software engineering. In this paper we propose a new Architecture Description Language, called ACDL, to represent the centralized-mode architectural connection in which all components are linked by a single connector. Following one usual approach to architectural description, in which component types and components are distinguished, and connectors integrate behaviors of components by specifying their coordination protocols, ACDL describes connectors in such a way that connectors are insensitive to the numbers of attached same-type components. Based on ACDL, we develop analytic techniques to facilitate the system checking of temporal properties of an architecture. In particular, our method shows to what extent one can add, delete and replace components without making the whole system lose desired temporal properties, and improves the system checking in several ways, for example enhancing the use of previous checking results to deal with new checking problems.
Ying, M. 2007, 'Quantum logic and automata theory' in Engesser, K., Gabbay, D.M. & Lehmann, D. (eds), Handbook of Quantum Logic and Quantum Structures, Elsevier, London, UK, pp. 619-754.
An axiomatization of a mathematical theory consists of a system of basic notions as well as a set of axioms about these notions. The mathematical theory is then the set of theorems which can be derived from the axioms. Obviously, one needs a certain logic providing the tools of reasoning in the derivation of these theorems from the axioms. As pointed out by A. Heyting [1963, p. 5], in the early stages of the axiomatic viewpoint, logic was used in an unanalyzed form. In a later stage, in the study of the foundations of mathematics beginning early in the twentieth century, it was realized that a major part of mathematics has to exploit the full power of classical (Boolean) logic [Hatcher, 1982], the strongest in the family of existing logics. For example, group theory is based on first-order logic, and point-set topology is built on a fragment of second-order logic. However, some mathematicians, including the big names of L. E. J. Brouwer, H. Poincare, L. Kronecker and H. Weyl, have taken a constructive position which is in more or less explicit opposition to certain forms of mathematical reasoning used by the majority of the mathematical community. Some of them even endeavoured to establish so-called constructive mathematics, i.e. the part of mathematics that can be rebuilt on constructivist principles. The logic employed in the development of constructive mathematics is intuitionistic logic [Troelstra and van Dalen, 1988], which is genuinely weaker than classical logic.

## Conferences

Feng, Y. & Ying, M. 2015, 'Toward automatic verification of quantum cryptographic protocols', Leibniz International Proceedings in Informatics, LIPIcs, the 26th International Conference on Concurrency Theory (CONCUR'15), pp. 441-455.
&copy; Yuan Feng and Mingsheng Ying; licensed under Creative Commons License CC-BY. 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.
Li, Y. & Ying, M. 2014, '(Un)decidable problems about reachability of quantum systems', Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 482-496.
We study the reachability problem of a quantum system modeled by a quantum automaton, namely, a set of processes each of which is formalized as a quantum unitary transformation. The reachable sets are chosen to be boolean combinations of (closed) subspaces of the state Hilbert 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. &copy; 2014 Springer-Verlag.
Feng, Y., Yu, N. & Ying, M. 2013, 'Reachability Analysis of Recursive Quantum Markov Chains', Lecture Notes in Computer Science, the 38th Int. Symp. on Mathematical Foundations of Computer Science (MFCS'13), Springer, IST Austria, pp. 385-396.
We introduce the notion of recursive quantum Markov chain (RQMC) for analysing recursive quantum programs with procedure calls. RQMCs are natural extension of Etessami and Yannakakiss recursive Markov chains where the probabilities along transitions are replaced by completely positive and trace-nonincreasing super-operators on a state Hilbert space of a quantum system. We study the reachability problem for RQMCs and establish a reduction from it to computing the least solution of a system of polynomial equations in the semiring of super-operators. It is shown that for an important subclass of RQMCs, namely linear RQMCs, the reachability problem can be solved in polynomial time. For general case, technique of Newtonian program analysis recently developed by Esparza, Kiefer and Luttenberger is employed to approximate reachability super-operators. A polynomial time algorithm that computes the support subspaces of the reachability super-operators in general case is also proposed.
Ying, M., Feng, Y. & Yu, N. 2013, 'Quantum information-flow security - noninterference and access control', Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium, IEEE Computer Security Foundations Symposium, IEEE Computer Society, Tulane University, New Orleans, Louisiana, USA, pp. 130-144.
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. Due 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.
Ying, S., Feng, Y., Yu, N. & Ying, M. 2013, 'Reachability probabilities of quantum Markov chains', Lecture Notes in Computer Science, the 24th International Conference on Concurrency Theory (CONCUR'13), Springer, University of Buenos Aires, Argentina, pp. 334-348.
This paper studies three kinds of long-term behaviour, 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.
Su, G., Ying, M. & Zhang, C. 2012, 'Semantic Analysis of Component-aspect Dynamism for Connector-based Architecture Styles', 2012 Joint Working Conference on Software Architecture & 6th European Conference on Software Architecture, Joint Working Conference on Software Architecture & 6th European Conference on Software Architecture, IEEE Computer Society, Helsinki (Finland), pp. 151-160.
Architecture Description Languages usually specify software architectures in the levels of types and instances. Components instantiate component types by parameterization and type conformance. Behavioral analysis of dynamic architectures needs to deal with the uncertainty of actual configurations of components, even if the type-level architectural descriptions are explicitly provided. This paper addresses this verification difficulty for connector-based architecture styles, in which all communication channels of a system are between components and a connector. The contribution of this paper is two-fold: (1) We propose a process-algebraic model, in which the main architectural concepts (such as component type and component conformance) and several fundamental architectural properties (i.e. deadlock-freedom, non-starvation, conservation, and completeness) are formulated. (2)We demonstrate that the state space of verification of these properties can be reduced from the entire universe of possible configurations to specific configurations that are fixed according to the typelevel architectural descriptions.
Yu, N. & Ying, M. 2012, 'Reachability and Termination Analysis of Concurrent Quantum Programs.', CONCUR, Springer, pp. 69-83.
Feng, Y., Duan, R. & Ying, M. 2011, 'Bisimulation for Quantum Processes', Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming language, annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, Austin, Texas, USA, pp. 523-534.
Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the other hand, quantum protocol designers may commit much more faults than classical protocol designers since human intuition is much better adapted to the classical world than the quantum world. To offer formal techniques for modeling and verification of quantum protocols, several quantum extensions of process algebra have been proposed. One of the most serious issues in quantum process algebra is to discover a quantum generalization of the notion of bisimulation, which lies in a central position in process algebra, preserved by parallel composition in the presence of quantum entanglement, which has no counterpart in classical computation. Quite a few versions of bisimulation have been defined for quantum processes in the literature, but in the best case they are only proved to be preserved by parallel composition of purely quantum processes where no classical communications are involved. Many quantum cryptographic protocols, however, employ the LOCC (Local Operations and Classical Communications) scheme, where classical communications must be explicitly specified. So, a notion of bisimulation preserved by parallel composition in the circumstance of both classical and quantum communications is crucial for process algebra approach to verification of quantum cryptographic protocols. In this paper we introduce a novel notion of 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.
Feng, Y., Duan, R., Ying, M. & ACM 2011, 'Bisimulation for Quantum Processes', POPL 11: PROCEEDINGS OF THE 38TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, pp. 523-534.
Zhang, H., Zhang, Y., Ying, M. & Zhou, Y. 2011, 'Translating first-order theories into logic programs', IJCAI International Joint Conference on Artificial Intelligence, pp. 1126-1131.
This paper focuses on computing first-order theories under either stable model semantics or circumscription. A reduction from first-order theories to logic programs under stable model semantics over finite structures is proposed, and an embedding of circumscription into stable model semantics is also given. Having such reduction and embedding, reasoning problems represented by first-order theories under these two semantics can then be handled by using existing answer set solvers. The effectiveness of this approach in computing hard problems beyond NP is demonstrated by some experiments.
Zhang, H. & Ying, M. 2010, 'Decidable fragments of first-order language under stable model semantics and circumscription', 24th AAAI Conference on Artificial Intelligence 2010, Conference on Artificial Intelligence, The AAAI Press, Atlanta, Georgia, pp. 375-380.
The stable model semantics was recently generalized by Ferraris, Lee and Lifschitz to the full first-order language with a syntax translation approach that is very similar to McCarthy's circumscription. In this paper, we investigate the decidability and
Ying, M. 2010, 'Foundations of quantum programming', Programming Languages and Systems 8th Asian Symposium, APLAS 2010, Programming Languages and Systems, Springer-Verlag, Shanghai, China, pp. 16-20.
Progress in the techniques of quantum devices has made people widely believe that large-scale and functional quantum computers will be eventually built. By then, super-powered quantum computer will solve many problems affecting economic and social life t
Zhang, X., Liu, W., Li, S. & Ying, M. 2008, 'Reasoning with Cardinal Directions: An Efficient Algorithm', Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence vol 1, National Conference of the American Association for Artificial Intelligence, AAAI Press, Chicago, Illinois, USA, pp. 387-392.
Direction relations between extended spatial objects are important commonsense knowledge. Recently, Goyal and Egenhofer proposed a formal model, called 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. As one byproduct, we also show that any consistent network of CDC constraints has a canonical realization in digital plane. The cubic algorithm can also been adapted to cope with disconnected regions, in which case the current best algorithm is of time complexity O(n5).
Xia, L., Lang, J. & Ying, M. 2007, 'Sequential voting rules and multiple elections paradoxes', Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2007, pp. 279-288.
Multiple election paradoxes arise when voting separately on each issue from a set of related issues results in an obviously undesirable outcome. Several authors have argued that a sufficient condition for avoiding multiple election paradoxes is the assumption that voters have separable preferences. We show that this extremely demanding restriction can be relaxed into the much more reasonable one: there exists a linear order x1 > ... > x p on the set of issues such that for each voter, every issue x i is preferentially independent of xi+1, ..., x p given x1, ..., xi-1. This leads us to define a family of sequential voting rules, defined as the sequential composition of local voting rules. These rules relate to the setting of conditional preference networks (CP-nets) recently developed in the Artificial Intelligence literature. We study in detail how these sequential rules inherit, or do not inherit, the properties of their local components. We focus on the case of multiple referenda, corresponding to multiple elections with binary issues.
Xia, L., Lang, J. & Ying, M. 2007, 'Strongly decomposable voting rules on multiattribute domains', Proceedings of the National Conference on Artificial Intelligence, pp. 776-781.
Sequential composition of voting rules, by making use of structural properties of the voters' preferences, provide computationally economical ways for making a common decision over a Cartesian product of finite local domains. A sequential composition is usually defined on a set of legal profiles following a fixed order. In this paper, we generalize this by order-independent sequential composition and strong decomposable, which are independent of the chosen order. We study to which extent some usual properties of voting rules transfer from the local rules to their order-independent sequential composition. Then, to capture the idea that a voting rule is neutral or decomposable on a slightly smaller domain, we define nearly neutral, nearly decomposable rules for both sequential composition and order-independent sequential composition, which leads us to defining and studying decomposable permutations. We prove that any sequential composition of neutral local rules and any order-independent sequential composition of neutral local rules satisfying a necessary condition are nearly neutral. Copyright &copy; 2007, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
Ying, M. 2009, 'A theory of computation based on quantum logic', 2005 IEEE International Conference On Granular Computing, IEEE International Conference on Granular Computing, IEEE, Beijing, China, pp. 91-91.
Summary form only given. The (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. It is currently understood as a logic whose truth values are taken from an orthomodular lattice. The major difference between Boolean logic and quantum logic is that the latter does not enjoy distributivity in general. The rapid development of quantum computation in recent years stimulates us to establish a theory of computation based on quantum logic. The present paper is the first step toward such a new theory and it focuses on the simplest models of computation, namely finite automata. We introduce the notion of orthomodular lattice-valued (quantum) automaton. The Kleene theorem about equivalence of regular expressions and finite automata is generalized into quantum logic. We also present a pumping lemma for orthomodular lattice-valued regular languages.
Ying, M. & Wirsing, M. 2000, 'Approximate bisimilarity', Algebraic Methodology and Software Technology, Algebraic Methodology and Software Technology, Springer-Verlag Berlin, Iowa City, Iowa, pp. 309-322.
We introduce a notion of approximate bisimilarity in order to be able to reason about the approximate equivalence of processes. Approximate bisimilarity is based on the notion of bisimulation index for labelled transition systems. We establish some basic properties of bisimulation indexes and give a Hennessy-Milner logical characterization of approximate bisimilarity. As an application we show how to describe approximate correctness of real time systems by giving an example in real time ACP.
Ying, M. 1997, 'Topology in lambda calculus (I)', New Technologies On Computer Software, World Publishing Corporation, Beijing, pp. 1-5.
Ying, M. & Bouchon-Meunier, B. 1996, 'Quantifiers, modifiers and qualifiers in fuzzy logic', Soft Computing In Intelligent Systems And Information Processing, IEEE, Kenting, Taiwan, pp. 490-495.
In this paper, we propose a formalization of fuzzy logic and obtain some interesting results on fuzzy quantifiers, modifiers and qualifiers in this setting.
Ying, M. 1988, 'On zadeh's method for interpreting linguistically quantified proposition.', Proceedings of The International Symposium on Multiple-Valued Logic, pp. 248-252.
The author establishes an interesting result on multiquantified propositions. He then gives a novel method for interpreting linguistically quantified propositions with nearness measures.
Ying, M.S. 1986, 'FIRST ORDER FUZZY PREDICATE LOGIC (I).', Proceedings of The International Symposium on Multiple-Valued Logic, pp. 242-247.
Some tools for analyzing fuzzy measures (Sugeno's integrals, etc. ) are introduced into the semantics of first-order predicate logic to explain the concept of fuzzy quantifiers. The truth value of a fuzzy quantification proposition is represented by Sugeno's integral. With this framework, the concepts of formation rules, fuzzy valuations, and fuzzy validity are discussed.

## Journal articles

Liu, T., Li, Y., Wang, S., Ying, M. & Zhan, N. 2016, 'A Theorem Prover for Quantum Hoare Logic and Its Applications.', CoRR, vol. abs/1601.03835.
Yu, N. & Ying, M. 2015, 'Optimal simulation of Deutsch gates and the Fredkin gate', PHYSICAL REVIEW A, vol. 91, no. 3.
Ying, S., Ying, M. & Feng, Y. 2015, 'Quantum Privacy-Preserving Data Mining.', CoRR, vol. abs/1512.04009.
Feng, Y., Deng, Y. & Ying, M. 2014, 'Symbolic bisimulation for quantum processes', ACM Transactions on Computational Logic (TOCL), vol. 15, pp. 14-14.
Li, Y. & Ying, M. 2014, 'Debugging quantum processes using monitoring measurements', Physical Review A, vol. 89.
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.
Li, Y., Yu, N. & Ying, M. 2014, 'Termination of nondeterministic quantum programs', Acta Informatica, vol. 51, pp. 1-24.
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, which formalize the quantum mechanical behaviors of the machine. An execution of a nondeterministic quantum program is modeled by a sequence of actions of individual processes, and at each step of an execution a process is chosen nondeterministically to perform the next action. This execution model formalize the users behavior of calling the processes in the classical world. Applying the model to a quantum walk as an instance of physically realizable systems, we describe an execution step by step. 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. 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.
Yu, N., Duan, R. & Ying, M. 2014, 'Distinguishability of Quantum States by Positive Operator-Valued Measures with Positive Partial Transpose', IEEE Transactions on Information Theory, vol. 60, no. 4, pp. 2069-2079.
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})$.
Ying, M., Li, Y., Yu, N. & Feng, Y. 2014, 'Model-Checking Linear-Time Properties of Quantum Systems', ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, vol. 15, no. 3.
Ying, M., Yu, N. & Feng, Y. 2014, 'Alternation in Quantum Programming: From Superposition of Data to Superposition of Programs.', CoRR, vol. abs/1402.5172.
Ying, S. & Ying, M. 2014, 'Reachability Analysis of Quantum Markov Decision Processes.', CoRR, vol. abs/1406.6146.
Ying, M. 2014, 'Quantum Recursion and Second Quantisation: Basic Ideas and Examples.', CoRR, vol. abs/1405.4443.
Feng, Y., Yu, N. & Ying, M. 2013, 'Model Checking Quantum Markov Chains', Journal of Computer and System Sciences, vol. 79, no. 7, pp. 1181-1198.
Although security of quantum cryptography is provable based on principles of quantum mechanics, it can be compromised by flaws in the design of quantum protocols. So, it is indispensable to develop techniques for verifying and debugging quantum cryptogra
Ying, M., Yu, N., Feng, Y. & Duan, R. 2013, 'Verification of quantum programs', Science Of Computer Programming, vol. 78, no. 9, pp. 1679-1700.
This paper develops verification methodology for quantum programs, and the contribution of the paper is two-fold. Sharir, Pnueli and Hart [M. Sharir, A. Pnueli, S. Hart, Verification of probabilistic programs, SIAM Journal of Computing 13 (1984) 292314] 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 to 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 SharirPnueliHart method can be elegantly generalized to quantum programs by exploiting the Schr&ouml;dingerHeisenberg duality between quantum states and observables. In particular, a completeness theorem for the SharirPnueliHart verification method of quantum programs is established.
Ying, S. & Ying, M. 2013, 'Removing Measurements From Quantum Walks', Physical Review A, vol. 87, no. 1, pp. 1-9.
Quantum walks are very useful tools in designing quantum algorithms. Amplitude amplification is a key technique to increase the success probability of a quantum-walk-based algorithm, and it is quadratically faster than classical probabilistic amplification. However, amplitude amplification only applies to quantum walks with one-shot hitting time, where no measurements except a final one are performed, and not to quantum walks with concurrent hitting time, where measurements happen or absorbing boundaries exist at each step. In this paper, we propose a procedure to modify quantum walks with concurrent hitting time by removing measurements from them. This procedure enables us to use amplitude amplification to design algorithms based on the modified quantum walks which are faster than those based on the original walks with a concurrent hitting time and more robust than those based on the corresponding walks with a one-shot hitting time.
Cao, Y., Xia, L. & Ying, M. 2013, 'Probabilistic Automata for Computing with Words', Journal of Computer and System Sciences, vol. 79, no. 1, pp. 152-172.
Usually, 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 ?rst introduce probabilistic automata and probabilistic grammars for computing with (some special) words, where the words are interpreted as probabilistic distributions or possibility distributions over a set of crisp symbols. By probabilistic conditioning, we then 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 arbitrary inputs. These principles show that computing with values and computing with all words can be respectively implemented by computing with some special words. To compare the transition probabilities of two near inputs, we also examine some analytical properties of the transition probability functions of generalized extensions. Moreover, the retractions and the generalized extensions are shown to be equivalence-preserving. Finally, we clarify some relationships among the retractions, the generalized extensions, and the extensions studied by Qiu and Wang.
Yu, N., Duan, R. & Ying, M. 2013, 'Five two-qubit gates are necessary for implementing the Toffoli gate', PHYSICAL REVIEW A, vol. 88, no. 1.
Ying, M., Feng, Y. & Yu, N. 2013, 'Quantum Information-Flow Security: Noninterference and Access Control', CoRR, vol. abs/1301.6804.
Ying, M., Feng, Y., Duan, R., Li, Y. & Yu, N. 2012, 'Quantum Programming: From Theories To Implementations', Chinese Science Bulletin, vol. 57, no. 16, pp. 1903-1909.
This paper surveys the new field of programming methodology and techniques for future quantum computers, including design of sequential and concurrent quantum programming languages, their semantics and implementations. Several verification methods for qu
Feng, Y., Duan, R. & Ying, M. 2012, 'Bisimulation For Quantum Processes', ACM Transactions pn Programming Language and Systems (TOPLAS), vol. 34, no. 4, pp. 1-43.
Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the oth
Zhou, C. & Ying, M. 2012, 'Approximating Markov processes through filtration', Theoretical Computer Science, vol. 446, pp. 75-97.
In this paper, we define a probabilistic version of filtration and use it to provide a finite approximation of Markov processes. In order to measure the approximation, we employ probability logic to construct the final Markov process and define a metric on the set of Markov processes through this logic. Moreover, we show that the set endowed with this metric is a Polish space. Finally we point to some questions connecting approximation to uniformity and approximate bisimilarity as topics for future research.
Yu, N. & Ying, M. 2012, 'Reachability and Termination Analysis of Concurrent Quantum Programs', Lecture Notes in Computer Science, vol. 7454, pp. 69-83.
We introduce a Markov chain model of concurrent quantum programs. This model is a quantum generalization of Hart, Sharir and Pnuelis probabilistic concurrent programs. Some characterizations of the reachable space, uniformly repeatedly reachable space and termination of a concurrent quantum program are derived by the analysis of their mathematical structures. Based on these characterizations, algorithms for computing the reachable space and uniformly repeatedly reachable space and for deciding the termination are given.
Yu, N., Duan, R. & Ying, M. 2012, 'Four Locally Indistinguishable Ququad-Ququad Orthogonal Maximally Entangled States', PHYSICAL REVIEW LETTERS, vol. 109, no. 2.
Feng, Y., Deng, Y. & Ying, M. 2012, 'Symbolic bisimulation for quantum processes', CoRR, vol. abs/1202.3484.
Ying, M., Yu, N. & Feng, Y. 2012, 'Defining Quantum Control Flow', CoRR, vol. abs/1209.4379.
Su, G., Ying, M. & Zhang, C. 2012, 'Session Communication and Integration', CoRR, vol. abs/1210.2125.
Ying, M. & Feng, Y. 2011, 'A Flowchart Language For Quantum Programming', IEEE Transactions On Software Engineering, vol. 37, no. 4, pp. 466-485.
Several high-level quantum programming languages have been proposed in the previous research. In this paper, we define a low-level flowchart language for quantum programming, which can be used in implementation of high-level quantum languages and in desi
Ying, M. 2011, 'Floyd-hoare Logic For Quantum Programs', ACM Transactions pn Programming Language and Systems (TOPLAS), vol. 33, no. 6, pp. 1-49.
Floyd-Hoare 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
Yu, N., Duan, R. & Ying, M. 2011, 'Any 2 Circle Times N Subspace Is Locally Distinguishable', Physical Review A, vol. 84, no. 1, pp. 1-3.
A subspace of a multipartite Hilbert space is said to be locally indistinguishable if any orthonormal basis of this subspace cannot be perfectly distinguished by local operations and classical communication. Previously it was shown that any m . n bipartite system with 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 in negative by showing that any 2 . n bipartite subspace contains a basis that is locally distinguishable. As an interesting application, we show that any quantum channel with two Kraus operators has optimal environment-assisted classical capacity.
Feng, Y., Duan, R. & Ying, M. 2011, 'Bisimulation for Quantum Processes', ACM SIGPLAN NOTICES, vol. 46, no. 1, pp. 523-534.
Ji, Z., Chen, J., Wei, Z. & Ying, M. 2010, 'The LU-LC conjecture is false', Quantum Information and Computation, vol. 10, no. 1, pp. 97-108.
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.
Li, Y., Duan, R. & Ying, M. 2010, 'Local Unambiguous Discrimination With Remaining Entanglement', Physical Review A, vol. 82, no. 3, pp. 1-6.
A bipartite state, which is secretly chosen from a finite set of known entangled pure states, cannot immediately be useful in standard quantum information processing tasks. To effectively make use of the entanglement contained in this unknown state, we i
Yu, N., Duan, R. & Ying, M. 2010, 'Optimal Simulation Of A Perfect Entangler', Physical Review A, vol. 81, no. 3, pp. 1-4.
A2 circle times 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 are required to
Duan, R., Xin, Y. & Ying, M. 2010, 'Locally Indistinguishable Subspaces Spanned By Three-Qubit Unextendible Product Bases', Physical Review A, vol. 81, no. 3, pp. 1-10.
We study the local distinguishability of general multiqubit 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 that
Ying, M. 2010, 'Quantum Computation, Quantum Theory And AI', Artificial Intelligence Journal, vol. 174, no. 2, pp. 162-176.
The main purpose of this paper is to examine some (potential) applications of quantum computation in AI and to review the interplay between quantum theory and AI. For the readers who are not familiar with quantum computation, a brief introduction to it i
Liu, W., Zhang, X., Li, S. & Ying, M. 2010, 'Reasoning about Cardinal Directions between Extended Objects', Artificial Intelligence Journal, vol. 174, no. 12-13, pp. 951-983.
Direction relations between extended spatial objects are important commonsense knowledge. Recently, Goyal and Egenhofer proposed a relation model, known as the cardinal direction calculus (CDC), for representing direction relations between connected plane regions. The 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 the consistency of complete networks of basic CDC constraints, and proves that reasoning with the CDC is in general an NP-complete problem. For a consistent complete network of basic CDC constraints, our algorithm returns a &acirc;canonical&acirc; solution in cubic time. This cubic algorithm is also adapted to check the consistency of complete networks of basic cardinal constraints between possibly disconnected regions.
Ying, M. & Feng, Y. 2010, 'Quantum loop programs', Acta Informatica, vol. 47, no. 4, pp. 221-250.
Loop 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 paper, we introduce a general scheme of quantum loops and describe its computational process. The function computed by a quantum loop is defined, and a denotational semantics and a weakest precondition semantics of a quantum loop are given. The notions of termination and almost termination are proposed for quantum loops. This paper only consider the case of finite-dimensional state spaces. Necessary and sufficient conditions for termination and almost termination of a general quantum loop on any mixed input state are presented. A quantum loop is said to be (almost) terminating if it (almost) terminates on any input state. We show that a quantum loop is almost terminating if and only if it is uniformly almost terminating. It is observed that a small disturbance either on the unitary transformation in the loop body or on the measurement in the loop guard can make any quantum loop (almost) terminating, provided that some dimension restriction is satisfied. Moreover, a representation of the function computed by a quantum loop is given in terms of finite summations of matrices. To illustrate the notions and results obtained in this paper, two simple classes of quantum loop programs, one qubit quantum loops, and two qubit quantum loops defined by controlled gates, are carefully examined, and to show their expressive power, quantum loops are applied in describing quantum walks.
Chen, J. & Ying, M. 2010, 'Ancilla-assisted discrimination of quantum gates', Quantum Information and Computation, vol. 10, no. 1-2, pp. 160-177.
The 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 basic scheme of discrimination of quantum gates, called ancilla-assisted discrimination, in which a set of quantum gates on a d-dimensional system are perfectly discriminated with assistance from an r-dimensional ancilla system. The main contribution of the present paper is two-fold: (1) The number of quantum gates that can be discriminated in this scheme is evaluated. We prove that any rd + 1 quantum gates cannot be perfectly discriminated with assistance from the ancilla, and there exist rd quantum gates which can be perfectly discriminated with assistance from the ancilla. (2) The dimensionality of the minimal ancilla system is estimated. We prove that there exists a constant positive number c such that for any k cr quantum gates, if they are d-assisted discriminable, then they are also r-assisted discriminable, and there are cr (c > c) different quantum gates which can be discriminated with a d-dimensional ancilla, but they cannot be discriminated if the ancilla is reduced to an r-dimensional system. Thus, the order O(r) of the number of quantum gates that can be discriminated with assistance from an r-dimensional ancilla is optimal. The results reported in this paper represent a preliminary step toward understanding the role ancilla system plays in discrimination of quantum gates as well as the power and limit of superdense coding. &copy; Rinton Press.
Zhengfeng, J.I., Chen, J., Wei, Z. & Ying, M. 2010, 'The LU-LC conjecture is false', Quantum Information and Computation, vol. 10, no. 1-2, pp. 97-108.
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. &copy; Rinton Press.
Duan, R., Feng, Y., Xin, Y. & Ying, M. 2009, 'Distinguishability of Quantum States by Separable Operations', IEEE Transactions On Information Theory, vol. 55, no. 3, pp. 1320-1330.
In this paper, we 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 of this condition is derived for the case of (D - 1) pure states, where D is the total dimension of the state space under consideration. A number of interesting consequences of this result are then carefully investigated. Remarkably, we show there exists a large class of 2 circle times 2 separable operations not being realizable by local operations and classical communication. Before our work, only a class of 3 circle times 3 nonlocal separable operations was known [Bennett et al, Phys. Rev. A 59, 1070 (1999)]. We also show that any basis of the orthogonal complement of a multipartite pure state is indistinguishable by separable operations if and only if this state cannot be a superposition of one or two orthogonal product states, i.e., has an orthogonal Schmidt number not less than three, thus generalize the recent work about indistinguishable bipartite subspaces [Watrous, Phys. Rev. Lett. 95, 080505 (2005)]. Notably, we obtain an explicit construction of indistinguishable subspaces of dimension 7 (or 6) by considering a composite quantum system consisting of two qutrits (resp., three qubits), which is slightly better than the previously known indistinguishable bipartite subspace with dimension 8.
Ying, M., Feng, Y., Duan, R. & Ji, Z. 2009, 'An Algebra Of Quantum Processes', Acm Transactions On Computational Logic, vol. 10, no. 3, pp. 1-36.
We introduce an algebra qCCS of pure quantum processes in which communications by moving quantum states physically are allowed and computations are modeled by super-operators, but no classical data is explicitly involved. An operational semantics of qCCS is presented in terms of (nonprobabilistic) 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.
Ying, M. & Feng, Y. 2009, 'An Algebraic Language For Distributed Quantum Computing', IEEE Transactions On Computers, vol. 58, no. 6, pp. 728-743.
A classical circuit can be represented by a circuit graph or equivalently by a Boolean expression. The advantage of a circuit graph is that it can help us to obtain an intuitive understanding of the circuit under consideration, whereas the advantage of a Boolean expression is that it is suited to various algebraic manipulations. In the literature, however, quantum circuits are mainly drawn as circuit graphs, and a formal language for quantum circuits that has a function similar to that of Boolean expressions for classical circuits is still missing. Certainly, quantum circuit graphs will become unmanageable when complicated quantum computing problems are encountered, and in particular, when they have to be solved by employing the distributed paradigm where complex quantum communication networks are involved. In this paper, we design an algebraic language for formally specifying quantum circuits in distributed quantum computing. Using this language, quantum circuits can be represented in a convenient and compact way, similar to the way in which we use Boolean expressions in dealing with classical circuits. Moreover, some fundamental algebraic laws for quantum circuits expressed in this language are established. These laws form a basis of rigorously reasoning about distributed quantum computing and quantum communication protocols.
Chen, G., Ying, M. & Liu, Y. 2009, 'Dealing With Uncertainty And Fuzziness In Intelligent Systems', International Journal of Intelligent Systems, vol. 24, no. 3, pp. 223-225.
NA
Feng, Y., Duan, R. & Ying, M. 2009, 'Locally undetermined states, generalized Schmidt decomposition, and application in distributed computing', Quantum Information and Computation, vol. 9, no. 11, pp. 997-1012.
Multipartite 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 a pure multipartite state to be locally undetermined, and moreover, characterizing precisely all the pure states sharing the same set of reduced states with it. Interestingly, local determinability of pure states is closely related to a generalized notion of Schmidt decomposition. Furthermore, we find that locally undetermined states have some applications to the well-known consensus problem in distributed computation. To be specific, given some physically separated agents, when communication between them, either classical or quantum, is unreliable and they are not allowed to use local ancillary quantum systems, then there exists a totally correct and completely fault-tolerant protocol for them to reach a consensus if and only if they share a priori a locally undetermined quantum state
Duan, R., Feng, Y. & Ying, M. 2009, 'Perfect Distinguishability of Quantum Operations', PHYSICAL REVIEW LETTERS, vol. 103, no. 21.
Ying, M., Feng, Y., Duan, R. & Ji, Z. 2009, 'An algebra of quantum processes', ACM Transactions on Computational Logic, vol. 10, no. 3, pp. 1-36.
Feng, Y., Duan, R. & Ying, M. 2009, 'Locally undetermined states, generalized schmidt decomposition, and application in deistributed comuting', Quantum Information and Computation, vol. 9, no. 11-12, pp. 0997-1012.
Multipartite 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 a pure multipartite state to be locally undetermined, and moreover, characterizing precisely all the pure states sharing the same set of reduced states with it. Interestingly, local determinability of pure states is closely related to a generalized notion of Schmidt decomposition. Furthermore, we find that locally undetermined states have some applications to the well-known consensus problem in distributed computing. To be specific, given some physically separated agents, when communication between them, either classical or quantum, is unreliable, then there exists a totally correct and completely fault-tolerant protocol for them to reach a consensus if and only if they share a priori a locally undetermined quantum state. &copy; Rinton Press.
Ji, Z., Wang, G., Duan, R., Feng, Y. & Ying, M. 2008, 'Parameter Estimation of Quantum Channels', IEEE Transactions On Information Theory, vol. 54, no. 11, pp. 5172-5185.
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 nonunitary 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.
Li, S. & Ying, M. 2008, 'Soft constraint abstraction based on semiring homomorphism', Theoretical Computer Science, vol. 403, no. 2-3, pp. 192-201.
The semiring-based constraint satisfaction problems (semiring CSPs), proposed by Bistarelli, Montanari and Rossi [S. Bistarelli, U. Montanari, F. Rossi, Semiring-based constraints solving and optimization, Journal of the ACM 44 (2) (1997) 201236], 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, we first work in the abstract problem and find its optimal solutions, and then use 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 View the MathML source of P such that View the MathML source has the same value as t in ?(P).
Wang, G. & Ying, M. 2008, 'Deterministic Distributed Dense Coding With Stabilizer States', Physical Review A, vol. 77, no. 3, pp. 1-10.
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 subsyst
Chen, J.F., Duan, R., Ji, Z., Ying, M. & Yu, J.X. 2008, 'Existence Of Universal Entangler', Journal of Mathematical Physics, vol. 49, no. 1, pp. 1-7.
A gate is called an 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 gener
Duan, R., Feng, Y. & Ying, M. 2008, 'Local Distinguishability Of Multipartite Unitary Operations', Physical Review Letters, vol. 100, no. 2, pp. 1-4.
We show that any two different unitary operations acting on an arbitrary multipartite quantum system can be perfectly distinguished by local operations and classical communication when a finite number of runs is allowed. Intuitively, this result indicate
Wang, G. & Ying, M. 2008, 'Perfect Many-To-One Teleportation With Stabilizer States', Physical Review A, vol. 77, no. 3, pp. 1-12.
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 sev
Chen, J. & Ying, M. 2008, 'Ancilla-Assisted Discrimination Of Quantum Gates', Quantum Information and Computation, vol. 10, no. 1-Feb, pp. 160-177.
The 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 basic scheme of discrimination of quantum gates, called ancilla-assisted discrimination, in which a s
Chen, J. & Ying, M. 2008, 'Ancilla-Assisted Discrimination Of Quantum Gates', Quantum Information and Computation, vol. 10, no. 1-Feb, pp. 160-177.
The 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 basic scheme of discrimination of quantum gates, called ancilla-assisted discrimination, in which a s
Ying, M., Chen, J.F., Feng, Y. & Duan, R. 2007, 'Commutativity Of Quantum Weakest Preconditions', Information Processing Letters, vol. 104, no. 4, pp. 152-158.
The notion of quantum weakest precondition was introduced by D'Hondt and P. Panangaden [E. D'Hondt, P. Panangaden, Quantum weakest preconditions, Mathematical Structures in Computer Science 16 (2006) 429-451], and they presented a representation of weake
Zhang, C., Wang, G. & Ying, M. 2007, 'Discrimination Between Pure States And Mixed States', Physical Review A, vol. 75, no. 6, pp. 1-6.
In 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 prove that
Duan, R., Feng, Y., Ji, Z. & Ying, M. 2007, 'Distinguishing Arbitrary Multipartite Basis Unambiguously Using Local Operations And Classical Communication', Physical Review Letters, vol. 98, no. 23, pp. 1-4.
We show that an arbitrary basis of a multipartite quantum state space consisting of K distant parties such that the kth party has local dimension d(k) always contains at least N=Sigma(K)(k=1)(d(k)-1)+1 members that are unambiguously distinguishable using
Duan, R., Feng, Y. & Ying, M. 2007, 'Entanglement Is Not Necessary For Perfect Discrimination Between Unitary Operations', Physical Review Letters, vol. 98, no. 10, pp. 1-4.
We show that a unitary operation (quantum circuit) secretly 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 ope
Liu, Y., Ying, M. & Chen, G. 2007, 'On Fundamentals Of Fuzzy Logic And Soft Computing And Some Applications', Fuzzy Sets and Systems, vol. 158, no. 9, pp. 927-928.
NA
Feng, Y., Duan, R., Ji, Z. & Ying, M. 2007, 'Probabilistic Bisimulations For Quantum Processes', Information And Computation, vol. 205, no. 11, pp. 1608-1639.
Modeling and reasoning about concurrent quantum systems is very important for both distributed quantum computing and quantum protocol verification. As a consequence, a general framework formally describing communication and concurrency in complex quantum
Feng, Y., Duan, R., Ji, Z. & Ying, M. 2007, 'Proof Rules For The Correctness Of Quantum Programs', Theoretical Computer Science, vol. 386, no. 1-2, pp. 151-166.
We apply the notion of quantum predicate proposed by D'Hondt and Panangaden to analyze a simple language fragment which may describe the quantum part of a future quantum computer in Knill's architecture. The notion of weakest liberal precondition semanti
Wei, Z. & Ying, M. 2007, 'Quantum Adiabatic Computation And Adiabatic Conditions', Physical Review A, vol. 76, no. 2, pp. 1-4.
Recently, quantum adiabatic computation has attracted more and more attention in the literature. It is a novel quantum computation model based on adiabatic approximation, and the analysis of a quantum adiabatic algorithm depends highly on the adiabatic c
Cao, Y., Ying, M. & Chen, G. 2007, 'Retraction And Generalized Extension Of Computing With Words', IEEE Transactions on Fuzzy Systems, vol. 15, no. 6, pp. 1238-1250.
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 cons
Cao, Y., Ying, M. & Chen, G. 2007, 'State-Based Control of Fuzzy Discrete-Event Systems', IEEE Transactions on Systems, Man, and Cybernetics, Part B: Cybernetics, vol. 37, no. 2, pp. 410-424.
To effectively represent possibility arising from states and dynamics of a system, fuzzy discrete-event systems (DESs) as a generalization of conventional DESs 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 DESs in this paper. An approach to finding all fuzzy states that are reachable by controlling the system is presented first. After introducing the notion of controllability for fuzzy states, a necessary and sufficient condition for a set of fuzzy states to be controllable is then provided. It was also found that event- and state-based controls are not equivalent, and the relationship between them was further discussed. Finally, we examine the possibility of driving a fuzzy DES under control from a given initial state to a prescribed set of fuzzy states and then keeping it there indefinitely
Ying, M. 2007, 'Topology, randomness and noise in process calculus', Frontiers of Electrical and Electronic Engineering in China, vol. 2, no. 2, pp. 127-131.
Formal models of communicating and concurrent systems are one of the most important topics in formal methods, and process calculus is one of the most successful formal models of communicating and concurrent systems. In the previous works, the author systematically studied topology in process calculus, probabilistic process calculus and pi-calculus with noisy channels in order to describe approximate behaviors of communicating and concurrent systems as well as randomness and noise in them. This article is a brief survey of these works.
Wang, G. & Ying, M. 2007, 'Multipartite Unlockable Bound Entanglement In The Stabilizer Formalism', Physical Review A, vol. 75, no. 5, pp. 1-8.
We 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 mixe
Duan, R., Feng, Y. & Ying, M. 2007, 'Entanglement is Not Necessary for Perfect Discrimination between Unitary Operations', Physical Review Letters, vol. 98, no. 10.
Duan, R., Feng, Y., Ji, Z. & Ying, M. 2007, 'Distinguishing arbitrary multipartite basis unambiguously using local operations and classical communication.', Physical review letters, vol. 98, no. 23, p. 230502.
We show that an arbitrary basis of a multipartite quantum state space consisting of K distant parties such that the kth party has local dimension dk always contains at least N= Sigma(k=1)(K) (dk-1)+1 members that are unambiguously distinguishable using local operations and classical communication (LOCC). We further show that this lower bound is optimal by analytically constructing a special product basis having only N members unambiguously distinguishable by LOCC. Interestingly, such a special product basis not only gives a stronger form of the weird phenomenon "nonlocality without entanglement," but also implies the existence of a locally distinguishable entangled basis.
Duan, R., Feng, Y. & Ying, M. 2007, 'Entanglement is not necessary for perfect discrimination between unitary operations.', Physical review letters, vol. 98, no. 10, p. 100503.
We show that a unitary operation (quantum circuit) secretly 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 operations are required in our scheme. We further show that our scheme is optimal in the sense that the number of the runs is minimal when discriminating only two unitary operations.
Duan, R., Feng, Y., Ji, Z. & Ying, M. 2007, 'Distinguishing arbitrary multipartite basis unambiguously using local operations and classical communication (vol 98, art no 230602, 2007)', PHYSICAL REVIEW LETTERS, vol. 99, no. 1.
Duan, R., Feng, Y. & Ying, M. 2007, 'Entanglement is not necessary for perfect discrimination between unitary operations (vol 98, pg 100503, 2007)', PHYSICAL REVIEW LETTERS, vol. 98, no. 12.
Feng, Y., Duan, R., Ji, Z. & Ying, M. 2007, 'Probabilistic bisimulations for quantum processes', Information and Computation.
Wei, Z. & Ying, M. 2006, 'A Relation Between Fidelity And Quantum Adiabatic Evolution', Physics Letters A, vol. 356, no. 4-5, pp. 312-315.
Recently, some quantum algorithms have been implemented by quantum adiabatic evolutions. In this Letter, 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 ev
Ji, Z., Feng, Y., Duan, R. & Ying, M. 2006, 'Boundary Effect Of Deterministic Dense Coding', Physical Review A, vol. 73, no. 3, pp. 1-3.
We present a rigorous proof of an interesting boundary effect of deterministic dense coding first observed by S. Mozes, J. Oppenheim, and B. Reznik [Phys. Rev. A 71, 012311 (2005)]. Namely, it is shown that d(2)-1 cannot be the maximal alphabet size of a
Ji, Z., Feng, Y., Duan, R. & Ying, M. 2006, 'Identification And Distance Measures Of Measurement Apparatus', Physical Review Letters, vol. 96, no. 20, pp. 1-4.
We propose simple schemes that can perfectly identify projective measurement apparatuses secretly chosen from a finite set. Entanglement is used in these schemes both to make possible the perfect identification and to improve the efficiency significantly
Ying, M. 2006, 'Linguistic Quantifiers Modeled By Sugeno Integrals', Artificial Intelligence, vol. 170, no. 6-7, pp. 581-606.
Since quantifiers have the ability of summarizing the properties of a class of objects without enumerating them, linguistic quantification is a very important topic in the field of high level knowledge representation and reasoning. This paper introduces
Wei, Z. & Ying, M. 2006, 'Majorization In Quantum Adiabatic Algorithms', Physical Review A, vol. 74, no. 4, pp. 1-7.
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 universall
Cao, Y. & Ying, M. 2006, 'Observability And Decentralized Control Of Fuzzy Discrete-Event Systems', IEEE Transactions on Fuzzy Systems, vol. 14, no. 2, pp. 202-216.
Fuzzy 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-ev
Duan, R., Feng, Y. & Ying, M. 2006, 'Partial Recovery Of Quantum Entanglement', IEEE Transactions On Information Theory, vol. 52, no. 7, pp. 3080-3104.
Suppose 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
Feng, Y., Duan, R. & Ying, M. 2006, 'Relation Between Catalyst-Assisted Transformation And Multiple-Copy Transformation For Bipartite Pure States', Physical Review A, vol. 74, no. 4, pp. 1-7.
We 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. A 7
Cao, Y. & Ying, M. 2006, 'Similarity-Based Supervisory Control Of Discrete-Event Systems', IEEE Transactions On Automatic Control, vol. 51, no. 2, pp. 325-330.
Due 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 tradit
Duan, R., Ji, Z., Feng, Y. & Ying, M. 2006, 'Some Issues In Quantum Information Theory', Journal Of Computer Science And Technology, vol. 21, no. 5, pp. 776-789.
Quantum information theory is a new interdisciplinary research field related to quantum mechanics, computer science, information theory, and applied mathematics. It provides completely new paradigms to do information processing tasks by employing the pri
Wang, G. & Ying, M. 2006, 'Unambiguous Discrimination Among Quantum Operations', Physical Review A, vol. 73, no. 4, pp. 1-5.
We 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 t
Zhang, C., Feng, Y. & Ying, M. 2006, 'Unambiguous Discrimination Of Mixed Quantum States', Physics Letters A, vol. 353, no. 4, pp. 300-306.
The problem of unambiguous discrimination between mixed quantum states is addressed by isolating the part of each mixed state which has no contribution to discrimination and by employing the strategy of set discrimination of pure states. A necessary and
Zhang, C., Ying, M. & Qiao, B. 2006, 'Universal Programmable Devices For Unambiguous Discrimination', Physical Review A, vol. 74, no. 4, pp. 1-9.
We 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
Wei, Z. & Ying, M. 2006, 'A Modified Quantum Adiabatic Evolution For The Deutsch-Jozsa Problem', Physics Letters A, vol. 354, no. 4, pp. 271-273.
Deutsch-Jozsa algorithm has been implemented via a quantum adiabatic evolution by S. Das et al. [S. Das, R. Kobes, G. Kunstatter, Phys. Rev. A 65 (2002) 062310]. This adiabatic algorithm gives rise to a quadratic speed up over classical algorithms. We sh
Feng, Y., Duan, R. & Ying, M. 2006, 'Relation between catalyst-assisted transformation and multiple-copy transformation for bipartite pure states', Physical Review A, vol. 74, no. 4.
Ji, Z., Feng, Y., Duan, R. & Ying, M. 2006, 'Identification and distance measures of measurement apparatus.', Physical review letters, vol. 96, no. 20, p. 200401.
We propose simple schemes that can perfectly identify projective measurement apparatuses secretly chosen from a finite set. Entanglement is used in these schemes both to make possible the perfect identification and to improve the efficiency significantly. Based on these results, a brief discussion on the problem of how to appropriately define distance measures of measurements is also provided.
Ji, Z., Feng, Y., Duan, R. & Ying, M. 2006, 'Boundary effect of deterministic dense coding', Physical Review A, vol. 73, no. 3.
Zhang, C., Ying, M. & Qiao, B. 2006, 'Optimal universal programmable detectors for unambiguous discrimination', Phys. Rev. A, vol. 74, pp. 042308-042308.
We 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 data register. The quantum state in the data register is what users want to identify, which is confirmed to be among the n states in program registers. The task of the discriminator is to tell the users which state stored in the program registers is equivalent to that in the data register. First, we give a necessary and sufficient condition for judging an unambiguous programmable discriminator. Then, if $m=n$, we present an optimal unambiguous programmable discriminator for them, in the sense of maximizing the worst-case probability of success. Finally, we propose a universal unambiguous programmable discriminator for arbitrary n quantum states.
Ying, M. 2005, 'A Theory Of Computation Based On Quantum Logic (I)', Theoretical Computer Science, vol. 344, no. 2-3, pp. 134-207.
The (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 60 years ago. It is currently understood as a logic whose truth val
Feng, Y., Duan, R. & Ying, M. 2005, 'Catalyst-Assisted Probabilistic Entanglement Transformation', IEEE Transactions On Information Theory, vol. 51, no. 3, pp. 1090-1101.
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
Duan, R., Feng, Y., Ji, Z. & Ying, M. 2005, 'Efficiency Of Deterministic Entanglement Transformation', Physical Review A, vol. 71, no. 2, pp. 1-7.
We prove that sufficiently many copies of a bipartite entangled pure state can always be transformed into some copies of another one with certainty by local quantum operations and classical communication. The efficiency of such a transformation is charac
Ying, M. 2005, 'Knowledge Transformation And Fusion In Diagnostic Systems', Artificial Intelligence, vol. 163, no. 1, pp. 1-45.
Diagnostic systems depend on knowledge bases specifying the causal, structural or functional interactions among components of the diagnosed objects. A diagnostic specification in a diagnostic system is a semantic interpretation of a knowledge base. We in
Ji, Z., Feng, Y. & Ying, M. 2005, 'Local Cloning Of Two Product States', Physical Review A, vol. 72, no. 3, pp. 1-5.
Local 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 constrain
Duan, R., Feng, Y., Li, X. & Ying, M. 2005, 'Multiple-Copy Entanglement Transformation And Entanglement Catalysis', Physical Review A, vol. 71, no. 4, pp. 1-11.
We prove that any multiple-copy entanglement transformation [S. Bandyopadhyay, V. Roychowdhury, and U. Sen, Phys. Rev. A 65, 052315 (2002)] can be implemented by a suitable entanglement-assisted local transformation [D. Jonathan and M. B. Plenio, Phys. R
Li, S., Ying, M. & Li, Y. 2005, 'On Countable RCC Models', Fundamenta Informaticae, vol. 65, no. 4, pp. 329-351.
Region Connection Calculus (RCC) is the most widely studied formalism of Qualitative Spatial Reasoning. It has been known for some time that each connected regular topological space provides an RCC model. These 'standard' models are inevitable uncountabl
Ji, Z., Cao, H. & Ying, M. 2005, 'Optimal Conclusive Discrimination Of Two States Can Be Achieved Locally', Physical Review A, vol. 71, no. 3, pp. 1-5.
This paper constructs a local operation and classical communication protocol that achieves the global optimality of conclusive discrimination of any two pure states with arbitrary a priori probability. This can be interpreted that there is no
Ying, M. 2005, 'Pi-Calculus With Noisy Channels', Acta Informatica, vol. 41, no. 9, pp. 525-593.
It is assumed in the pi-calculus that communication channels are always noiseless. But it is usually not the case in the mobile systems that developers are faced with in the real life. In this paper, we introduce an extension of pi, called pi(N), in whic
Cao, Y. & Ying, M. 2005, 'Supervisory Control Of Fuzzy Discrete Event Systems', IEEE Transactions on Systems, Man, and Cybernetic..., vol. 35, no. 2, pp. 366-371.
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 modeled by fuzzy automata. The behavior of such discrete event systems is described by fuzzy
Sun, X., Duan, R. & Ying, M. 2005, 'The Existence Of Quantum Entanglement Catalysts', IEEE Transactions On Information Theory, vol. 51, no. 1, pp. 75-80.
Without 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., vol. 83, p. 3566, 1999) presented an interesting
Duan, R., Feng, Y., Li, X. & Ying, M. 2005, 'Trade-Off Between Multiple-Copy Transformation And Entanglement Catalysis', Physical Review A, vol. 71, no. 6, pp. 1-7.
We 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
Duan, R., Feng, Y. & Ying, M. 2005, 'Entanglement-Assisted Transformation Is Asymptotically Equivalent To Multiple-Copy Transformation', Physical Review A, vol. 72, no. 2, pp. 1-5.
We show that two ways of manipulating quantum entanglement-namely, entanglement-assisted local transformation [D. Jonathan and M. B. Plenio, Phys. Rev. Lett. 83, 3566 (1999)] and multiple-copy transformation [S. Bandyopadhyay, V. Roychowdhury, and U. Sen
Duan, R., Feng, Y., Li, X. & Ying, M. 2005, 'Trade-off between multiple-copy transformation and entanglement catalysis', Physical Review A, vol. 71, no. 6.
Duan, R., Feng, Y., Li, X. & Ying, M. 2005, 'Multiple-copy entanglement transformation and entanglement catalysis', Physical Review A, vol. 71, no. 4.
Duan, R., Feng, Y., Ji, Z. & Ying, M. 2005, 'Efficiency of deterministic entanglement transformation', Physical Review A, vol. 71, no. 2.
Duan, R., Feng, Y. & Ying, M. 2005, 'Entanglement-assisted transformation is asymptotically equivalent to multiple-copy transformation', Physical Review A, vol. 72, no. 2.
Feng, Y., Duan, R., Ji, Z.-.F. & Ying, M. 2005, 'Proof rules for purely quantum programs', CoRR, vol. abs/cs/0507043.
Li, Y., Li, S. & Ying, M. 2005, 'Relational reasoning in the region connection calculus', CoRR, vol. abs/cs/0505041.
Li, S. & Ying, M. 2004, 'Generalized Region Connection Calculus', Artificial Intelligence, vol. 160, no. 1-2, pp. 1-34.
The Region Connection Calculus (RCC) is one of the most widely referenced system of high-level (qualitative) spatial reasoning. RCC assumes a continuous representation of space. This contrasts sharply with the fact that spatial information obtained from physical recording devices is nowadays invariably digital in form and therefore implicitly uses a discrete representation of space. Recently, Galton developed a theory of discrete space that parallels RCC, but question still lies in that can we have a theory of qualitative spatial reasoning admitting models of discrete spaces as well as continuous spaces? In this paper we aim at establishing a formal theory which accommodates both discrete and continuous spatial information, and a generalization of Region Connection Calculus is introduced. GRCC, the new theory, takes two primitives: the mereological notion of part and the topological notion of connection. RCC and Galton's theory for discrete space are both extensions of GRCC. The relation between continuous models and discrete ones is also clarified by introducing some operations on models of GRCC. In particular, we propose a general approach for constructing countable RCC models as direct limits of collections of finite models. Compared with standard RCC models given rise from regular connected spaces, these countable models have the nice property that each region can be constructed in finite steps from basic regions. Two interesting countable RCC models are also given: one is a minimal RCC model, the other is a countable sub-model of the continuous space R2.
Qiu, D. & Ying, M. 2004, 'Characterizations Of Quantum Automata', Theoretical Computer Science, vol. 312, no. 2-3, pp. 479-489.
We define q quantum finite automata (qQFAs) and q quantum regular grammars (qQRGs), and verify that they are exactly equivalent to those measure-once quantum finite automata (MO-QFAs) in the literature. In particular, we define q quantum pushdown automat
Ji, Z., Duan, R. & Ying, M. 2004, 'Comparability Of Multipartite Entanglement', Physics Letters A, vol. 330, no. 6, pp. 418-423.
We prove, in a multipartite setting, that it is always feasible to exactly transform a genuinely m-partite entangled pure state with sufficient many copies to any other m-partite state via local quantum operation and classical communication. This result
Cao, H. & Ying, M. 2004, 'Local Discrimination Of Maximally Entangled States In Canonical Form', Physics Letters A, vol. 333, no. 3-4, pp. 232-234.
It is shown that two copies are enough to distinguish a complete basis of maximally entangled states in canonical form by constructing an explicit protocol. In particular, in such a protocol, no auxiliary system is needed and the symmetrical roles of cer
Feng, Y. & Ying, M. 2004, 'Process Algebra Approach To Reasoning About Concurrent Actions', Journal Of Computer Science And Technology, vol. 19, no. 3, pp. 364-373.
A reasonable transition rule is proposed for synchronized actions and some equational properties of bisimilarity and weak bisimilarity in the process algebra for reasoning about concurrent actions are presented.
Duan, R., Ji, Z., Feng, Y. & Ying, M. 2004, 'Quantum Operation Quantum Fourier Transform And Semi-Definite Programming', Physics Letters A, vol. 323, no. 1-2, pp. 48-56.
We 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 for
Feng, Y., Duan, R. & Ying, M. 2004, 'When Catalysis Is Useful For Probabilistic Entanglement Transformation', Physical Review A, vol. 69, no. 6, pp. 1-5.
We determine all 2x2 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, a
Feng, Y.A., Duan, R.Y. & Ying, M.S. 2004, 'Unambiguous discrimination between mixed quantum states', PHYSICAL REVIEW A, vol. 70, no. 1.
Feng, Y., Duan, R. & Ying, M. 2004, 'When catalysis is useful for probabilistic entanglement transformation', Physical Review A - Atomic, Molecular, and Optical Physics, vol. 69, no. 6, pp. 062310-062311.
The quantum states that served as useful catalysts for a probabilistic entanglement transformation were discussed. It was stated that the quantum states provided maximum transformation probability. A sufficiently necessary condition was derived when higher-dimensional catalysts were considered. It was found that among these conditions certain probabilistic transformation had useful catalysts.
Li, S. & Ying, M. 2003, 'Region Connection Calculus: Its models and composition table', Artificial Intelligence, vol. 145, no. 1-2, pp. 121-146.
Originating in Allen's analysis of temporal relations, the notion of composition table has become a key technique in providing an efficient inference mechanism for a wide class of theories in the field artificial intelligence. This paper is mainly about the consistency-based composition table (RCC8 CT) of the Region Connection Calculus (RCC) raised by Randell, Cui and Cohn. First we show each RCC model is a consistent model of the RCC8 CT. Then after an exhaustive analysis we show that no RCC model can be interpreted extensionally anyway and hence give a negative answer to a conjecture raised by Bennett. All these results are given in an extensional RCC8 composition table, where we attach to each cell entry in the RCC8 CT a superscript to indicate in what circumstances an extensional interpretation is possible.
Li, S. & Ying, M. 2003, 'Extensionality Of The RCC8 Composition Table', Fundamenta Informaticae, vol. 55, no. 3-4, pp. 363-385.
This paper is mainly concerned with the RCC8 composition table entailed by the Region Connection Calculus (RCC), a well-known formalism for Qualitative Spatial Reasoning. This table has been independently generated by Egenhofer in the context of Geograph
Ying, M. 2003, 'Reasoning About Probabilistic Sequential Programs In A Probabilistic Logic', Acta Informatica, vol. 39, no. 5, pp. 315-389.
We introduce a notion of strong monotonicity of probabilistic predicate transformers. This notion enables us to establish a normal form theorem for monotone probabilistic predicate transformers. Three other healthiness conditions, namely, conjunctivity,
Ying, M. 2002, 'Bisimulation Indexes And Their Applications', Theoretical Computer Science, vol. 275, no. 1-Feb, pp. 1-68.
Bisimulation expresses the equivalence of processes whose external actions are identical. Sometimes we may meet two processes which are not exactly bisimilar but more or less bisimilar in the sense that whenever a process makes an action the other can ma
Ying, M. 2002, 'Implication Operators In Fuzzy Logic', IEEE Transactions on Fuzzy Systems, vol. 10, no. 1, pp. 88-91.
The choice of fuzzy implication as well as other connectives is an important problem in the theoretical development of fuzzy logic, and at the same time, it Is significant for the performance of the systems In which fuzzy logic technique is employed. The
Ying, M. & Wang, H. 2002, 'Lattice-Theoretic Models Of Conjectures, Hypotheses And Consequences', Artificial Intelligence, vol. 139, no. 2, pp. 253-267.
Trillas, Cubillo and Castineira [Artificial Intelligence 117 (2000) 255-275] defined several interesting operators in orthocomplemented lattices. These operators give a quite general algebraic model for conjectures, consequences and hypotheses. We presen
Feng, Y., Zhang, S., Duan, R. & Ying, M. 2002, 'Lower Bound On Inconclusive Probability Of Unambiguous Discrimination', Physical Review A, vol. 66, no. 6, pp. 1-4.
We derive a lower bound on the inconclusive probability of unambiguous discrimination among n linearly independent quantum states by using the constraint of no signaling. It improves the bound presented in the. paper of Zhang, Feng, Sun, and Ying [Phys.
Sun, X., Zhang, S., Feng, Y. & Ying, M. 2002, 'Mathematical Nature Of And A Family Of Lower Bounds For The Success Probability Of Unambiguous Discrimination', Physical Review A, vol. 65, no. 4, pp. 1-3.
Unambiguous discrimination is a strategy to the discrimination problem that identifies the state with certainty, leaving a possibility of undecidability. This paper points out that the optimal success probability of unambiguous discrimination is mathemat
Feng, Y., Zhang, S. & Ying, M. 2002, 'Probabilistic Cloning And Deleting Of Quantum States', Physical Review A, vol. 65, no. 4, pp. 1-4.
We construct a probabilistic cloning and deleting machine which, taking several copies of an input quantum state, can output a linear superposition of multiple cloning and deleting states. Since the machine can perform cloning and deleting in a single un
Zhang, S. & Ying, M. 2002, 'Set Discrimination Of Quantum States', Physical Review A, vol. 65, no. 6, pp. 1-5.
We introduce a notion of set discrimination, which is an interesting extension of quantum state discrimination. A state is secretly chosen from a number of quantum states, which are partitioned into some disjoint sets. A set discrimination is required to
Feng, Y., Zhang, S., Sun, X. & Ying, M. 2002, 'Universal And Original-Preserving Quantum Copying Is Impossible', Physics Letters A, vol. 297, no. 1-Feb, pp. 1-3.
We show that an arbitrary quantum state cannot be universally 1 --> 2 copied keeping the original copy unchanged. Indeed, the density operator of the additional copy after the copying transformation is nothing but the scale product of the identity matrix
Ying, M. 2002, 'Universal Quantum-Copying Machines: A Sufficient And Necessary Condition', Physics Letters A, vol. 302, no. 1, pp. 1-7.
It was shown that the copying quality of the Wootters-Zurek quantum copying machine depends on the input states. So Buzek and Hillery proposed the notion of universal copying machine. A universal machine is a quantum copier whose copying quality is indep
Ying, M. 2002, 'Wootters-Zurek Quantum-Copying Machine: The Higher-Dimensional Case', Physics Letters A, vol. 299, no. 2-Mar, pp. 107-115.
We examine Wootters-Zurek quantum-copying machine on a higher-dimensional state space and evaluate the index D-a of copying quality and three indexes D-ab((1)), D-ab((2)) and D-ab((3)) of entanglement of the output modes. (C) 2002 Elsevier Science B.V. A
Ying, M. 2002, 'A Formal Model Of Computing With Words', IEEE Transactions on Fuzzy Systems, vol. 10, no. 5, pp. 640-652.
Classical automata are formal models of computing with values. Fuzzy automata are generalizations of classical automata where the knowledge about the system's next state is vague or uncertain. It is worth noting that like classical automata, fuzzy automa
Ying, M. 2002, 'Additive Models Of Probabilistic Processes', Theoretical Computer Science, vol. 275, no. 1-Feb, pp. 481-519.
We propose a new model of probabilistic processes. In this model, a probability is assigned to the action of a prefix and a probability distribution is assigned to the components of a parallel composition. In addition, the probability of a transition of
Feng, Y., Zhang, S., Duan, R. & Ying, M. 2002, 'Lower bound on inconclusive probability of unambiguous discrimination', Physical Review A - Atomic, Molecular, and Optical Physics, vol. 66, no. 6, pp. 623131-623134.
A lower bound on the inconclusive probability of unambiguous discrimination among n linearly independent quantum states was derived. The constraint of no signaling was used for the derivation. An alternative method was also proposed by constructing an appropriate measurement to derive the lower bound.
Sun, X., Zhang, S., Feng, Y. & Ying, M. 2002, 'Mathematical nature of and a family of lower bounds for the success probability of unambiguous discrimination', Physical Review A. Atomic, Molecular, and Optical Physics, vol. 65, no. 4 B, pp. 443061-443063.
Unambiguous discrimination was described as a strategy applicable to quantum state discrimination. It described a state with certainity, leaving a possibility of undecidability. The problem of success probability of unambiguous discrimination was proved to be a case of the semidefinite programming (SDP) problem. A family of lower bounds of the optimal success probability was also presented.
Feng, Y., Zhang, S. & Ying, M. 2002, 'Probabilistic cloning and deleting of quantum states', Physical Review A. Atomic, Molecular, and Optical Physics, vol. 65, no. 4 A, pp. 423241-423244.
A probabilistic cloning and deleting machine was constructed to enable a linear superposition of multiple cloning and deleting states by taking several copies of an input quantum state. A necessary and sufficient condition for successful cloning and deleting was presented, and it required that the copies of an arbitrarily presumed number of the input states were linearly independent. An upper bound for the success probability of the cloning and deleting machine was derived.
Zhang, S. & Ying, M. 2002, 'Set discrimination of quantum states', Physical Review A - Atomic, Molecular, and Optical Physics, vol. 65, no. 6 A, pp. 623221-623225.
A notion of set discrimination of quantum states was introduced. Quantum states were partitioned into some disjoint sets and a state was secretly chosen from them. It was found that a perfect set discrimination could be performed only if the sets were orthogonal. The best efficiency of discrimination was derived in set discrimination and in combined case.
Feng, Y., Zhang, S.Y. & Ying, M.S. 2002, 'Probabilistic cloning and deleting of quantum states', PHYSICAL REVIEW A, vol. 65, no. 4.
Ying, M. 2001, 'Fuzzy Topology Based On Residuated Lattice-Valued Logic', Acta Mathematica Sinica-English Series, vol. 17, no. 1, pp. 89-102.
We use a semantical method of complete residuated lattice-valued logic to give a generalization of fuzzy topology as a partial answer to a problem by Rosser and Turquette.
Ying, M. & Wirsing, M. 2001, 'Recursive Equations In Higher-Order Process Calculi', Theoretical Computer Science, vol. 266, no. 1-Feb, pp. 839-852.
Regarding behaviour equivalence in higher-order process calculi, Sangiorgi (Inform. and Comput. 131 (1996) 141) and Thomsen (Inform. and Comput. 116 (1995) 38) introduced context and higher-order bisimulations, respectively. In this paper, uniqueness of
Zhang, S., Feng, Y., Sun, X. & Ying, M. 2001, 'Upper Bound For The Success Probability Of Unambiguous Discrimination Among Quantum States', Physical Review A, vol. 64, no. 6, pp. 1-3.
One strategy to the discrimination problem is to identify the state with certainty, leaving a possibility of undecidability. This paper gives an upper bound for the maximal success probability of unambiguous discrimination among n states. This bound coin
Biacino, L., Gerla, G. & Ying, M. 2000, 'Approximate Reasoning Based On Similarity', Mathematical Logic Quarterly, vol. 46, no. 1, pp. 77-86.
The connection between similarity logic and the theory of closure operators is examined. Indeed one proves that the consequence relation defined in [14] can be obtained by composing two closure operators and that the resulting operator is still a closure
Ying, M. 2000, 'Automata Theory Based On Quantum Logic Ii', International Journal Of Theoretical Physics, vol. 39, no. 11, pp. 2545-2557.
We establish the pumping lemma in automata theory based on quantum logic under certain conditions on implication, and discuss the recognizability by the product and union of orthomodular lattice-valued (quantum) automata. In particular, we show that the
Ying, M. 2000, 'Automata Theory Based On Quantum Logic. (I)', International Journal Of Theoretical Physics, vol. 39, no. 4, pp. 985-995.
We present a basic Framework of automats theory based on quantum logic. In particular, we introduce the orthomodular lattice-valued (quantum) predicate of recognizability and establish some of its fundamental properties.
Ying, M. 2000, 'Declarative Semantics Of Programming In Residuated Lattice-Valued Logic', Science in China Series E: Technological Sciences, vol. 43, no. 5, pp. 481-494.
We give two generalizations of Tarski's fixpoint theorem in the setting of residuated lattices and use them to establish van Emdem-Kowalski's least fixpoint semantics for residuated lattice-valued logic programs.
Ying, M. 2000, 'Weak Confluence And Tau-Inertness', Theoretical Computer Science, vol. 238, no. 1-Feb, pp. 465-475.
We introduce a new definition of weak confluences and show that they are equivalent to tau-inertness without any appealing to tau-well-foundedness. (C) 2000 Elsevier Science B.V. All rights reserved.
Ying, M. 2000, 'Weak confluence and -inertness', Theoretical Computer Science, vol. 238, no. 1-2, pp. 465-475.
We introduce a new definition of weak confluences and show that they are equivalent to -inertness without any appealing to -well-foundedness. &copy; 2000 Elsevier Science B.V. All rights reserved.
Ying, M. 1999, 'A Shorter Proof To Uniqueness Of Solutions Of Equations', Theoretical Computer Science, vol. 216, no. 1-Feb, pp. 395-397.
We give a very short proof of uniqueness of solutions of equations regarding observation congruence, the main notion of equality, over Milner's process calculus. (C) 1999-Elsevier Science B.V. All rights reserved.
Ying, M. 1999, 'Perturbation Of Fuzzy Reasoning', IEEE Transactions on Fuzzy Systems, vol. 7, no. 5, pp. 625-629.
We propose the concepts of maximum and average perturbations of fuzzy sets and estimate maximum and average perturbation parameters for various methods of fuzzy reasoning.
Ying, M. 1999, 'Topology in process calculus (I): limit behaviour of agents', Journal of Computer Science and Technology, vol. 14, no. 4, pp. 328-336.
As part of a work aimed at constructing natural topologies on agent expressions, the concepts of modifications on actions of a topology on names of actions and the simplest topology on agents induced by a topology on names of actions are introduced. It is shown that the limit behavior of some agents is compatible with transitional semantics.
Ying, M.S. & Liu, F.C. 1999, 'Three-valued and four-valued approach to logic programming with negation', Chinese Journal of Advanced Software Research, vol. 6, no. 1, pp. 71-83.
The relation among various semantic approaches for programming in three-valued logics is further clarified, some of the main results on Lassez and Maher's consequence operator are generalized, and all possible choices of three-valued implications under the following two conditions are found: (1) Every program has the (strong or weak) model intersection property, and (2) Fixpoints or post-fixpoints of Delahaye and Thibau, Fitting, and Lassez and Maher's consequence operators associated with a program coincide with its models. To overcome some objections to programming in three-valued logics, a four-valued semantics for logic programming with negation is also proposed.
Ying, M. 1999, 'Phase semantics for a pure noncommutative linear propositional logic', Journal of Computer Science and Technology, vol. 14, no. 2, pp. 135-139.
We use a many-sorted language to remove commutativity from phase semantics of linear logic and show that pure noncommutative intuitionistic linear propositional logic plus two classical rules enjoys the soundness and completeness with respect to completely noncommutative phase semantics. &copy; 1999 Science Press, Beijing China and Allerton Press Inc.
Ying, M. 1999, 'A shorter proof to uniqueness of solutions of equations', Theoretical Computer Science, vol. 216, no. 1-2, pp. 395-397.
We give a very short proof of uniqueness of solutions of equations regarding observation congruence, the main notion of equality, over Milner's process calculus. &copy; 1999 - Elsevier Science B.V. All rights reserved.
Lu, R. & Ying, M. 1998, 'A Model Of Reasoning About Knowledge', Science in China Series E: Technological Sciences, vol. 41, no. 5, pp. 527-534.
A modal logical language and its Kripke semantics and Aumann semantics are introduced. A complete for mal deduction system is established to describe reasoning about knowledge in multi-agent systems involving different languages, and an institution of lo
Ying, M. & Bouchon-Meunier, B. 1998, 'Approximate Reasoning With Linguistic Modifiers', International Journal of Intelligent Systems, vol. 13, no. 5, pp. 403-418.
We analyze the influence of some usual linguistic modifiers, such as scalar product, normalization, Bouchon-Meunier modifiers, perturbation, and (weakening and reinforcement) power, in the process of approximate reasoning and clarify the difference betwe
Ying, M. 1998, 'Compactness In Fuzzy Logic', Chinese Science Bulletin, vol. 43, no. 14, pp. 1166-1171.
Compactness in Pavelka's fuzzy logic for some compact lattices of truth values is shown, and the concept of gradual compactness is introduced to establish some corresponding results in a more general setting.
Lu, R. & Ying, M. 1998, 'A model of reasoning about knowledge', Science in China, Series E: Technological Sciences, vol. 41, no. 5, pp. x11-534.
A modal logical language and its Kripke semantics and Aumann semantics are introduced. A complete formal deduction system is established to describe reasoning about knowledge in multi-agent systems involving different languages, and an institution of logics for multi-agent systems is constructed.
Ying, M. & Bouchon-Meunier, B. 1997, 'Quantifiers, modifiers and qualifiers in fuzzy logic', Journal of Applied Non-Classical Logics, vol. 7, no. 3, pp. 335-342.
In this paper, we propose a formalization of fuzzy logic and obtain some results concerning the composition, exchange and compatibility with propositional connectives of fuzzy quantifiers, modifiers and qualifiers in this setting.
Ying, M. 1996, 'An Open Logic System Admitting Modification Of Inference Rules', Chinese Science Bulletin, vol. 41, no. 13, pp. 1069-1071.
NA
Ying, M. 1996, 'When Is The Ideal Completion Of Abstract Basis Algebraic', Theoretical Computer Science, vol. 159, no. 2, pp. 355-356.
The concepts of abstract basis and its ideal completion play an important role in domain theory because the category of bases (and approximable relations) is equivalent to the category of continuous domains (and continuous mappings) (cf. [1, Theorem 2.2.
Ying, M. 1996, 'Initial and terminal semantics for glued theories in institutions', Ruan Jian Xue Bao/Journal of Software, vol. 7, no. 6, pp. 360-363.
In this paper, the correspondence among initial (terminal) semantics of glued theories and factor theories in institutions is clarified under certain intuitive conditions.
Ying, M. 1995, 'Putting consistent theories together in institutions', Journal of Computer Science and Technology, vol. 10, no. 3, pp. 260-266.
The problem of putting consistent theories together in institutions is discussed. A general necessary condition for consistency of the resulting theory is carried out, and some sufficient conditions are given for diagrams of theories in which shapes are tree bundles or directed graphs. Moreover, some transformations from complicated cases to simple ones are established. &copy; 1995, Science Press, Beijing China and Allerton Press Inc.. All rights reserved.
Ying, M. 1995, 'Institutions of variable truth values: An approach in the ordered style', Journal of Computer Science and Technology, vol. 10, no. 3, pp. 267-273.
The concept of institution of variable truth values is introduced and some main results about institutions are generalized. In particular, some properties of institutions of variable truth values preserved by change of truth values are established. &copy; 1995, Science Press, Beijing China and Allerton Press Inc.. All rights reserved.
Ying, M. 1994, 'A Logic For Approximate Reasoning', Journal Of Symbolic Logic, vol. 59, no. 3, pp. 830-837.
NA
Ying, M. 1994, 'On The Method Of Neighborhood-Systems In Fuzzy Topology', Fuzzy Sets and Systems, vol. 68, no. 2, pp. 227-238.
In this paper, we revivify the theory of neighborhood systems in fuzzy topology with the method used to develop fuzzifying topology and find another kind of reasonable neighborhood structure in fuzzy topology except quasi-neighborhood systems of Pu and L
Ying, M. 1993, 'A New Approach For Fuzzy Topology .3.', Fuzzy Sets and Systems, vol. 55, no. 2, pp. 193-207.
The concepts of fuzzy continuity, product and quotient spaces are presented, and their fundamental properties are obtained in fuzzifying topology.
Ying, M. 1993, 'Compactness In Fuzzifying Topology', Fuzzy Sets and Systems, vol. 55, no. 1, pp. 79-92.
We introduce the concept of compactness and establish a generalization of Tychonoff's theorem in the framework of fuzzifying topology.
Ying, M. 1993, 'Fuzzifying Uniform-Spaces', Fuzzy Sets and Systems, vol. 53, no. 1, pp. 93-104.
We introduce the concept of fuzzifying uniform spaces in the framework of fuzzifying topology and establish some fundamental properties of fuzzifying uniform spaces.
Ying, M. 1993, 'Fuzzifying Topology Based On Complete Residuated Lattice-Valued Logic .1.', Fuzzy Sets and Systems, vol. 56, no. 3, pp. 337-373.
We greatly extend fuzzifying topology by introducing a unary fuzzy predicate interpreted as the property to be fuzzifying topological spaces on the class of all so-called fuzzifying pretopological spaces and by adopting the semantic method of complete re
Ying, M. 1992, 'A New Approach For Fuzzy Topology .2.', Fuzzy Sets and Systems, vol. 47, no. 2, pp. 221-232.
We introduce the concepts of interior, boundary, subspace, connected space, first- and second-countable spaces, and establish some of their properties in fuzzifying topology.
Ying, M. 1992, 'Another Version Of The Fundamental Theorem Of Ultraproduct Of Lattice-Valued Models', Chinese Science Bulletin, vol. 37, no. 17, pp. 1491-1492.
NA
Ying, M. 1992, 'Compactness, The Lowenheim-Skolem Property And The Direct-Product Of Lattices Of Truth Values', Zeitschrift Fur Mathematische Logik Und Grundlag..., vol. 38, no. 5-Jun, pp. 521-524.
We show that compactness is preserved by arbitrary direct products of lattices of truth values and that the Lowenheim-Skolem property is preserved by finite direct products of lattices of truth values. MSC: 03C07, 03B50.
Ying, M. 1992, 'Reasonableness Of The Compositional Rule Of Fuzzy Inference', Fuzzy Sets and Systems, vol. 36, no. 2, pp. 305-310.
NA
Ying, M. 1992, 'The Fundamental Theorem Of Ultraproduct In Pavelkas Logic', Zeitschrift Fur Mathematische Logik Und Grundlag..., vol. 38, no. 3, pp. 197-201.
In [This Zeitschrift 25 (1979), 45-52, 119-134, 447-464], Pavelka systematically discussed propositional calculi with values in enriched residuated lattices and developed a general framework for approximate reasoning. In the first part of this paper we i
Ying, M. 1991, 'A New Approach For Fuzzy Topology (I)', Fuzzy Sets and Systems, vol. 39, no. 3, pp. 303-321.
We point out a new approach for fuzzy topology with fuzzy logic, and discuss the neighborhood structure of a point and the convergence of nets and filters in this new framework.
Ying, M. 1991, 'Deduction Theorem For Many-Valued Inference', Zeitschrift Fur Mathematische Logik Und Grundlag..., vol. 37, no. 6, pp. 533-537.
NA
Ying, M. 1990, 'The Alternativity Measures Of Fuzzy-Sets', Fuzzy Sets and Systems, vol. 37, no. 1, pp. 105-110.
NA
Ying, M. 1990, 'On Probabilistic Normed Spaces Under T,L', International Journal of Mathematics and Mathematical Sciences, vol. 13, no. 4, pp. 731-736.
We introduce the operation [formula omitted] copulative with T,L to define PN space under T,L and establish some basic properties of probabilistic seminorms and norms under T,L. Finally, we discuss so-called L-simple spaces. &copy; 1990, Hindawi Publishing Corporation. All rights reserved.
Ying, M. 1989, 'On A Class Of Non-Causal Triangle Functions', Mathematical Proceedings Of The Cambridge Philos..., vol. 106, no. NA, pp. 467-469.
NA
Ying, M. 1989, 'On Epsilon-Fuzzy Sets', Fuzzy Sets and Systems, vol. 31, no. 1, pp. 123-129.
NA
Ying, M.S. 1989, 'On a class of non-causal triangle functions', Mathematical Proceedings of the Cambridge Philosophical Society, vol. 106, no. 03, pp. 467-467.
Ying, M. 1988, 'Conjugate Transforms For Tau-T,L-Semigroups Of Distance Distribution-Functions', Kexue Tongbao, vol. 33, no. 23, pp. 2001-2002.
NA
Ying, M. 1988, 'On Standard Models Of Fuzzy Modal-Logics', Fuzzy Sets and Systems, vol. 26, no. 3, pp. 357-363.
NA
Ying, M. 1988, 'Some Notes On Multidimensional Fuzzy-Reasoning', Cybernetics And Systems, vol. 19, no. 4, pp. 281-293.
NA
Ying, M. 1988, 'Report from Jiangxi Province, People's Republic of China', Fuzzy Sets and Systems, vol. 25, no. 3, p. 382.
Ying, M. 1987, 'A Counter-example Of Gottwald Theorem', Fuzzy Sets and Systems, vol. 23, no. 3, pp. 399-400.
NA
Ying, M. 1987, 'Fuzzy Semilattices', Information Sciences, vol. 43, no. 3, pp. 155-159.
NA
Sun, X., Duan, R. & Ying, M., 'The Existence of Quantum Entanglement Catalysts', IEEE. Trans. Inform. Theory, vol. 51, p. 1.
Without 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 showing that the presence of another state, called a catalyst, enables such a transformation without changing the catalyst. They also pointed out that in general it is very hard to find an analytical condition under which a catalyst exists. In this paper we study the existence of catalysts for two incomparable quantum states. For the simplest case of $2\times 2$ catalysts for transformations from one $4\times 4$ state to another, a necessary and sufficient condition for existence is found. For the general case, we give an efficient polynomial time algorithm to decide whether a $k\times k$ catalyst exists for two $n\times n$ incomparable states, where $k$ is treated as a constant.
Duan, R., Feng, Y. & Ying, M., 'An Equivalence of Entanglement-Assisted Transformation and Multiple-Copy Entanglement Transformation'.
We 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 condition, for any non-maximally entangled bipartite pure state and any integer $n$ not less than 4, we are able to explicitly construct a set of $n\times n$ quantum states which can be produced by using the given state as a catalyst. Second, we prove that for any positive integer $k$, entanglement-assisted transformation with $k\times k$-dimensional catalysts is useful in producing a target state if and only if multiple-copy entanglement transformation with $k$ copies of state is useful in producing the same target. Moreover, a necessary and sufficient condition for both of them is obtained in terms of the Schmidt coefficients of the target. This equivalence of entanglement-assisted transformation and multiple-copy entanglement transformation implies many interesting properties of entanglement transformation. Furthermore, these results are generalized to the case of probabilistic entanglement transformations.
Duan, R., Feng, Y. & Ying, M., 'Partial Recovery of Quantum Entanglement', IEEE Trans. Inform. Theory, vol. 52, p. 7.
Suppose 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 of transformation. However, an interesting phenomenon called partial entanglement recovery shows that it is possible to recover some amount of entanglement by adding another entangled state and transforming the two entangled states collectively. In this paper we are mainly concerned with the feasibility of partial entanglement recovery. The basic problem we address is whether a given state is useful in recovering entanglement lost in a specified transformation. In the case where the source and target states of the original transformation satisfy the strict majorization relation, a necessary and sufficient condition for partial entanglement recovery is obtained. For the general case we give two sufficient conditions. We also give an efficient algorithm for the feasibility of partial entanglement recovery in polynomial time. As applications, we establish some interesting connections between partial entanglement recovery and the generation of maximally entangled states, quantum catalysis, mutual catalysis, and multiple-copy entanglement transformation.
Feng, Y., Duan, R. & Ying, M., 'Catalyst-assisted Probabilistic Entanglement Transformation', IEEE Trans. Inform. Theory, vol. 51, p. 3.
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.
Yu, N., Duan, R. & Ying, M., 'Optimal Simulation of a Perfect Entangler', Phys. Rev. A, vol. 81, p. 032328.
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.
Ji, Z., Feng, Y. & Ying, M., 'Local cloning of two product states', Phys. Rev. A, vol. 72, p. 032324.
Local 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 in some sense. In this paper, we show that cloning is not that lucky; namely, conclusive LOCC cloning of two product states is strictly less efficient than global cloning.
Yu, N. & Ying, M., 'Non-Additivity of Minimum Output p-$\mathbf{R\acute{e}nyi}$ Entropy'.
Hastings 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 0.2855$.
Yu, N. & Ying, M., '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.
Ji, Z., Chen, J., Wei, Z. & Ying, M., 'The LU-LC conjecture is false', Quantum Inf. Comput., vol. 10, p. 1.
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.
Ying, M., 'Another Quantum Lovász Local Lemma'.
We define a natural conceptual framework in which a generalization of the Lov\'{a}sz Local Lemma can be established in quantum probability theory.
Ying, M., 'Hoare Logic for Quantum Programs'.
Hoare 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 foundation of programming methodology for quantum computers, we develop a full-fledged Hoare logic for both partial and total correctness of quantum programs. It is proved that this logic is (relatively) complete by exploiting the power of weakest preconditions and weakest liberal preconditions for quantum programs.
Ying, M., '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.
Wei, Z. & Ying, M., 'Quantum search algorithm by adiabatic evolution under a priori probability'.
Grover'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 Grover's algorithm. In this paper, we show that quantum search algorithm by adiabatic evolution has two properties that conventional quantum search algorithm doesn't have. Firstly, we show that in the initial state of the algorithm only the amplitude of the basis state corresponding to the solution affects the running time of the algorithm, while other amplitudes do not. Using this property, if we know a priori probability about the location of the solution before search, we can modify the adiabatic evolution to make the algorithm faster. Secondly, we show that by a factor for the initial and finial Hamiltonians we can reduce the running time of the algorithm arbitrarily. Especially, we can reduce the running time of adiabatic search algorithm to a constant time independent of the size of the database. The second property can be extended to other adiabatic algorithms.
Wei, Z. & Ying, M., 'Quantum adiabatic evolutions that can't be used to design efficient algorithms'.
Quantum 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 path is too simple, the minimal gap between the ground state and the first excited state of this quantum adiabatic evolution is an inverse exponential distance. Thus quantum adiabatic evolutions of this kind can't be used to design efficient quantum algorithms. Similarly, we show that a quantum adiabatic evolution with a simple final hamiltonian also has a long running time, which suggests that some functions can't be minimized efficiently by any quantum adiabatic evolution with a interpolation path.
Wang, G. & Ying, M., 'Realization of positive-operator-valued measures by projective measurements without introducing ancillary dimensions'.
We 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 outcomes is faithfully reproduced. A necessary and sufficient condition for a POVM to be realizable in this way is also derived. In contrast to the canonical approach provided by Neumark's theorem, our method has the advantage of requiring no auxiliary system. Moreover, an arbitrary POVM can be realized by utilizing our protocol on an extended space which is formed by adding only a single extra dimension.
Wei, Z. & Ying, M., 'Linearity and Quantum Adiabatic Theorem'.
We 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 the linearity and the adiabatic approximation simultaneously. Besides, based on this observation we point out the mistake in the traditional proof for the adiabatic theorem. This mistake is the root of the troubles that the adiabatic theorem has met. We also show that a similar mistake remains in some recent modifications of the traditional adiabatic theorem attempting to eliminate the troubles.
Selected Peer-Assessed Projects