# 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 ...

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 ...

Ying, M., Duan, R., Feng, Y. & Ji, Z. 2010, 'Predicate Transformer Semantics of Quantum Programs' in Gay, S. & Mackie, I. (eds),

View/Download from: UTS OPUS

*Semantic Techniques in Quantum Computation*, Cambridge University Press, Cambridge, pp. 311-360.View/Download from: UTS OPUS

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âs suggestion of representing quantum programs by superoperators and elucidates DâHondt-Panangadenâ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â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â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),

View/Download from: UTS OPUS or Publisher's site

*Lecture Notes in Computer Science 6285 - Software Architecture*, Springer, Germany, pp. 8-23.View/Download from: UTS OPUS or Publisher's site

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),

View/Download from: UTS OPUS or Publisher's site

*Handbook of Quantum Logic and Quantum Structures*, Elsevier, London, UK, pp. 619-754.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Leibniz International Proceedings in Informatics, LIPIcs*, the 26th International Conference on Concurrency Theory (CONCUR'15), pp. 441-455.View/Download from: UTS OPUS or Publisher's site

© 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',

View/Download from: Publisher's site

*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)*, pp. 482-496.View/Download from: Publisher's site

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. © 2014 Springer-Verlag.

Feng, Y., Yu, N. & Ying, M. 2013, 'Reachability Analysis of Recursive Quantum Markov Chains',

View/Download from: UTS OPUS or Publisher's site

*Lecture Notes in Computer Science*, the 38th Int. Symp. on Mathematical Foundations of Computer Science (MFCS'13), Springer, IST Austria, pp. 385-396.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*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.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Lecture Notes in Computer Science*, the 24th International Conference on Concurrency Theory (CONCUR'13), Springer, University of Buenos Aires, Argentina, pp. 334-348.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*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.View/Download from: UTS OPUS or Publisher's site

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.',

View/Download from: Publisher's site

*CONCUR*, Springer, pp. 69-83.View/Download from: Publisher's site

Feng, Y., Duan, R. & Ying, M. 2011, 'Bisimulation for Quantum Processes',

View/Download from: UTS OPUS or Publisher's site

*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.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: Publisher's site

*POPL 11: PROCEEDINGS OF THE 38TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES*, pp. 523-534.View/Download from: Publisher's site

Zhang, H., Zhang, Y., Ying, M. & Zhou, Y. 2011, 'Translating first-order theories into logic programs',

View/Download from: Publisher's site

*IJCAI International Joint Conference on Artificial Intelligence*, pp. 1126-1131.View/Download from: Publisher's site

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',

View/Download from: UTS OPUS

*24th AAAI Conference on Artificial Intelligence 2010*, Conference on Artificial Intelligence, The AAAI Press, Atlanta, Georgia, pp. 375-380.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Programming Languages and Systems 8th Asian Symposium, APLAS 2010*, Programming Languages and Systems, Springer-Verlag, Shanghai, China, pp. 16-20.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*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.View/Download from: UTS OPUS

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',

View/Download from: Publisher's site

*Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2007*, pp. 279-288.View/Download from: Publisher's site

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 © 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',

View/Download from: UTS OPUS or Publisher's site

*2005 IEEE International Conference On Granular Computing*, IEEE International Conference on Granular Computing, IEEE, Beijing, China, pp. 91-91.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: Publisher's site

*PHYSICAL REVIEW A*, vol. 91, no. 3.View/Download from: Publisher's site

Ying, S., Ying, M. & Feng, Y. 2015, 'Quantum Privacy-Preserving Data Mining.',

*CoRR*, vol. abs/1512.04009. Li, Y. & Ying, M. 2014, 'Debugging quantum processes using monitoring measurements',

View/Download from: Publisher's site

*Physical Review A*, vol. 89.View/Download from: Publisher's site

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',

View/Download from: Publisher's site

