#### Can supervise: YES

#### Publications

Ying, M 2016, *Foundations of Quantum Programming*, Morgan Kaufmann.View/Download from: Publisher's site

Ying, M 2001, *Topology in Process Calculus*, Springer New York.View/Download from: Publisher's site

Ying, M 2001, *Topology in process calculus : approximate correctness and infinite evolution of concurrent programs*, Springer, New York.

Chen, G, Ying, M & Kai-Yuan, C 1999, *Fuzzy logic and soft computing*, Kluwer Academic Publishers, Boston.

Barthe, G, Hsu, J, Ying, M, Yu, N & Zhou, L 2020, 'Relational proofs for quantum programs.', *Proc. ACM Program. Lang.*, vol. 4, pp. 21:1-21:1.

Guan, J, Fang, W & Ying, M 2020, 'Robustness Verification of Quantum Machine Learning.', *CoRR*, vol. abs/2008.07230.

Li, R, Wu, B, Ying, M, Sun, X & Yang, G 2020, 'Quantum Supremacy Circuit Simulation on Sunway TaihuLight', *IEEE Transactions on Parallel and Distributed Systems*, vol. 31, no. 4, pp. 805-816.View/Download from: Publisher's site

#### View description

© 1990-2012 IEEE. With the rapid progress made by industry and academia, quantum computers with dozens of qubits or even larger size are being realized. However, the fidelity of existing quantum computers often sharply decreases as the circuit depth increases. Thus, an ideal quantum circuit simulator on classical computers, especially on high-performance computers, is needed for benchmarking and validation. We design a large-scale simulator of universal random quantum circuits, often called 'quantum supremacy circuits', and implement it on Sunway TaihuLight. The simulator can be used to accomplish the following two tasks: 1) Computing a complete output state-vector; 2) Calculating one or a few amplitudes. We target the simulation of 49-qubit circuits. For task 1), we successfully simulate such a circuit of depth 39, and for task 2) we reach the 55-depth level. To the best of our knowledge, both of the simulation results reach the largest depth for 49-qubit quantum supremacy circuits.

Wang, Q & Ying, M 2020, 'Quantum Büchi Automata', *CoRR*, vol. abs/1804.08982.

Wang, Q & Ying, M 2020, 'Quantum Random Access Stored-Program Machines.', *CoRR*, vol. abs/2003.03514.

Zhou, L, Ying, S, Yu, N & Ying, M 2020, 'Quantum Coupling and Strassen Theorem.', *CoRR*, vol. abs/1803.10393.

Zhou, L, Ying, S, Yu, N & Ying, M 2020, 'Strassen's theorem for quantum couplings', *Theoretical Computer Science*, vol. 802, pp. 67-76.View/Download from: Publisher's site

#### View description

© 2019 Elsevier B.V. Strassen's theorem for probabilistic couplings is a fundamental theorem in probability theory that can be used to bound the probability of an event in a distribution by the probability of an event in another distribution coupled with the first. It has been widely applied in computer science for analysis of random algorithms, machine learning and verification of security and privacy protocols. We extend the coupling techniques in probability theory to quantum systems. A quantum generalisation of the notion of lifting, a coupling under certain constraints, is introduced. Several interesting examples and basic properties of quantum couplings and liftings are presented. Finally, a quantum extension of Strassen's theorem is established.

Zhou, L, Ying, S, Yu, N & Ying, M 2020, 'Strassen's theorem for quantum couplings', *THEORETICAL COMPUTER SCIENCE*, vol. 802, pp. 67-76.View/Download from: Publisher's site

Barthe, G, Hsu, J, Ying, M, Yu, N & Zhou, L 2019, 'Coupling Techniques for Reasoning about Quantum Programs.', *CoRR*, vol. abs/1901.05184.

Guo, GC & Ying, M 2019, 'Preface to special topic on quantum computing', *National Science Review*, vol. 6, no. 1, pp. 20-20.View/Download from: Publisher's site

Hung, S-H, Hietala, K, Zhu, S, Ying, M, Hicks, M & Wu, X 2019, 'Quantitative robustness analysis of quantum programs', *Proceedings of the ACM on Programming Languages*, vol. 3, no. POPL, pp. 1-29.View/Download from: Publisher's site

#### View description

Quantum computation is a topic of significant recent interest, with practical advances coming from both research and industry. A major challenge in quantum programming is dealing with errors (quantum noise) during execution. Because quantum resources (e.g., qubits) are scarce, classical error correction techniques applied at the level of the architecture are currently cost-prohibitive. But while this reality means that quantum programs are almost certain to have errors, there as yet exists no principled means to reason about erroneous behavior. This paper attempts to fill this gap by developing a semantics for erroneous quantum while-programs, as well as a logic for reasoning about them. This logic permits proving a property we have identified, called є-robustness, which characterizes possible "distance" between an ideal program and an erroneous one. We have proved the logic sound, and showed its utility on several case studies, notably: (1) analyzing the robustness of noisy versions of the quantum Bernoulli factory (QBF) and quantum walk (QW); (2) demonstrating the (in)effectiveness of different error correction schemes on single-qubit errors; and (3) analyzing the robustness of a fault-tolerant version of QBF.

Hung, S-H, Hietala, K, Zhu, S, Ying, M, Hicks, M & Wu, X 2019, 'Quantitative robustness analysis of quantum programs.', *Proceedings of the ACM on Programming Languages*, vol. 3, pp. 31:1-31:29.View/Download from: Publisher's site

#### View description

Quantum computation is a topic of significant recent interest, with practical advances coming from both research and industry. A major challenge in quantum programming is dealing with errors (quantum noise) during execution. Because quantum resources (e.g., qubits) are scarce, classical error correction techniques

applied at the level of the architecture are currently cost-prohibitive. But while this reality means that quantum

programs are almost certain to have errors, there as yet exists no principled means to reason about erroneous

behavior. This paper attempts to fill this gap by developing a semantics for erroneous quantum while programs, as well as a logic for reasoning about them. This logic permits proving a property we have identified, called ϵ-robustness, which characterizes possible łdistancež between an ideal program and an erroneous one. We have proved the logic sound, and showed its utility on several case studies, notably: (1) analyzing the robustness of noisy versions of the quantum Bernoulli factory (QBF) and quantum walk (QW); (2) demonstrating the (in)effectiveness of different error correction schemes on single-qubit errors; and (3) analyzing the robustness of a fault-tolerant version of QBF.

Li, G, Zhou, L, Yu, N, Ding, Y, Ying, M & Xie, Y 2019, 'Poq: Projection-based Runtime Assertions for Debugging on a Quantum Computer.', *CoRR*, vol. abs/1911.12855.

Liu, J, Zhan, B, Wang, S, Ying, S, Liu, T, Li, Y, Ying, M & Zhan, N 2019, 'Quantum Hoare Logic.', *Arch. Formal Proofs*, vol. 2019.

Liu, J, Zhou, L & Ying, M 2019, 'Expected Runtime of Quantum Programs.', *CoRR*, vol. abs/1911.12557.

Wang, Q, Liu, J & Ying, M 2019, 'Equivalence Checking of Quantum Finite-State Machines.', *CoRR*, vol. abs/1901.02173.

Ying, M 2019, 'Toward automatic verification of quantum programs', *Formal Aspects of Computing*, vol. 31, no. 1, pp. 3-25.View/Download from: Publisher's site

#### View description

© 2018, British Computer Society. This paper summarises the results obtained by the author and his collaborators in a program logic approach to the verification of quantum programs, including quantum Hoare logic, invariant generation and termination analysis for quantum programs. It also introduces the notion of proof outline and several auxiliary rules for more conveniently reasoning about quantum programs. Some problems for future research are proposed at the end of the paper.

Ying, M 2019, 'Toward automatic verification of quantum programs.', *Formal Aspects Comput.*, vol. 31, pp. 3-25.

Guan, J, Feng, Y, Turrini, A & Ying, M 2019, 'Model Checking Applied to Quantum Physics.', *CoRR*, vol. abs/1902.03218.

Ying, M & Feng, Y 2019, 'Model-checking quantum systems', *National Science Review*, vol. 6, no. 1, pp. 28-31.View/Download from: Publisher's site

Guan, J, Feng, Y & Ying, M 2018, 'Super-activating quantum memory with entanglement.', *Quantum Inf. Comput.*, vol. 18, pp. 1115-1124.

Feng, Y & Ying, MS 2018, 'Verification of Quantum Programs', *Ruan Jian Xue Bao/Journal of Software*, vol. 29, no. 4, pp. 1085-1093.View/Download from: Publisher's site

#### View description

© Copyright 2018, Institute of Software, the Chinese Academy of Sciences. All rights reserved. With the rapid development of quantum hardware, people tend to believe that special-purpose quantum computers with more than 100 qubits will be available in 5 to 10 years. It is conceivable that, once this becomes a reality, the development of quantum software will be crucial in harnessing the power of quantum computers. However, due to the distinguishable features of quantum mechanics, such as the no-cloning of quantum information and the nonlocal effect of entanglement, developing correct and efficient quantum programs and communication protocols is a challenging issue. Formal verification methods, particularly model checking techniques, have proven effective in classical software design and system modelling. Therefore, formal verification of quantum software has received more and more attention recently. This article reviews recent research findings in verification of both sequential quantum programs and quantum communication protocols, with the focus placed on the work of the two authors' research groups. Future directions and challenges in this area are also discussed.