*Acta Informatica*, vol. 51, pp. 1-24.View/Download from: Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*IEEE Transactions on Information Theory*, vol. 60, no. 4, pp. 2069-2079.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*ACM TRANSACTIONS ON COMPUTATIONAL LOGIC*, vol. 15, no. 3.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Journal of Computer and System Sciences*, vol. 79, no. 7, pp. 1181-1198.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Science Of Computer Programming*, vol. 78, no. 9, pp. 1679-1700.View/Download from: UTS OPUS or Publisher's site

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ö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',

View/Download from: UTS OPUS or Publisher's site

*Physical Review A*, vol. 87, no. 1, pp. 1-9.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Journal of Computer and System Sciences*, vol. 79, no. 1, pp. 152-172.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*PHYSICAL REVIEW A*, vol. 88, no. 1.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Chinese Science Bulletin*, vol. 57, no. 16, pp. 1903-1909.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*ACM Transactions pn Programming Language and Systems (TOPLAS)*, vol. 34, no. 4, pp. 1-43.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Theoretical Computer Science*, vol. 446, pp. 75-97.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Lecture Notes in Computer Science*, vol. 7454, pp. 69-83.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: Publisher's site

*PHYSICAL REVIEW LETTERS*, vol. 109, no. 2.View/Download from: Publisher's site

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. Ying, M. & Feng, Y. 2011, 'A Flowchart Language For Quantum Programming',

View/Download from: UTS OPUS or Publisher's site

*IEEE Transactions On Software Engineering*, vol. 37, no. 4, pp. 466-485.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*ACM Transactions pn Programming Language and Systems (TOPLAS)*, vol. 33, no. 6, pp. 1-49.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Physical Review A*, vol. 84, no. 1, pp. 1-3.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: Publisher's site

*ACM SIGPLAN NOTICES*, vol. 46, no. 1, pp. 523-534.View/Download from: Publisher's site

Ji, Z., Chen, J., Wei, Z. & Ying, M. 2010, 'The LU-LC conjecture is false',

View/Download from: UTS OPUS

*Quantum Information and Computation*, vol. 10, no. 1, pp. 97-108.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Physical Review A*, vol. 82, no. 3, pp. 1-6.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Physical Review A*, vol. 81, no. 3, pp. 1-4.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Physical Review A*, vol. 81, no. 3, pp. 1-10.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Artificial Intelligence Journal*, vol. 174, no. 2, pp. 162-176.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Artificial Intelligence Journal*, vol. 174, no. 12-13, pp. 951-983.View/Download from: UTS OPUS or Publisher's site

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 âcanonicalâ 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',

View/Download from: UTS OPUS or Publisher's site

*Acta Informatica*, vol. 47, no. 4, pp. 221-250.View/Download from: UTS OPUS or Publisher's site

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. © 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. © Rinton Press.

Duan, R., Feng, Y., Xin, Y. & Ying, M. 2009, 'Distinguishability of Quantum States by Separable Operations',

View/Download from: UTS OPUS or Publisher's site

*IEEE Transactions On Information Theory*, vol. 55, no. 3, pp. 1320-1330.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Acm Transactions On Computational Logic*, vol. 10, no. 3, pp. 1-36.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*IEEE Transactions On Computers*, vol. 58, no. 6, pp. 728-743.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*International Journal of Intelligent Systems*, vol. 24, no. 3, pp. 223-225.View/Download from: UTS OPUS or Publisher's site

NA

Feng, Y., Duan, R. & Ying, M. 2009, 'Locally undetermined states, generalized Schmidt decomposition, and application in distributed computing',

View/Download from: UTS OPUS

*Quantum Information and Computation*, vol. 9, no. 11, pp. 997-1012.View/Download from: UTS OPUS

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',

View/Download from: Publisher's site

*PHYSICAL REVIEW LETTERS*, vol. 103, no. 21.View/Download from: Publisher's site

Ying, M., Feng, Y., Duan, R. & Ji, Z. 2009, 'An algebra of quantum processes',

View/Download from: Publisher's site

*ACM Transactions on Computational Logic*, vol. 10, no. 3, pp. 1-36.View/Download from: Publisher's site

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. © Rinton Press.