Hung, S-H, Hietala, K, Zhu, S, Ying, M, Hicks, M & Wu, X 2018, 'Quantitative Robustness Analysis of Quantum Programs (Extended Version).', *CoRR*, vol. abs/1811.03585.

Li, Y & Ying, M 2018, 'Algorithmic analysis of termination problems for quantum programs.', *Proceedings of the ACM on Programming Languages*, vol. 2, pp. 35:1-35:1.View/Download from: Publisher's site

Ying, M & Li, Y 2018, 'Reasoning about Parallel Quantum Programs.', *CoRR*, vol. abs/1810.11334.

Ying, S & Ying, M 2018, 'Reachability analysis of quantum Markov decision processes.', *Inf. Comput.*, vol. 263, pp. 31-51.

Ying, S & Ying, M 2018, 'Reachability Analysis of Quantum Markov Decision Processes.', *Information and Computation*, vol. 263, pp. 31-51.View/Download from: Publisher's site

Guan, J, Feng, Y & Ying, M 2018, 'Decomposition of quantum Markov chains and its applications', *Journal of Computer and System Sciences*, vol. 95, pp. 55-68.View/Download from: Publisher's site

#### View description

© 2018 Elsevier Inc. Markov chains have been widely employed as a fundamental model in the studies of probabilistic and stochastic communicating and concurrent systems. It is well-understood that decomposition techniques play a key role in reachability analysis and model-checking of Markov chains. (Discrete-time) quantum Markov chains have been introduced as a model of quantum communicating systems [1] and also a semantic model of quantum programs [2]. The BSCC (Bottom Strongly Connected Component) and stationary coherence decompositions of quantum Markov chains were introduced in [3–5]. This paper presents a new decomposition technique, namely periodic decomposition, for quantum Markov chains. We further establish a limit theorem for them. As an application, an algorithm to find a maximum dimensional noiseless subsystem of a quantum communicating system is given using decomposition techniques of quantum Markov chains.

Guan, J, Feng, Y & Ying, M 2018, 'Super-activating Quantum Memory with Entanglement', *Quantum Information and Computation*, vol. 18, no. 13-14, pp. 1115-1124.

#### View description

Noiseless subsystems were proved to be an efficient and faithful approach to preserve fragile information against decoherence in quantum information processing and quantum computation. They were employed to design a general (hybrid) quantum memory cell model that can store both quantum and classical information. In this Letter, we find an interesting new phenomenon that the purely classical memory cell can be super-activated to preserve quantum states, whereas the null memory cell can only be super-activated to encode classical information. Furthermore, necessary and sufficient conditions for this phenomenon are discovered so that the super-activation can be easily checked by examining certain eigenvalues of the quantum memory cell without computing the

noiseless subsystems explicitly. In particular, it is found that entangled and separable stationary states are responsible for the super-activation of storing quantum and classical information, respectively.

Ying, M, Ying, S & Wu, X 2017, 'Invariants of quantum programs: characterisations and generation', *ACM SIGPLAN Notices*, vol. 52, no. 1, pp. 818-832.View/Download from: Publisher's site

Ying, S, Ying, M & Feng, Y 2017, 'Quantum Privacy-Preserving Data Analytics.', *CoRR*, vol. abs/1702.04420.

Ying, S, Ying, M & Feng, Y 2017, 'Quantum Privacy-Preserving Perceptron.', *CoRR*, vol. abs/1707.09893.

Yu, N & Ying, M 2015, 'Optimal simulation of Deutsch gates and the Fredkin gate', *PHYSICAL REVIEW A*, vol. 91, no. 3.View/Download from: Publisher's site

Li, Y & Ying, M 2014, 'Debugging quantum processes using monitoring measurements', *Physical Review A*, vol. 89.View/Download from: Publisher's site

#### View description

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

Li, Y, Yu, N & Ying, M 2014, 'Termination of nondeterministic quantum programs', *Acta Informatica*, vol. 51, pp. 1-24.View/Download from: Publisher's site

#### View description

We define a language-independent model of nondeterministic quantum programs in which a quantum program consists of a finite set of quantum processes. These processes are represented by quantum Markov chains over the common state space, which formalize the quantum mechanical behaviors of the machine. An execution of a nondeterministic quantum program is modeled by a sequence of actions of individual processes, and at each step of an execution a process is chosen nondeterministically to perform the next action. This execution model formalize the users behavior of calling the processes in the classical world. Applying the model to a quantum walk as an instance of physically realizable systems, we describe an execution step by step. A characterization of reachable space and a characterization of diverging states of a nondeterministic quantum program are presented. We establish a zero-one law for termination probability of the states in the reachable space. A combination of these results leads to a necessary and sufficient condition for termination of nondeterministic quantum programs. Based on this condition, an algorithm is found for checking termination of nondeterministic quantum programs within a fixed finite-dimensional state space.

Yu, N, Duan, R & Ying, M 2014, 'Distinguishability of Quantum States by Positive Operator-Valued Measures with Positive Partial Transpose', *IEEE Transactions on Information Theory*, vol. 60, no. 4, pp. 2069-2079.View/Download from: Publisher's site

#### View description

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})$.

Feng, Y, Deng, Y & Ying, M 2014, 'Symbolic bisimulation for quantum processes', *ACM Transactions on Computational Logic*, vol. 15, no. 2, pp. 1-35.View/Download from: Publisher's site

#### View description

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

Ying, M, Li, Y, Yu, N & Feng, Y 2014, 'Model-Checking Linear-Time Properties of Quantum Systems', *ACM TRANSACTIONS ON COMPUTATIONAL LOGIC*, vol. 15, no. 3.View/Download from: Publisher's site

Cao, Y, Xia, L & Ying, M 2013, 'Probabilistic Automata for Computing with Words', *Journal of Computer and System Sciences*, vol. 79, no. 1, pp. 152-172.View/Download from: Publisher's site

#### View description

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.

Ying, S & Ying, M 2013, 'Removing Measurements From Quantum Walks', *Physical Review A*, vol. 87, no. 1, pp. 1-9.View/Download from: Publisher's site

#### View description

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.

Yu, N, Duan, R & Ying, M 2013, 'Five two-qubit gates are necessary for implementing the Toffoli gate', *PHYSICAL REVIEW A*, vol. 88, no. 1.View/Download from: Publisher's site

Feng, Y, Yu, N & Ying, M 2013, 'Model Checking Quantum Markov Chains', *Journal of Computer and System Sciences*, vol. 79, no. 7, pp. 1181-1198.View/Download from: Publisher's site

#### View description

Although security of quantum cryptography is provable based on principles of quantum mechanics, it can be compromised by flaws in the design of quantum protocols. So, it is indispensable to develop techniques for verifying and debugging quantum cryptogra

Ying, M, Yu, N, Feng, Y & Duan, R 2013, 'Verification of quantum programs', *Science Of Computer Programming*, vol. 78, no. 9, pp. 1679-1700.View/Download from: Publisher's site

#### View description

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.

Mbuh, RN 2012, 'Introduction', *ASIAN WOMEN*, vol. 28, no. 4, pp. 3-7.

Zhou, C & Ying, M 2012, 'Approximating Markov processes through filtration', *Theoretical Computer Science*, vol. 446, pp. 75-97.View/Download from: Publisher's site

#### View description

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, Duan, R & Ying, M 2012, 'Four locally indistinguishable ququad-ququad orthogonal maximally entangled states.', *Physical Review Letters*, vol. 109, no. 2, pp. 020506-020506.View/Download from: Publisher's site

#### View description

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

Feng, Y, Duan, R & Ying, M 2012, 'Bisimulation For Quantum Processes', *ACM Transactions pn Programming Language and Systems (TOPLAS)*, vol. 34, no. 4, pp. 1-43.View/Download from: Publisher's site

#### View description

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

Ying, M, Feng, Y, Duan, R, Li, Y & Yu, N 2012, 'Quantum Programming: From Theories To Implementations', *Chinese Science Bulletin*, vol. 57, no. 16, pp. 1903-1909.View/Download from: Publisher's site

#### View description

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

Ying, M 2011, 'Floyd-hoare Logic For Quantum Programs', *ACM Transactions pn Programming Language and Systems (TOPLAS)*, vol. 33, no. 6, pp. 1-49.View/Download from: Publisher's site

#### View description

Floyd-Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a

Yu, N, Duan, R & Ying, M 2011, 'Any 2 Circle Times N Subspace Is Locally Distinguishable', *Physical Review A*, vol. 84, no. 1, pp. 1-3.View/Download from: Publisher's site

#### View description

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.

Ying, M & Feng, Y 2011, 'A Flowchart Language For Quantum Programming', *IEEE Transactions On Software Engineering*, vol. 37, no. 4, pp. 466-485.View/Download from: Publisher's site

#### View description

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

Duan, R, Xin, Y & Ying, M 2010, 'Locally Indistinguishable Subspaces Spanned By Three-Qubit Unextendible Product Bases', *Physical Review A*, vol. 81, no. 3, pp. 1-10.View/Download from: Publisher's site

#### View description

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

Li, Y, Duan, R & Ying, M 2010, 'Local Unambiguous Discrimination With Remaining Entanglement', *Physical Review A*, vol. 82, no. 3, pp. 1-6.View/Download from: Publisher's site

#### View description

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

Liu, W, Zhang, X, Li, S & Ying, M 2010, 'Reasoning about Cardinal Directions between Extended Objects', *Artificial Intelligence Journal*, vol. 174, no. 12-13, pp. 951-983.View/Download from: Publisher's site

#### View description

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 2010, 'Quantum Computation, Quantum Theory And AI', *Artificial Intelligence Journal*, vol. 174, no. 2, pp. 162-176.View/Download from: Publisher's site

#### View description

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

Yu, N, Duan, R & Ying, M 2010, 'Optimal Simulation Of A Perfect Entangler', *Physical Review A*, vol. 81, no. 3, pp. 1-4.View/Download from: Publisher's site

#### View description

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

Ying, M & Feng, Y 2010, 'Quantum loop programs', *Acta Informatica*, vol. 47, no. 4, pp. 221-250.View/Download from: Publisher's site

#### View description

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.

Ji, Z, Chen, J, Wei, Z & Ying, M 2010, 'The LU-LC conjecture is false', *Quantum Information and Computation*, vol. 10, no. 1, pp. 97-108.

#### View description

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.

Chen, G, Ying, M & Liu, Y 2009, 'Dealing With Uncertainty And Fuzziness In Intelligent Systems', *International Journal of Intelligent Systems*, vol. 24, no. 3, pp. 223-225.View/Download from: Publisher's site

#### View description

NA

Duan, R, Feng, Y & Ying, M 2009, 'Perfect Distinguishability of Quantum Operations', *PHYSICAL REVIEW LETTERS*, vol. 103, no. 21.View/Download from: Publisher's site

Duan, R, Feng, Y, Xin, Y & Ying, M 2009, 'Distinguishability of Quantum States by Separable Operations', *IEEE Transactions On Information Theory*, vol. 55, no. 3, pp. 1320-1330.View/Download from: Publisher's site

#### View description

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.

Feng, Y, Duan, R & Ying, M 2009, 'Locally undetermined states, generalized Schmidt decomposition, and application in distributed computing', *Quantum Information and Computation*, vol. 9, no. 11, pp. 997-1012.

#### View description

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

Ying, M & Feng, Y 2009, 'An Algebraic Language For Distributed Quantum Computing', *IEEE Transactions On Computers*, vol. 58, no. 6, pp. 728-743.View/Download from: Publisher's site

#### View description

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.

Ying, M, Feng, Y, Duan, R & Ji, Z 2009, 'An Algebra Of Quantum Processes', *Acm Transactions On Computational Logic*, vol. 10, no. 3, pp. 1-36.View/Download from: Publisher's site

#### View description

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.

Chen, J & Ying, M 2008, 'Ancilla-Assisted Discrimination Of Quantum Gates', *Quantum Information and Computation*, vol. 10, no. 1-Feb, pp. 160-177.

#### View description

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

Li, S & Ying, M 2008, 'Soft constraint abstraction based on semiring homomorphism', *Theoretical Computer Science*, vol. 403, no. 2-3, pp. 192-201.View/Download from: Publisher's site

#### View description

The semiring-based constraint satisfaction problems (semiring CSPs), proposed by Bistarelli, Montanari and Rossi [S. Bistarelli, U. Montanari, F. Rossi, Semiring-based constraints solving and optimization, Journal of the ACM 44 (2) (1997) 201236], is a very general framework of soft constraints. In this paper we propose an abstraction scheme for soft constraints that uses semiring homomorphism. To find optimal solutions of the concrete problem, we first work in the abstract problem and find its optimal solutions, and then use them to solve the concrete problem. In particular, we show that a mapping preserves optimal solutions if and only if it is an order-reflecting semiring homomorphism. Moreover, for a semiring homomorphism ? and a problem P over S, if t is optimal in ?(P), then there is an optimal solution View the MathML source of P such that View the MathML source has the same value as t in ?(P).

Wang, G & Ying, M 2008, 'Deterministic Distributed Dense Coding With Stabilizer States', *Physical Review A*, vol. 77, no. 3, pp. 1-10.View/Download from: Publisher's site

#### View description

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

Wang, G & Ying, M 2008, 'Perfect Many-To-One Teleportation With Stabilizer States', *Physical Review A*, vol. 77, no. 3, pp. 1-12.View/Download from: Publisher's site

#### View description

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

Duan, R, Feng, Y & Ying, M 2008, 'Local Distinguishability Of Multipartite Unitary Operations', *Physical Review Letters*, vol. 100, no. 2, pp. 1-4.View/Download from: Publisher's site

#### View description

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

Chen, JF, Duan, R, Ji, Z, Ying, M & Yu, JX 2008, 'Existence Of Universal Entangler', *Journal of Mathematical Physics*, vol. 49, no. 1, pp. 1-7.View/Download from: Publisher's site

#### View description

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

Ji, Z, Wang, G, Duan, R, Feng, Y & Ying, M 2008, 'Parameter Estimation of Quantum Channels', *IEEE Transactions On Information Theory*, vol. 54, no. 11, pp. 5172-5185.View/Download from: Publisher's site

#### View description

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.

Cao, Y, Ying, M & Chen, G 2007, 'Retraction And Generalized Extension Of Computing With Words', *IEEE Transactions on Fuzzy Systems*, vol. 15, no. 6, pp. 1238-1250.View/Download from: Publisher's site

#### View description

Fuzzy automata, whose input alphabet is a set of numbers or symbols, are a formal model of computing with values. Motivated by Zadeh's paradigm of computing with words rather than numbers, Ying proposed a kind of fuzzy automata, whose input alphabet cons

Cao, Y, Ying, M & Chen, G 2007, 'State-Based Control of Fuzzy Discrete-Event Systems', *IEEE Transactions on Systems, Man, and Cybernetics, Part B: Cybernetics*, vol. 37, no. 2, pp. 410-424.View/Download from: Publisher's site

#### View description

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

Liu, Y, Ying, M & Chen, G 2007, 'On Fundamentals Of Fuzzy Logic And Soft Computing And Some Applications', *Fuzzy Sets and Systems*, vol. 158, no. 9, pp. 927-928.View/Download from: Publisher's site

#### View description

NA

Wang, G & Ying, M 2007, 'Multipartite Unlockable Bound Entanglement In The Stabilizer Formalism', *Physical Review A*, vol. 75, no. 5, pp. 1-8.

#### View description

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

Wei, Z & Ying, M 2007, 'Quantum Adiabatic Computation And Adiabatic Conditions', *Physical Review A*, vol. 76, no. 2, pp. 1-4.

#### View description

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

Ying, M 2007, 'Topology, randomness and noise in process calculus', *Frontiers of Electrical and Electronic Engineering in China*, vol. 2, no. 2, pp. 127-131.

#### View description

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.

Zhang, C, Wang, G & Ying, M 2007, 'Discrimination Between Pure States And Mixed States', *Physical Review A*, vol. 75, no. 6, pp. 1-6.

#### View description

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 & Ying, M 2007, 'Entanglement Is Not Necessary For Perfect Discrimination Between Unitary Operations', *Physical Review Letters*, vol. 98, no. 10, pp. 1-4.

#### View description

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

Duan, R, Feng, Y & Ying, M 2007, 'Entanglement is not necessary for perfect discrimination between unitary operations (vol 98, pg 100503, 2007)', *PHYSICAL REVIEW LETTERS*, vol. 98, no. 12.View/Download from: Publisher's site

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

#### View description

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.

Ying, M, Chen, JF, Feng, Y & Duan, R 2007, 'Commutativity Of Quantum Weakest Preconditions', *Information Processing Letters*, vol. 104, no. 4, pp. 152-158.View/Download from: Publisher's site

#### View description

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

Duan, R, Feng, Y, Ji, Z & Ying, M 2007, 'Distinguishing Arbitrary Multipartite Basis Unambiguously Using Local Operations And Classical Communication', *Physical Review Letters*, vol. 98, no. 23, pp. 1-4.

#### View description

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, Ji, Z & Ying, M 2007, 'Distinguishing arbitrary multipartite basis unambiguously using local operations and classical communication (vol 98, art no 230602, 2007)', *PHYSICAL REVIEW LETTERS*, vol. 99, no. 1.View/Download from: Publisher's site

Feng, Y, Duan, R, Ji, Z & Ying, M 2007, 'Probabilistic Bisimulations For Quantum Processes', *Information And Computation*, vol. 205, no. 11, pp. 1608-1639.View/Download from: Publisher's site