Ji, Z., Wang, G., Duan, R., Feng, Y. & Ying, M. 2008, 'Parameter Estimation of Quantum Channels',

View/Download from: UTS OPUS or Publisher's site

*IEEE Transactions On Information Theory*, vol. 54, no. 11, pp. 5172-5185.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Theoretical Computer Science*, vol. 403, no. 2-3, pp. 192-201.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Physical Review A*, vol. 77, no. 3, pp. 1-10.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Journal of Mathematical Physics*, vol. 49, no. 1, pp. 1-7.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Physical Review Letters*, vol. 100, no. 2, pp. 1-4.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Physical Review A*, vol. 77, no. 3, pp. 1-12.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Quantum Information and Computation*, vol. 10, no. 1-Feb, pp. 160-177.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS

*Quantum Information and Computation*, vol. 10, no. 1-Feb, pp. 160-177.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Information Processing Letters*, vol. 104, no. 4, pp. 152-158.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 75, no. 6, pp. 1-6.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS

*Physical Review Letters*, vol. 98, no. 23, pp. 1-4.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS

*Physical Review Letters*, vol. 98, no. 10, pp. 1-4.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Fuzzy Sets and Systems*, vol. 158, no. 9, pp. 927-928.View/Download from: UTS OPUS or Publisher's site

NA

Feng, Y., Duan, R., Ji, Z. & Ying, M. 2007, 'Probabilistic Bisimulations For Quantum Processes',

View/Download from: UTS OPUS or Publisher's site

*Information And Computation*, vol. 205, no. 11, pp. 1608-1639.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Theoretical Computer Science*, vol. 386, no. 1-2, pp. 151-166.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 76, no. 2, pp. 1-4.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*IEEE Transactions on Fuzzy Systems*, vol. 15, no. 6, pp. 1238-1250.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*IEEE Transactions on Systems, Man, and Cybernetics, Part B: Cybernetics*, vol. 37, no. 2, pp. 410-424.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Frontiers of Electrical and Electronic Engineering in China*, vol. 2, no. 2, pp. 127-131.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 75, no. 5, pp. 1-8.View/Download from: UTS OPUS

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',

View/Download from: Publisher's site

*Physical Review Letters*, vol. 98, no. 10.View/Download from: Publisher's site

Duan, R., Feng, Y., Ji, Z. & Ying, M. 2007, 'Distinguishing arbitrary multipartite basis unambiguously using local operations and classical communication.',

View/Download from: Publisher's site

*Physical review letters*, vol. 98, no. 23, p. 230502.View/Download from: Publisher's site

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)',

View/Download from: Publisher's site

*PHYSICAL REVIEW LETTERS*, vol. 99, no. 1.View/Download from: Publisher's site

Duan, R., Feng, Y. & Ying, M. 2007, 'Entanglement is not necessary for perfect discrimination between unitary operations (vol 98, pg 100503, 2007)',

View/Download from: Publisher's site

*PHYSICAL REVIEW LETTERS*, vol. 98, no. 12.View/Download from: Publisher's site

Feng, Y., Duan, R., Ji, Z. & Ying, M. 2007, 'Probabilistic bisimulations for quantum processes',

View/Download from: Publisher's site

*Information and Computation*.View/Download from: Publisher's site

Wei, Z. & Ying, M. 2006, 'A Relation Between Fidelity And Quantum Adiabatic Evolution',

View/Download from: UTS OPUS or Publisher's site

*Physics Letters A*, vol. 356, no. 4-5, pp. 312-315.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 73, no. 3, pp. 1-3.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS

*Physical Review Letters*, vol. 96, no. 20, pp. 1-4.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Artificial Intelligence*, vol. 170, no. 6-7, pp. 581-606.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 74, no. 4, pp. 1-7.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*IEEE Transactions on Fuzzy Systems*, vol. 14, no. 2, pp. 202-216.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*IEEE Transactions On Information Theory*, vol. 52, no. 7, pp. 3080-3104.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 74, no. 4, pp. 1-7.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*IEEE Transactions On Automatic Control*, vol. 51, no. 2, pp. 325-330.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Journal Of Computer Science And Technology*, vol. 21, no. 5, pp. 776-789.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 73, no. 4, pp. 1-5.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Physics Letters A*, vol. 353, no. 4, pp. 300-306.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 74, no. 4, pp. 1-9.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Physics Letters A*, vol. 354, no. 4, pp. 271-273.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: Publisher's site