#### View description

Modeling and reasoning about concurrent quantum systems is very important for both distributed quantum computing and quantum protocol verification. As a consequence, a general framework formally describing communication and concurrency in complex quantum

Feng, Y, Duan, R, Ji, Z & Ying, M 2007, 'Proof Rules For The Correctness Of Quantum Programs', *Theoretical Computer Science*, vol. 386, no. 1-2, pp. 151-166.View/Download from: Publisher's site

#### View description

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

Cao, Y & Ying, M 2006, 'Observability And Decentralized Control Of Fuzzy Discrete-Event Systems', *IEEE Transactions on Fuzzy Systems*, vol. 14, no. 2, pp. 202-216.View/Download from: Publisher's site

#### View description

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

Cao, Y & Ying, M 2006, 'Similarity-Based Supervisory Control Of Discrete-Event Systems', *IEEE Transactions On Automatic Control*, vol. 51, no. 2, pp. 325-330.View/Download from: Publisher's site

#### View description

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

Wang, G & Ying, M 2006, 'Unambiguous Discrimination Among Quantum Operations', *Physical Review A*, vol. 73, no. 4, pp. 1-5.

#### View description

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

Wei, Z & Ying, M 2006, 'A Modified Quantum Adiabatic Evolution For The Deutsch-Jozsa Problem', *Physics Letters A*, vol. 354, no. 4, pp. 271-273.View/Download from: Publisher's site

#### View description

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

Wei, Z & Ying, M 2006, 'A Relation Between Fidelity And Quantum Adiabatic Evolution', *Physics Letters A*, vol. 356, no. 4-5, pp. 312-315.View/Download from: Publisher's site

#### View description

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

Ying, M 2006, 'Linguistic Quantifiers Modeled By Sugeno Integrals', *Artificial Intelligence*, vol. 170, no. 6-7, pp. 581-606.View/Download from: Publisher's site

#### View description

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

Zhang, C, Ying, M & Qiao, B 2006, 'Optimal universal programmable detectors for unambiguous discrimination', *Phys. Rev. A*, vol. 74, pp. 042308-042308.View/Download from: Publisher's site

#### View description

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.

Zhang, C, Ying, M & Qiao, B 2006, 'Universal Programmable Devices For Unambiguous Discrimination', *Physical Review A*, vol. 74, no. 4, pp. 1-9.

#### View description

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

Duan, R, Feng, Y & Ying, M 2006, 'Partial Recovery Of Quantum Entanglement', *IEEE Transactions On Information Theory*, vol. 52, no. 7, pp. 3080-3104.View/Download from: Publisher's site

#### View description

Suppose Alice and Bob try to transform an entangled state shared between them into another one by local operations and classical communications. Then in general a certain amount of entanglement contained in the initial state will decrease in the process

Feng, Y, Duan, R & Ying, M 2006, 'Relation Between Catalyst-Assisted Transformation And Multiple-Copy Transformation For Bipartite Pure States', *Physical Review A*, vol. 74, no. 4, pp. 1-7.

#### View description

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

Zhang, C, Feng, Y & Ying, M 2006, 'Unambiguous Discrimination Of Mixed Quantum States', *Physics Letters A*, vol. 353, no. 4, pp. 300-306.View/Download from: Publisher's site

#### View description

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

Duan, R, Ji, Z, Feng, Y & Ying, M 2006, 'Some Issues In Quantum Information Theory', *Journal Of Computer Science And Technology*, vol. 21, no. 5, pp. 776-789.View/Download from: Publisher's site

#### View description

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

Ji, Z, Feng, Y, Duan, R & Ying, M 2006, 'Boundary Effect Of Deterministic Dense Coding', *Physical Review A*, vol. 73, no. 3, pp. 1-3.

#### View description

We present a rigorous proof of an interesting boundary effect of deterministic dense coding first observed by S. Mozes, J. Oppenheim, and B. Reznik [Phys. Rev. A 71, 012311 (2005)]. Namely, it is shown that d(2)-1 cannot be the maximal alphabet size of a

Ji, Z, Feng, Y, Duan, R & Ying, M 2006, 'Identification And Distance Measures Of Measurement Apparatus', *Physical Review Letters*, vol. 96, no. 20, pp. 1-4.

#### View description

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

Wei, Z & Ying, M 2006, 'Majorization In Quantum Adiabatic Algorithms', *Physical Review A*, vol. 74, no. 4, pp. 1-7.

#### View description

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 2005, 'Supervisory Control Of Fuzzy Discrete Event Systems', *IEEE Transactions on Systems, Man, and Cybernetic...*, vol. 35, no. 2, pp. 366-371.View/Download from: Publisher's site

#### View description

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

Feng, Y, Duan, R, Ji, Z-F & Ying, M 2005, 'Proof rules for purely quantum programs', *CoRR*, vol. abs/cs/0507043.

Li, S, Ying, M & Li, Y 2005, 'On Countable RCC Models', *Fundamenta Informaticae*, vol. 65, no. 4, pp. 329-351.

#### View description

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

Li, Y, Li, S & Ying, M 2005, 'Relational reasoning in the region connection calculus', *CoRR*, vol. abs/cs/0505041.

Sun, X, Duan, R & Ying, M 2005, 'The Existence Of Quantum Entanglement Catalysts', *IEEE Transactions On Information Theory*, vol. 51, no. 1, pp. 75-80.View/Download from: Publisher's site

#### View description

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

Ying, M 2005, 'A Theory Of Computation Based On Quantum Logic (I)', *Theoretical Computer Science*, vol. 344, no. 2-3, pp. 134-207.View/Download from: Publisher's site

#### View description

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

Ying, M 2005, 'A theory of computation based on quantum logic (I).', *Theor. Comput. Sci.*, vol. 344, pp. 134-207.

Ying, M 2005, 'Knowledge Transformation And Fusion In Diagnostic Systems', *Artificial Intelligence*, vol. 163, no. 1, pp. 1-45.View/Download from: Publisher's site

#### View description

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

Ying, M 2005, 'Pi-Calculus With Noisy Channels', *Acta Informatica*, vol. 41, no. 9, pp. 525-593.View/Download from: Publisher's site

#### View description

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

Feng, Y, Duan, R & Ying, M 2005, 'Catalyst-Assisted Probabilistic Entanglement Transformation', *IEEE Transactions On Information Theory*, vol. 51, no. 3, pp. 1090-1101.View/Download from: Publisher's site

#### View description

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 & Ying, M 2005, 'Entanglement-Assisted Transformation Is Asymptotically Equivalent To Multiple-Copy Transformation', *Physical Review A*, vol. 72, no. 2, pp. 1-5.

#### View description

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, 'Multiple-Copy Entanglement Transformation And Entanglement Catalysis', *Physical Review A*, vol. 71, no. 4, pp. 1-11.

#### View description

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

Duan, R, Feng, Y, Li, X & Ying, M 2005, 'Trade-Off Between Multiple-Copy Transformation And Entanglement Catalysis', *Physical Review A*, vol. 71, no. 6, pp. 1-7.

#### View description

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, Ji, Z & Ying, M 2005, 'Efficiency Of Deterministic Entanglement Transformation', *Physical Review A*, vol. 71, no. 2, pp. 1-7.

#### View description

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

Ji, Z, Cao, H & Ying, M 2005, 'Optimal Conclusive Discrimination Of Two States Can Be Achieved Locally', *Physical Review A*, vol. 71, no. 3, pp. 1-5.

#### View description

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

Ji, Z, Feng, Y & Ying, M 2005, 'Local Cloning Of Two Product States', *Physical Review A*, vol. 72, no. 3, pp. 1-5.

#### View description

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

Cao, H & Ying, M 2004, 'Local Discrimination Of Maximally Entangled States In Canonical Form', *Physics Letters A*, vol. 333, no. 3-4, pp. 232-234.View/Download from: Publisher's site

#### View description

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, YA, Duan, RY & Ying, MS 2004, 'Unambiguous discrimination between mixed quantum states', *PHYSICAL REVIEW A*, vol. 70, no. 1.View/Download from: Publisher's site

Li, S & Ying, M 2004, 'Generalized Region Connection Calculus', *Artificial Intelligence*, vol. 160, no. 1-2, pp. 1-34.View/Download from: Publisher's site

#### View description

The Region Connection Calculus (RCC) is one of the most widely referenced system of high-level (qualitative) spatial reasoning. RCC assumes a continuous representation of space. This contrasts sharply with the fact that spatial information obtained from physical recording devices is nowadays invariably digital in form and therefore implicitly uses a discrete representation of space. Recently, Galton developed a theory of discrete space that parallels RCC, but question still lies in that can we have a theory of qualitative spatial reasoning admitting models of discrete spaces as well as continuous spaces? In this paper we aim at establishing a formal theory which accommodates both discrete and continuous spatial information, and a generalization of Region Connection Calculus is introduced. GRCC, the new theory, takes two primitives: the mereological notion of part and the topological notion of connection. RCC and Galton's theory for discrete space are both extensions of GRCC. The relation between continuous models and discrete ones is also clarified by introducing some operations on models of GRCC. In particular, we propose a general approach for constructing countable RCC models as direct limits of collections of finite models. Compared with standard RCC models given rise from regular connected spaces, these countable models have the nice property that each region can be constructed in finite steps from basic regions. Two interesting countable RCC models are also given: one is a minimal RCC model, the other is a countable sub-model of the continuous space R2.

Qiu, D & Ying, M 2004, 'Characterizations Of Quantum Automata', *Theoretical Computer Science*, vol. 312, no. 2-3, pp. 479-489.View/Download from: Publisher's site

#### View description

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

Feng, Y & Ying, M 2004, 'Process Algebra Approach To Reasoning About Concurrent Actions', *Journal Of Computer Science And Technology*, vol. 19, no. 3, pp. 364-373.View/Download from: Publisher's site

#### View description

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.

Feng, Y, Duan, R & Ying, M 2004, 'When Catalysis Is Useful For Probabilistic Entanglement Transformation', *Physical Review A*, vol. 69, no. 6, pp. 1-5.

#### View description

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

Duan, R, Ji, Z, Feng, Y & Ying, M 2004, 'Quantum Operation Quantum Fourier Transform And Semi-Definite Programming', *Physics Letters A*, vol. 323, no. 1-2, pp. 48-56.View/Download from: Publisher's site

#### View description

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

Ji, Z, Duan, R & Ying, M 2004, 'Comparability Of Multipartite Entanglement', *Physics Letters A*, vol. 330, no. 6, pp. 418-423.View/Download from: Publisher's site

#### View description

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

Li, S & Ying, M 2003, 'Extensionality Of The RCC8 Composition Table', *Fundamenta Informaticae*, vol. 55, no. 3-4, pp. 363-385.

#### View description

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

Li, S & Ying, M 2003, 'Region Connection Calculus: Its models and composition table', *Artificial Intelligence*, vol. 145, no. 1-2, pp. 121-146.View/Download from: Publisher's site

#### View description

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.

Ying, M 2003, 'Reasoning About Probabilistic Sequential Programs In A Probabilistic Logic', *Acta Informatica*, vol. 39, no. 5, pp. 315-389.View/Download from: Publisher's site

#### View description

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, 'A Formal Model Of Computing With Words', *IEEE Transactions on Fuzzy Systems*, vol. 10, no. 5, pp. 640-652.View/Download from: Publisher's site

#### View description

Classical automata are formal models of computing with values. Fuzzy automata are generalizations of classical automata where the knowledge about the system's next state is vague or uncertain. It is worth noting that like classical automata, fuzzy automa

Ying, M 2002, 'Additive Models Of Probabilistic Processes', *Theoretical Computer Science*, vol. 275, no. 1-Feb, pp. 481-519.View/Download from: Publisher's site

#### View description

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

Ying, M 2002, 'Bisimulation Indexes And Their Applications', *Theoretical Computer Science*, vol. 275, no. 1-Feb, pp. 1-68.View/Download from: Publisher's site

#### View description

Bisimulation expresses the equivalence of processes whose external actions are identical. Sometimes we may meet two processes which are not exactly bisimilar but more or less bisimilar in the sense that whenever a process makes an action the other can ma

Ying, M 2002, 'Implication Operators In Fuzzy Logic', *IEEE Transactions on Fuzzy Systems*, vol. 10, no. 1, pp. 88-91.

#### View description

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 2002, 'Universal Quantum-Copying Machines: A Sufficient And Necessary Condition', *Physics Letters A*, vol. 302, no. 1, pp. 1-7.View/Download from: Publisher's site

#### View description

It was shown that the copying quality of the Wootters-Zurek quantum copying machine depends on the input states. So Buzek and Hillery proposed the notion of universal copying machine. A universal machine is a quantum copier whose copying quality is indep

Ying, M 2002, 'Wootters-Zurek Quantum-Copying Machine: The Higher-Dimensional Case', *Physics Letters A*, vol. 299, no. 2-Mar, pp. 107-115.View/Download from: Publisher's site

#### View description

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 & Wang, H 2002, 'Lattice-Theoretic Models Of Conjectures, Hypotheses And Consequences', *Artificial Intelligence*, vol. 139, no. 2, pp. 253-267.View/Download from: Publisher's site

#### View description

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

Zhang, S & Ying, M 2002, 'Set Discrimination Of Quantum States', *Physical Review A*, vol. 65, no. 6, pp. 1-5.

#### View description

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 & Ying, M 2002, 'Probabilistic Cloning And Deleting Of Quantum States', *Physical Review A*, vol. 65, no. 4, pp. 1-4.

#### View description

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

Feng, Y, Zhang, S, Duan, R & Ying, M 2002, 'Lower Bound On Inconclusive Probability Of Unambiguous Discrimination', *Physical Review A*, vol. 66, no. 6, pp. 1-4.

#### View description

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.

Feng, Y, Zhang, S, Sun, X & Ying, M 2002, 'Universal And Original-Preserving Quantum Copying Is Impossible', *Physics Letters A*, vol. 297, no. 1-Feb, pp. 1-3.View/Download from: Publisher's site

#### View description

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

Sun, X, Zhang, S, Feng, Y & Ying, M 2002, 'Mathematical Nature Of And A Family Of Lower Bounds For The Success Probability Of Unambiguous Discrimination', *Physical Review A*, vol. 65, no. 4, pp. 1-3.

#### View description

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

Ying, M 2001, 'Fuzzy Topology Based On Residuated Lattice-Valued Logic', *Acta Mathematica Sinica-English Series*, vol. 17, no. 1, pp. 89-102.

#### View description

We use a semantical method of complete residuated lattice-valued logic to give a generalization of fuzzy topology as a partial answer to a problem by Rosser and Turquette.

Ying, M & Wirsing, M 2001, 'Recursive Equations In Higher-Order Process Calculi', *Theoretical Computer Science*, vol. 266, no. 1-Feb, pp. 839-852.View/Download from: Publisher's site

#### View description

Regarding behaviour equivalence in higher-order process calculi, Sangiorgi (Inform. and Comput. 131 (1996) 141) and Thomsen (Inform. and Comput. 116 (1995) 38) introduced context and higher-order bisimulations, respectively. In this paper, uniqueness of

Zhang, S, Feng, Y, Sun, X & Ying, M 2001, 'Upper Bound For The Success Probability Of Unambiguous Discrimination Among Quantum States', *Physical Review A*, vol. 64, no. 6, pp. 1-3.

#### View description

One strategy to the discrimination problem is to identify the state with certainty, leaving a possibility of undecidability. This paper gives an upper bound for the maximal success probability of unambiguous discrimination among n states. This bound coin

Biacino, L, Gerla, G & Ying, M 2000, 'Approximate Reasoning Based On Similarity', *Mathematical Logic Quarterly*, vol. 46, no. 1, pp. 77-86.View/Download from: 3.0.CO;2-X">Publisher's site

#### View description

The connection between similarity logic and the theory of closure operators is examined. Indeed one proves that the consequence relation defined in [14] can be obtained by composing two closure operators and that the resulting operator is still a closure

Ying, M 2000, 'Automata Theory Based On Quantum Logic Ii', *International Journal Of Theoretical Physics*, vol. 39, no. 11, pp. 2545-2557.View/Download from: Publisher's site

#### View description

We establish the pumping lemma in automata theory based on quantum logic under certain conditions on implication, and discuss the recognizability by the product and union of orthomodular lattice-valued (quantum) automata. In particular, we show that the

Ying, M 2000, 'Automata Theory Based On Quantum Logic. (I)', *International Journal Of Theoretical Physics*, vol. 39, no. 4, pp. 985-995.View/Download from: Publisher's site

#### View description

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.

#### View description

We give two generalizations of Tarski's fixpoint theorem in the setting of residuated lattices and use them to establish van Emdem-Kowalski's least fixpoint semantics for residuated lattice-valued logic programs.

Ying, M 2000, 'Weak Confluence And Tau-Inertness', *Theoretical Computer Science*, vol. 238, no. 1-Feb, pp. 465-475.View/Download from: Publisher's site

#### View description

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 1999, 'A Shorter Proof To Uniqueness Of Solutions Of Equations', *Theoretical Computer Science*, vol. 216, no. 1-Feb, pp. 395-397.

#### View description

We give a very short proof of uniqueness of solutions of equations regarding observation congruence, the main notion of equality, over Milner's process calculus. (C) 1999-Elsevier Science B.V. All rights reserved.

Ying, M 1999, 'Perturbation Of Fuzzy Reasoning', *IEEE Transactions on Fuzzy Systems*, vol. 7, no. 5, pp. 625-629.

#### View description

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, 'Phase Semantics for a Pure Noncommutative Linear Propositional Logic', *Journal of Computer Science and Technology*, vol. 14, no. 2, pp. 135-139.View/Download from: Publisher's site

#### View description

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.

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

#### View description

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, MS & Liu, FC 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.

#### View description

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.

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.