*Physical Review A*, vol. 74, no. 4.View/Download from: Publisher's site

Ji, Z., Feng, Y., Duan, R. & Ying, M. 2006, 'Identification and distance measures of measurement apparatus.',

View/Download from: Publisher's site

*Physical review letters*, vol. 96, no. 20, p. 200401.View/Download from: Publisher's site

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',

View/Download from: Publisher's site

*Physical Review A*, vol. 73, no. 3.View/Download from: Publisher's site

Zhang, C., Ying, M. & Qiao, B. 2006, 'Optimal universal programmable detectors for unambiguous discrimination',

View/Download from: Publisher's site

*Phys. Rev. A*, vol. 74, pp. 042308-042308.View/Download from: Publisher's site

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)',

View/Download from: UTS OPUS or Publisher's site

*Theoretical Computer Science*, vol. 344, no. 2-3, pp. 134-207.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*IEEE Transactions On Information Theory*, vol. 51, no. 3, pp. 1090-1101.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 71, no. 2, pp. 1-7.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Artificial Intelligence*, vol. 163, no. 1, pp. 1-45.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 72, no. 3, pp. 1-5.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 71, no. 4, pp. 1-11.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS

*Fundamenta Informaticae*, vol. 65, no. 4, pp. 329-351.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 71, no. 3, pp. 1-5.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Acta Informatica*, vol. 41, no. 9, pp. 525-593.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*IEEE Transactions on Systems, Man, and Cybernetic...*, vol. 35, no. 2, pp. 366-371.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*IEEE Transactions On Information Theory*, vol. 51, no. 1, pp. 75-80.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 71, no. 6, pp. 1-7.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 72, no. 2, pp. 1-5.View/Download from: UTS OPUS

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',

View/Download from: Publisher's site

*Physical Review A*, vol. 71, no. 6.View/Download from: Publisher's site

Duan, R., Feng, Y., Li, X. & Ying, M. 2005, 'Multiple-copy entanglement transformation and entanglement catalysis',

View/Download from: Publisher's site

*Physical Review A*, vol. 71, no. 4.View/Download from: Publisher's site

Duan, R., Feng, Y., Ji, Z. & Ying, M. 2005, 'Efficiency of deterministic entanglement transformation',

View/Download from: Publisher's site

*Physical Review A*, vol. 71, no. 2.View/Download from: Publisher's site

Duan, R., Feng, Y. & Ying, M. 2005, 'Entanglement-assisted transformation is asymptotically equivalent to multiple-copy transformation',

View/Download from: Publisher's site

*Physical Review A*, vol. 72, no. 2.View/Download from: Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Artificial Intelligence*, vol. 160, no. 1-2, pp. 1-34.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Theoretical Computer Science*, vol. 312, no. 2-3, pp. 479-489.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Physics Letters A*, vol. 330, no. 6, pp. 418-423.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Physics Letters A*, vol. 333, no. 3-4, pp. 232-234.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Journal Of Computer Science And Technology*, vol. 19, no. 3, pp. 364-373.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Physics Letters A*, vol. 323, no. 1-2, pp. 48-56.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 69, no. 6, pp. 1-5.View/Download from: UTS OPUS

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',

View/Download from: Publisher's site

*PHYSICAL REVIEW A*, vol. 70, no. 1.View/Download from: Publisher's site

Feng, Y., Duan, R. & Ying, M. 2004, 'When catalysis is useful for probabilistic entanglement transformation',

View/Download from: Publisher's site