#### View description

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 1998, 'Compactness In Fuzzy Logic', *Chinese Science Bulletin*, vol. 43, no. 14, pp. 1166-1171.View/Download from: Publisher's site

#### View description

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.

Ying, M & Bouchon-Meunier, B 1998, 'Approximate Reasoning With Linguistic Modifiers', *International Journal of Intelligent Systems*, vol. 13, no. 5, pp. 403-418.

#### View description

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 & Bouchon-Meunier, B 1997, 'Quantifiers, modifiers and qualifiers in fuzzy logic', *Journal of Applied Non-Classical Logics*, vol. 7, no. 3, pp. 335-342.View/Download from: Publisher's site

#### View description

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.

#### View description

NA

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.

#### View description

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 1996, 'When Is The Ideal Completion Of Abstract Basis Algebraic', *Theoretical Computer Science*, vol. 159, no. 2, pp. 355-356.

#### View description

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 1995, 'Institutions of variable truth values: An approach in the ordered style', *Journal of Computer Science and Technology*, vol. 10, no. 3, pp. 267-273.View/Download from: Publisher's site

#### View description

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 1995, 'Putting consistent theories together in institutions', *Journal of Computer Science and Technology*, vol. 10, no. 3, pp. 260-266.View/Download from: Publisher's site

#### View description

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 1994, 'A Logic For Approximate Reasoning', *Journal Of Symbolic Logic*, vol. 59, no. 3, pp. 830-837.View/Download from: Publisher's site

#### View description

NA

Ying, M 1994, 'On The Method Of Neighborhood-Systems In Fuzzy Topology', *Fuzzy Sets and Systems*, vol. 68, no. 2, pp. 227-238.View/Download from: Publisher's site

#### View description

In this paper, we revivify the theory of neighborhood systems in fuzzy topology with the method used to develop fuzzifying topology and find another kind of reasonable neighborhood structure in fuzzy topology except quasi-neighborhood systems of Pu and L

Ying, M 1993, 'A New Approach For Fuzzy Topology .3.', *Fuzzy Sets and Systems*, vol. 55, no. 2, pp. 193-207.View/Download from: Publisher's site

#### View description

The concepts of fuzzy continuity, product and quotient spaces are presented, and their fundamental properties are obtained in fuzzifying topology.

Ying, M 1993, 'Compactness In Fuzzifying Topology', *Fuzzy Sets and Systems*, vol. 55, no. 1, pp. 79-92.View/Download from: Publisher's site

#### View description

We introduce the concept of compactness and establish a generalization of Tychonoff's theorem in the framework of fuzzifying topology.

Ying, M 1993, 'Fuzzifying Topology Based On Complete Residuated Lattice-Valued Logic .1.', *Fuzzy Sets and Systems*, vol. 56, no. 3, pp. 337-373.View/Download from: Publisher's site

#### View description

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 1993, 'Fuzzifying Uniform-Spaces', *Fuzzy Sets and Systems*, vol. 53, no. 1, pp. 93-104.View/Download from: Publisher's site

#### View description

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 1992, 'A New Approach For Fuzzy Topology .2.', *Fuzzy Sets and Systems*, vol. 47, no. 2, pp. 221-232.View/Download from: Publisher's site

#### View description

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.

#### View description

NA

Ying, M 1992, 'Compactness, The Lowenheim-Skolem Property And The Direct-Product Of Lattices Of Truth Values', *Zeitschrift Fur Mathematische Logik Und Grundlag...*, vol. 38, no. 5-Jun, pp. 521-524.View/Download from: Publisher's site

#### View description

We show that compactness is preserved by arbitrary direct products of lattices of truth values and that the Lowenheim-Skolem property is preserved by finite direct products of lattices of truth values. MSC: 03C07, 03B50.

Ying, M 1992, 'Reasonableness Of The Compositional Rule Of Fuzzy Inference', *Fuzzy Sets and Systems*, vol. 36, no. 2, pp. 305-310.View/Download from: Publisher's site

#### View description

NA

Ying, M 1992, 'The Fundamental Theorem Of Ultraproduct In Pavelkas Logic', *Zeitschrift Fur Mathematische Logik Und Grundlag...*, vol. 38, no. 3, pp. 197-201.View/Download from: Publisher's site

#### View description

In [This Zeitschrift 25 (1979), 45-52, 119-134, 447-464], Pavelka systematically discussed propositional calculi with values in enriched residuated lattices and developed a general framework for approximate reasoning. In the first part of this paper we i

Ying, M 1991, 'A New Approach For Fuzzy Topology (I)', *Fuzzy Sets and Systems*, vol. 39, no. 3, pp. 303-321.View/Download from: Publisher's site

#### View description

We point out a new approach for fuzzy topology with fuzzy logic, and discuss the neighborhood structure of a point and the convergence of nets and filters in this new framework.

Ying, M 1991, 'Deduction Theorem For Many-Valued Inference', *Zeitschrift Fur Mathematische Logik Und Grundlag...*, vol. 37, no. 6, pp. 533-537.View/Download from: Publisher's site

#### View description

NA

Ying, M 1990, 'On Probabilistic Normed Spaces Under τT,L', *International Journal of Mathematics and Mathematical Sciences*, vol. 13, no. 4, pp. 731-736.View/Download from: Publisher's site

#### View description

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 1990, 'The Alternativity Measures Of Fuzzy-Sets', *Fuzzy Sets and Systems*, vol. 37, no. 1, pp. 105-110.View/Download from: Publisher's site

#### View description

NA

Ying, M 1989, 'On A Class Of Non-Causal Triangle Functions', *Mathematical Proceedings Of The Cambridge Philos...*, vol. 106, no. NA, pp. 467-469.

#### View description

NA

Ying, M 1989, 'On Epsilon-Fuzzy Sets', *Fuzzy Sets and Systems*, vol. 31, no. 1, pp. 123-129.View/Download from: Publisher's site

#### View description

NA

Ying, M 1988, 'Conjugate Transforms For Tau-T,L-Semigroups Of Distance Distribution-Functions', *Kexue Tongbao*, vol. 33, no. 23, pp. 2001-2002.

#### View description

NA

Ying, M 1988, 'On Standard Models Of Fuzzy Modal-Logics', *Fuzzy Sets and Systems*, vol. 26, no. 3, pp. 357-363.

#### View description

NA

Ying, M 1988, 'Report from Jiangxi Province, People's Republic of China', *Fuzzy Sets and Systems*, vol. 25, no. 3, p. 382.View/Download from: Publisher's site

Ying, M 1988, 'Some Notes On Multidimensional Fuzzy-Reasoning', *Cybernetics And Systems*, vol. 19, no. 4, pp. 281-293.

#### View description

NA

Ying, M 1987, 'A Counter-example Of Gottwald Theorem', *Fuzzy Sets and Systems*, vol. 23, no. 3, pp. 399-400.View/Download from: Publisher's site

#### View description

NA

Ying, M 1987, 'Fuzzy Semilattices', *Information Sciences*, vol. 43, no. 3, pp. 155-159.View/Download from: Publisher's site

#### View description

NA

Duan, R, Feng, Y & Ying, M, 'An Equivalence of Entanglement-Assisted Transformation and Multiple-Copy Entanglement Transformation'.

#### View description

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.

Yu, N & Ying, M, 'Non-Additivity of Minimum Output p-$\mathbf{R\acute{e}nyi}$ Entropy'.

#### View description

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

Liu, S, Wang, X, Zhou, L, Guan, J, Li, Y, He, Y, Duan, R & Ying, M 2018, 'Q| SI>: A Quantum Programing Environment' in *Symposium on Real-Time and Hybrid Systems (LVCS 11180)*, Springer, Switzerland, pp. 133-164.View/Download from: Publisher's site

#### View description

© Springer Nature Switzerland AG 2018. This paper describes a quantum programming environment, named Q| SI⟩, to support quantum programming using a quantum extension of the while -language. Embedded in the.Net framework, the Q| SI⟩ platform includes a quantum while -language compiler and a suite of tools to simulate quantum computation, optimize quantum circuits, analyze and verify quantum programs. This paper demonstrates Q| SI⟩ in use. Quantum behaviors are simulated on classical platforms with a combination of components and the compilation procedures for different back-ends are described in detail. Q| SI⟩ bridges the gap between quantum hardware and software. As a scalable framework, this platform allows users to code and simulate customized functions, optimize them for a range of quantum circuits, analyze the termination of a quantum program, and verify the program's correctness (The software of Q| SI⟩ is available at http://www.qcompiler.com.).

Ying, M 2016, 'Analysis of quantum programs' in *Foundations of Quantum Programming*, Elsevier, pp. 149-207.View/Download from: Publisher's site

Ying, M 2016, 'Logic for quantum programs' in *Foundations of Quantum Programming*, Elsevier, pp. 103-148.View/Download from: Publisher's site

Ying, M 2016, 'Preliminaries' in *Foundations of Quantum Programming*, Elsevier, pp. 11-58.View/Download from: Publisher's site

Ying, M 2016, 'Prospects' in *Foundations of Quantum Programming*, Elsevier, pp. 327-336.View/Download from: Publisher's site

Ying, M 2016, 'Quantum case statements' in *Foundations of Quantum Programming*, Elsevier, pp. 211-271.View/Download from: Publisher's site

Ying, M 2016, 'Quantum recursion' in *Foundations of Quantum Programming*, Elsevier, pp. 273-324.View/Download from: Publisher's site

Ying, M 2016, 'Syntax and semantics of quantum programs' in *Foundations of Quantum Programming*, Elsevier, pp. 61-102.View/Download from: Publisher's site

Su, G, Ying, M & Zhang, C 2010, 'An ADL-Approach to Specifying and Analyzing Centralized-Mode Architectural Connection' in Babar, MA & Gorton, I (eds), *Lecture Notes in Computer Science 6285 - Software Architecture*, Springer, Germany, pp. 8-23.View/Download from: Publisher's site

#### View description

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, Duan, R, Feng, Y & Ji, Z 2010, 'Predicate Transformer Semantics of Quantum Programs' in Gay, S & Mackie, I (eds), *Semantic Techniques in Quantum Computation*, Cambridge University Press, Cambridge, pp. 311-360.

#### View description

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.

Ying, M 2007, 'Quantum logic and automata theory' in Engesser, K, Gabbay, DM & Lehmann, D (eds), *Handbook of Quantum Logic and Quantum Structures*, Elsevier, London, UK, pp. 619-754.View/Download from: Publisher's site

#### View description

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.

Ying, M 2001, 'Bisimulation and Trace Limits of Agents' in *Topology in Process Calculus*, Springer New York, pp. 37-94.View/Download from: Publisher's site

Ying, M 2001, 'Bisimulation Indexes Induced by Metrics on Actions' in *Topology in Process Calculus*, Springer New York, pp. 139-206.View/Download from: Publisher's site

Ying, M 2001, 'Conclusion' in *Topology in Process Calculus*, Springer New York, pp. 207-211.View/Download from: Publisher's site

Ying, M 2001, 'Introduction' in *Topology in Process Calculus*, Springer New York, pp. 1-9.View/Download from: Publisher's site

Ying, M 2001, 'Limit Behavior of Agents' in *Topology in Process Calculus*, Springer New York, pp. 95-111.View/Download from: Publisher's site

Ying, M 2001, 'Near Bisimulations Defined by Closures' in *Topology in Process Calculus*, Springer New York, pp. 113-138.View/Download from: Publisher's site

Ying, M 2001, 'Process Calculus' in *Topology in Process Calculus*, Springer New York, pp. 11-36.View/Download from: Publisher's site

Ying, M 1999, 'Limits of Agents in Process Calculus' in *Fuzzy Logic and Soft Computing*, Springer US, pp. 221-240.View/Download from: Publisher's site

Barthe, G, Hsu, J, Ying, M, Yu, N & Zhou, L 2020, 'Relational proofs for quantum programs', *Proceedings of the ACM on Programming Languages*, Association for Computing Machinery (ACM), pp. 1-29.View/Download from: Publisher's site

Liu, J, Zhan, B, Wang, S, Ying, S, Liu, T, Li, Y, Ying, M & Zhan, N 2019, 'Formal verification of quantum algorithms using quantum hoare logic', *Computer Aided Verification*, International Conference on Computer Aided Verification, Springer, New York City, NY, USA, pp. 187-207.View/Download from: Publisher's site

#### View description

© The Author(s) 2019. We formalize the theory of quantum Hoare logic (QHL) [TOPLAS 33(6),19], an extension of Hoare logic for reasoning about quantum programs. In particular, we formalize the syntax and semantics of quantum programs in Isabelle/HOL, write down the rules of quantum Hoare logic, and verify the soundness and completeness of the deduction system for partial correctness of quantum programs. As preliminary work, we formalize some necessary mathematical background in linear algebra, and define tensor products of vectors and matrices on quantum variables. As an application, we verify the correctness of Grover's search algorithm. To our best knowledge, this is the first time a Hoare logic for quantum programs is formalized in an interactive theorem prover, and used to verify the correctness of a nontrivial quantum algorithm.

Zhou, L, Yu, N & Ying, M 2019, 'An Applied Quantum Hoare Logic', *PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19)*, 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) part of ACM's Federated Computing Research Conference (FCRC), ASSOC COMPUTING MACHINERY, Phoenix, AZ, pp. 1149-1162.View/Download from: Publisher's site

Liu, S, Wang, X, Zhou, L, Guan, J, Li, Y, He, Y, Duan, R & Ying, M 1970, 'Q vertical bar SI > : A Quantum Programming Environment', *SYMPOSIUM ON REAL-TIME AND HYBRID SYSTEMS: ESSAYS DEDICATED TO PROFESSOR CHAOCHEN ZHOU ON THE OCCASION OF HIS 80TH BIRTHDAY*, Symposium on Real-Time and Hybrid Systems, SPRINGER INTERNATIONAL PUBLISHING AG, Changsha, PEOPLES R CHINA, pp. 133-164.View/Download from: Publisher's site

Ying, M, Ying, S & Wu, X 2917, 'Invariants of quantum programs: Characterisations and generation', *Conference Record of the Annual ACM Symposium on Principles of Programming Languages*, ACM SIGPLAN Symposium on Principles of Programming Languages, ACM, Paris, France, pp. 818-832.View/Download from: Publisher's site

#### View description

© 2017 ACM. Program invariant is a fundamental notion widely used in program verification and analysis. The aim of this paper is twofold: (i) find an appropriate definition of invariants for quantum programs; and (ii) develop an effective technique of invariant generation for ver- ification and analysis of quantum programs. Interestingly, the no- tion of invariant can be defined for quantum programs in two d- ifferent ways - additive invariants and multiplicative invariants - corresponding to two interpretations of implication in a continuous valued logic: the £ukasiewicz implication and the Godel implica- tion. It is shown that both of them can be used to establish partial correctness of quantum programs. The problem of generating ad- ditive invariants of quantum programs is addressed by reducing it to an SDP (Semidefinite Programming) problem. This approach is applied with an SDP solver to generate invariants of two important quantum algorithms - quantum walk and quantum Metropolis sam- pling. Our examples show that the generated invariants can be used to verify correctness of these algorithms and are helpful in optimis- ing quantum Metropolis sampling. To our knowledge, this paper is the first attempt to define the notion of invariant and to develop a method of invariant generation for quantum programs.

Zhou, L & Ying, M 2017, 'Differential Privacy in Quantum Computation', *Proceedings - IEEE Computer Security Foundations Symposium*, IEEE Computer Security Foundations Symposium, IEEE, Santa Barbara, CA, USA, pp. 249-262.View/Download from: Publisher's site

#### View description

© 2017 IEEE. More and more quantum algorithms have been designed for solving problems in machine learning, database search and data analytics. An important problem then arises: how privacy can be protected when these algorithms are used on private data? For classical computing, the notion of differential privacy provides a very useful conceptual framework in which a great number of mechanisms that protect privacy by introducing certain noises into algorithms have been successfully developed. This paper defines a notion of differential privacy for quantum information processing. We carefully examine how the mechanisms using three important types of quantum noise, the amplitude/phase damping and depolarizing, can protect differential privacy. A composition theorem is proved that enables us to combine multiple privacy-preserving operations in quantum information processing.

Feng, Y & Ying, M 2015, 'Toward Automatic Verification of Quantum Cryptographic Protocols.', *CONCUR*, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 441-455.

Feng, Y & Ying, M 2015, 'Toward automatic verification of quantum cryptographic protocols', *Leibniz International Proceedings in Informatics, LIPIcs*, International Conference on Concurrency Theory, Springer, Spain, pp. 441-455.View/Download from: Publisher's site

#### View description

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

Li, Y & Ying, M 2014, '(Un)decidable problems about reachability of quantum systems', *Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)*, International Conference on Concurrency Theory, Springer, Rome, Italy, pp. 482-496.View/Download from: Publisher's site

#### View description

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', *Lecture Notes in Computer Science*, International Symposium on Mathematical Foundations of Computer Science, Springer, IST Austria, pp. 385-396.View/Download from: Publisher's site

#### View description

We introduce the notion of recursive quantum Markov chain (RQMC) for analysing recursive quantum programs with procedure calls. RQMCs are natural extension of Etessami and Yannakakiss recursive Markov chains where the probabilities along transitions are replaced by completely positive and trace-nonincreasing super-operators on a state Hilbert space of a quantum system. We study the reachability problem for RQMCs and establish a reduction from it to computing the least solution of a system of polynomial equations in the semiring of super-operators. It is shown that for an important subclass of RQMCs, namely linear RQMCs, the reachability problem can be solved in polynomial time. For general case, technique of Newtonian program analysis recently developed by Esparza, Kiefer and Luttenberger is employed to approximate reachability super-operators. A polynomial time algorithm that computes the support subspaces of the reachability super-operators in general case is also proposed.