*Physical Review A - Atomic, Molecular, and Optical Physics*, vol. 69, no. 6, pp. 062310-062311.View/Download from: Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Artificial Intelligence*, vol. 145, no. 1-2, pp. 121-146.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Fundamenta Informaticae*, vol. 55, no. 3-4, pp. 363-385.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Acta Informatica*, vol. 39, no. 5, pp. 315-389.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Theoretical Computer Science*, vol. 275, no. 1-Feb, pp. 1-68.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*IEEE Transactions on Fuzzy Systems*, vol. 10, no. 1, pp. 88-91.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Artificial Intelligence*, vol. 139, no. 2, pp. 253-267.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 66, no. 6, pp. 1-4.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 65, no. 4, pp. 1-3.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 65, no. 4, pp. 1-4.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 65, no. 6, pp. 1-5.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Physics Letters A*, vol. 297, no. 1-Feb, pp. 1-3.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Physics Letters A*, vol. 302, no. 1, pp. 1-7.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Physics Letters A*, vol. 299, no. 2-Mar, pp. 107-115.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*IEEE Transactions on Fuzzy Systems*, vol. 10, no. 5, pp. 640-652.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Theoretical Computer Science*, vol. 275, no. 1-Feb, pp. 481-519.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: Publisher's site

*PHYSICAL REVIEW A*, vol. 65, no. 4.View/Download from: Publisher's site

Ying, M. 2001, 'Fuzzy Topology Based On Residuated Lattice-Valued Logic',

View/Download from: UTS OPUS

*Acta Mathematica Sinica-English Series*, vol. 17, no. 1, pp. 89-102.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Theoretical Computer Science*, vol. 266, no. 1-Feb, pp. 839-852.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS

*Physical Review A*, vol. 64, no. 6, pp. 1-3.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or 3.0.CO;2-X">Publisher's site

*Mathematical Logic Quarterly*, vol. 46, no. 1, pp. 77-86.View/Download from: UTS OPUS or 3.0.CO;2-X">Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*International Journal Of Theoretical Physics*, vol. 39, no. 11, pp. 2545-2557.View/Download from: UTS OPUS or Publisher's site

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)',

View/Download from: UTS OPUS or Publisher's site

*International Journal Of Theoretical Physics*, vol. 39, no. 4, pp. 985-995.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Theoretical Computer Science*, vol. 238, no. 1-Feb, pp. 465-475.View/Download from: UTS OPUS or Publisher's site

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. © 2000 Elsevier Science B.V. All rights reserved.

Ying, M. 1999, 'A Shorter Proof To Uniqueness Of Solutions Of Equations',

View/Download from: UTS OPUS

*Theoretical Computer Science*, vol. 216, no. 1-Feb, pp. 395-397.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS

*IEEE Transactions on Fuzzy Systems*, vol. 7, no. 5, pp. 625-629.View/Download from: UTS OPUS

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',

View/Download from: Publisher's site

*Journal of Computer Science and Technology*, vol. 14, no. 2, pp. 135-139.View/Download from: Publisher's site

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. © 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. © 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',

View/Download from: UTS OPUS

*International Journal of Intelligent Systems*, vol. 13, no. 5, pp. 403-418.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Chinese Science Bulletin*, vol. 43, no. 14, pp. 1166-1171.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: Publisher's site

*Journal of Applied Non-Classical Logics*, vol. 7, no. 3, pp. 335-342.View/Download from: Publisher's site

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',

View/Download from: UTS OPUS

*Theoretical Computer Science*, vol. 159, no. 2, pp. 355-356.View/Download from: UTS OPUS

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',

View/Download from: Publisher's site

*Journal of Computer Science and Technology*, vol. 10, no. 3, pp. 260-266.View/Download from: Publisher's site

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. © 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',

View/Download from: Publisher's site

*Journal of Computer Science and Technology*, vol. 10, no. 3, pp. 267-273.View/Download from: Publisher's site

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. © 1995, Science Press, Beijing China and Allerton Press Inc.. All rights reserved.

Ying, M. 1994, 'A Logic For Approximate Reasoning',

View/Download from: UTS OPUS or Publisher's site

*Journal Of Symbolic Logic*, vol. 59, no. 3, pp. 830-837.View/Download from: UTS OPUS or Publisher's site

NA

Ying, M. 1994, 'On The Method Of Neighborhood-Systems In Fuzzy Topology',

View/Download from: UTS OPUS or Publisher's site

*Fuzzy Sets and Systems*, vol. 68, no. 2, pp. 227-238.View/Download from: UTS OPUS or Publisher's site

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.',

View/Download from: UTS OPUS or Publisher's site

*Fuzzy Sets and Systems*, vol. 55, no. 2, pp. 193-207.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Fuzzy Sets and Systems*, vol. 55, no. 1, pp. 79-92.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Fuzzy Sets and Systems*, vol. 53, no. 1, pp. 93-104.View/Download from: UTS OPUS or Publisher's site

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.',

View/Download from: UTS OPUS or Publisher's site

*Fuzzy Sets and Systems*, vol. 56, no. 3, pp. 337-373.View/Download from: UTS OPUS or Publisher's site

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.',

View/Download from: UTS OPUS or Publisher's site

*Fuzzy Sets and Systems*, vol. 47, no. 2, pp. 221-232.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: Publisher's site

*Zeitschrift Fur Mathematische Logik Und Grundlag...*, vol. 38, no. 5-Jun, pp. 521-524.View/Download from: Publisher's site

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',

View/Download from: UTS OPUS or Publisher's site

*Fuzzy Sets and Systems*, vol. 36, no. 2, pp. 305-310.View/Download from: UTS OPUS or Publisher's site

NA

Ying, M. 1992, 'The Fundamental Theorem Of Ultraproduct In Pavelkas Logic',

View/Download from: Publisher's site

*Zeitschrift Fur Mathematische Logik Und Grundlag...*, vol. 38, no. 3, pp. 197-201.View/Download from: Publisher's site

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)',

View/Download from: UTS OPUS or Publisher's site

*Fuzzy Sets and Systems*, vol. 39, no. 3, pp. 303-321.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: Publisher's site

*Zeitschrift Fur Mathematische Logik Und Grundlag...*, vol. 37, no. 6, pp. 533-537.View/Download from: Publisher's site

NA

Ying, M. 1990, 'The Alternativity Measures Of Fuzzy-Sets',

View/Download from: UTS OPUS or Publisher's site

*Fuzzy Sets and Systems*, vol. 37, no. 1, pp. 105-110.View/Download from: UTS OPUS or Publisher's site

NA

Ying, M. 1990, 'On Probabilistic Normed Spaces Under T,L',

View/Download from: Publisher's site

*International Journal of Mathematics and Mathematical Sciences*, vol. 13, no. 4, pp. 731-736.View/Download from: Publisher's site

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. © 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',

View/Download from: UTS OPUS or Publisher's site

*Fuzzy Sets and Systems*, vol. 31, no. 1, pp. 123-129.View/Download from: UTS OPUS or Publisher's site

NA

Ying, M.S. 1989, 'On a class of non-causal triangle functions',

View/Download from: Publisher's site

*Mathematical Proceedings of the Cambridge Philosophical Society*, vol. 106, no. 03, pp. 467-467.View/Download from: Publisher's site

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',

View/Download from: UTS OPUS

*Fuzzy Sets and Systems*, vol. 26, no. 3, pp. 357-363.View/Download from: UTS OPUS

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',

View/Download from: UTS OPUS or Publisher's site

*Fuzzy Sets and Systems*, vol. 23, no. 3, pp. 399-400.View/Download from: UTS OPUS or Publisher's site

NA

Ying, M. 1987, 'Fuzzy Semilattices',

View/Download from: UTS OPUS or Publisher's site

*Information Sciences*, vol. 43, no. 3, pp. 155-159.View/Download from: UTS OPUS or Publisher's site

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',

View/Download from: Publisher's site

*Phys. Rev. A*, vol. 81, p. 032328.View/Download from: Publisher's site

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',

View/Download from: Publisher's site

*Phys. Rev. A*, vol. 72, p. 032324.View/Download from: Publisher's site

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**