Ying, M, Feng, Y & Yu, N 2013, 'Quantum information-flow security - noninterference and access control', *Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium*, IEEE Computer Security Foundations Symposium, IEEE Computer Society, Tulane University, New Orleans, Louisiana, USA, pp. 130-144.View/Download from: Publisher's site

#### View description

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

Ying, S, Feng, Y, Yu, N & Ying, M 2013, 'Reachability probabilities of quantum Markov chains', *Lecture Notes in Computer Science*, International Conference on Concurrency Theory, Springer, University of Buenos Aires, Argentina, pp. 334-348.View/Download from: Publisher's site

#### View description

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

Su, G, Ying, M & Zhang, C 2012, 'Semantic Analysis of Component-aspect Dynamism for Connector-based Architecture Styles', *2012 Joint Working Conference on Software Architecture & 6th European Conference on Software Architecture*, IEEE/IFIP Working Conference on Software Architecture (now with ECSA), IEEE Computer Society, Helsinki (Finland), pp. 151-160.View/Download from: Publisher's site

#### View description

Architecture Description Languages usually specify software architectures in the levels of types and instances. Components instantiate component types by parameterization and type conformance. Behavioral analysis of dynamic architectures needs to deal with the uncertainty of actual configurations of components, even if the type-level architectural descriptions are explicitly provided. This paper addresses this verification difficulty for connector-based architecture styles, in which all communication channels of a system are between components and a connector. The contribution of this paper is two-fold: (1) We propose a process-algebraic model, in which the main architectural concepts (such as component type and component conformance) and several fundamental architectural properties (i.e. deadlock-freedom, non-starvation, conservation, and completeness) are formulated. (2)We demonstrate that the state space of verification of these properties can be reduced from the entire universe of possible configurations to specific configurations that are fixed according to the typelevel architectural descriptions.

Yu, N & Ying, M 2012, 'Reachability and Termination Analysis of Concurrent Quantum Programs.', *CONCUR*, Springer, pp. 69-83.

Yu, N & Ying, M 2012, 'Reachability and Termination Analysis of Concurrent Quantum Programs', *Lecture Notes in Computer Science*, International Conference on Concurrency Theory, Sringer-Verlag, Newcastle upon Tyne, UK, pp. 69-83.View/Download from: Publisher's site

#### View description

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.

Zhang, H, Zhang, Y, Ying, M & Zhou, Y 2011, 'Translating first-order theories into logic programs', *IJCAI International Joint Conference on Artificial Intelligence*, International Joint Conference on Artificial Intelligence, AAAI Press, Barcelona, pp. 1126-1131.View/Download from: Publisher's site

#### View description

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.

Feng, Y, Duan, R & Ying, M 2011, 'Bisimulation for Quantum Processes', *Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming language*, ACM-SIGACT Symposium on Principles of Programming Languages, ACM, Austin, Texas, USA, pp. 523-534.View/Download from: Publisher's site

#### View description

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.

Ying, M 2010, 'Foundations of quantum programming', *Programming Languages and Systems 8th Asian Symposium, APLAS 2010*, Programming Languages and Systems, Springer-Verlag, Shanghai, China, pp. 16-20.View/Download from: Publisher's site

#### View description

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, H & Ying, M 2010, 'Decidable fragments of first-order language under stable model semantics and circumscription', *24th AAAI Conference on Artificial Intelligence 2010*, Conference on Artificial Intelligence, The AAAI Press, Atlanta, Georgia, pp. 375-380.

#### View description

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

Zhang, X, Liu, W, Li, S & Ying, M 2008, 'Reasoning with Cardinal Directions: An Efficient Algorithm', *Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence vol 1*, National Conference of the American Association for Artificial Intelligence, AAAI Press, Chicago, Illinois, USA, pp. 387-392.

#### View description

Direction relations between extended spatial objects are important commonsense knowledge. Recently, Goyal and Egenhofer proposed a formal model, called Cardinal Direction Calculus (CDC), for representing direction relations between connected plane regions. CDC is perhaps the most expressive qualitative calculus for directional information, and has attracted increasing interest from areas such as artificial intelligence, geographical information science, and image retrieval. Given a network of CDC constraints, the consistency problem is deciding if the network is realizable by connected regions in the real plane. This paper provides a cubic algorithm for checking consistency of basic CDC constraint networks. As one byproduct, we also show that any consistent network of CDC constraints has a canonical realization in digital plane. The cubic algorithm can also been adapted to cope with disconnected regions, in which case the current best algorithm is of time complexity O(n5).

Xia, L, Lang, J & Ying, M 2007, 'Sequential voting rules and multiple elections paradoxes', *Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2007*, pp. 279-288.View/Download from: Publisher's site

#### View description

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.

#### View description

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', *2005 IEEE International Conference On Granular Computing*, IEEE International Conference on Granular Computing, IEEE, Beijing, China, pp. 91-91.View/Download from: Publisher's site

#### View description

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.

#### View description

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.

#### View description

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.

#### View description

The author establishes an interesting result on multiquantified propositions. He then gives a novel method for interpreting linguistically quantified propositions with nearness measures.

Ying, MS 1986, 'FIRST ORDER FUZZY PREDICATE LOGIC (I).', *Proceedings of The International Symposium on Multiple-Valued Logic*, pp. 242-247.

#### View description

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.

Liu, S, Wang, X, Zhou, L, Guan, J, Li, Y, He, Y, Duan, R & Ying, M 2017, '$Q|SI\rangle$: A Quantum Programming Environment'.

#### View description

This paper describes a quantum programming environment, named $Q|SI\rangle$.

It is a platform embedded in the .Net language that supports quantum

programming using a quantum extension of the $\mathbf{while}$-language. The

framework of the platform includes a compiler of the quantum

$\mathbf{while}$-language and a suite of tools for simulating quantum

computation, optimizing quantum circuits, and analyzing and verifying quantum

programs. Throughout the paper, using $Q|SI\rangle$ to simulate quantum

behaviors on classical platforms with a combination of components is

demonstrated. The scalable framework allows the user to program customized

functions on the platform. The compiler works as the core of $Q|SI\rangle$

bridging the gap from quantum hardware to quantum software. The built-in

decomposition algorithms enable the universal quantum computation on the

present quantum hardware.

Liu, T, Li, Y, Wang, S, Ying, M & Zhan, N 2016, 'A Theorem Prover for Quantum Hoare Logic and Its Applications.'.

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

Ying, M 2014, 'Quantum Recursion and Second Quantisation: Basic Ideas and Examples.'.

#### View description

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.

Ying, M, Yu, N & Feng, Y 2014, 'Alternation in Quantum Programming: From Superposition of Data to Superposition of Programs.'.

#### View description

We extract a novel quantum programming paradigm - superposition of programs -

from the design idea of a popular class of quantum algorithms, namely quantum walkbased

algorithms. The generality of this paradigm is guaranteed by the universality

of quantum walks as a computational model. A new quantum programming language

QGCL is then proposed to support the paradigm of superposition of programs. This

language can be seen as a quantum extension of Dijkstra's GCL (Guarded Command

Language). Surprisingly, alternation in GCL splits into two different notions in the

quantum setting: classical alternation (of quantum programs) and quantum alternation,

with the latter being introduced in QGCL for the first time. Quantum alternation is the

key program construct for realizing the paradigm of superposition of programs.

The denotational semantics of QGCL are defined by introducing a new mathematical

tool called the guarded composition of operator-valued functions. Then the weakest

precondition semantics of QGCL can straightforwardly derived. Another very useful

program construct in realizing the quantum programming paradigm of superposition

of programs, called quantum choice, can be easily defined in terms of quantum alternation.

The relation between quantum choices and probabilistic choices is clarified

through defining the notion of local variables. We derive a family of algebraic laws

for QGCL programs that can be used in program verification, transformations and

compilation. The expressive power of QGCL is illustrated by several examples where

various variants and generalizations of quantum walks are conveniently expressed using

quantum alternation and quantum choice. We believe that quantum programming

with quantum alternation and choice will play an important role in further exploiting

the power of quantum computing.

Ying, M, Feng, Y & Yu, N 2013, 'Quantum Information-Flow Security: Noninterference and Access Control'.

Ying, M, Yu, N & Feng, Y 2012, 'Defining Quantum Control Flow'.

Ying, M 2011, 'Another Quantum Lovász Local Lemma'.

#### View description

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 2009, 'Hoare Logic for Quantum Programs'.

#### View description

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.

Wei, Z & Ying, M 2007, 'Linearity and Quantum Adiabatic Theorem'.

#### View description

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.

Wang, G & Ying, M 2006, 'Realization of positive-operator-valued measures by projective measurements without introducing ancillary dimensions'.

#### View description

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 2006, 'Quantum adiabatic evolutions that can't be used to design efficient algorithms'.

#### View description

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.

Wei, Z & Ying, M 2004, 'Quantum search algorithm by adiabatic evolution under a priori probability'.

#### View description

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.

Yu, N & Ying, M, 'Optimal simulation of three-qubit gates'.

#### View description

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.

#### Projects

**Selected projects**