# Professor Yuan Feng

**Professor,**A/DRsch Centre for Quantum Software and Information

**Core Member,**Centre for Quantum Software and Information

PhD (Tsinghua)

**Phone**

+61 2 9514 4479

**ORCID**

## Chapters

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

View/Download from: UTS OPUS

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

This chapter presents a systematic exposition of predicate transformer semantics for quantum programs. It is divided into two parts: The first part reviews the state transformer (forward) semantics of quantum programs according to Selingerâs suggestion of representing quantum programs by superoperators and elucidates DâHondt-Panangadenâs theory of quantum weakest preconditions in detail. In the second part, we develop a quite complete predicate transformer semantics of quantum programs based on Birkhoffâvon Neumann quantum logic by considering only quantum predicates expressed by projection operators. In particular, the universal coujunctivity and termination law of quantum programs are proved, and Hoareâs induction rule is established in the quantum setting.

## Conferences

Su, G., Chen, T., Feng, Y., Rosenblum, D.S. & Thiagarajan, P.S. 2016, 'An iterative decision-making scheme for markov decision processes and its application to self-adaptive systems',

View/Download from: Publisher's site

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

© Springer-Verlag Berlin Heidelberg 2016.Software is often governed by and thus adapts to phenomena that occur at runtime. Unlike traditional decision problems, where a decision-making model is determined for reasoning, the adaptation logic of such software is concerned with empirical data and is subject to practical constraints. We present an Iterative Decision-Making Scheme (IDMS) that infers both point and interval estimates for the undetermined transition probabilities in a Markov Decision Process (MDP) based on sampled data, and iteratively computes a confidently optimal scheduler from a given finite subset of schedulers. The most important feature of IDMS is the flexibility for adjusting the criterion of confident optimality and the sample size within the iteration, leading to a tradeoff between accuracy, data usage and computational overhead. We apply IDMS to an existing self-adaptation framework Rainbow and conduct a case study using a Rainbow system to demonstrate the flexibility of IDMS.

Li, Y., Song, L., Feng, Y. & Zhang, L. 2016, 'Verify LTL with Fairness Assumptions Efficiently',

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

*Proceedings of the International Symposium on Temporal Representation and Reasoning (TIME)*, 2016 23rd International Symposium on Temporal Representation and Reasoning (TIME), IEEE, Kongens Lyngby, Denmark, pp. 41-50.View/Download from: UTS OPUS or Publisher's site

© 2016 IEEE.This paper deals with model checking problems with respect to LTL properties under fairness assumptions. We first present an efficient algorithm to deal with a fragment of fairness assumptions and then extend the algorithm to handle arbitrary ones. Notably, by making use of some syntactic transformations, our algorithm avoids constructing corresponding Büchi automata for the whole fairness assumptions, which can be very large in practice. We implement our algorithm in NuSMV and consider a large selection of formulas. Our experiments show that in many cases our approach exceeds the automata-theoretic approach up to several orders of magnitude, in both time and memory.

Feng, Y., Hahn, E.M., Turrini, A. & Zhang, L. 2015, 'QPMC: A model checker for quantum programs and protocols',

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

*FM 2015: Formal Methods (LNCS)*, International Symposium on Formal Methods, Springer, Oslo; Norway, pp. 265-272.View/Download from: UTS OPUS or Publisher's site

© Springer International Publishing Switzerland 2015. We present QPMC (Quantum Program/Protocol Model Checker), an extension of the probabilistic model checker ISCASMC to automatically verify quantum programs and quantum protocols. QPMC distinguishes itself from the previous quantum model checkers proposed in the literature in that it works for general quantum programs and protocols, not only those using Clifford operations. A command-line version of QPMC is available at http://iscasmc.ios.ac.cn/tool/qmc/.

Song, L., Feng, Y. & Zhang, L. 2015, 'Planning for stochastic games with Co-safe objectives',

View/Download from: UTS OPUS

*Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)*, International Joint Conference on Artificial Intelligence, AAAI, Buenos Aires, pp. 1682-1688.View/Download from: UTS OPUS

We consider planning problems for stochastic games with objectives specified by a branching-time logic, called probabilistic computation tree logic (PCTL). This problem has been shown to be undecidable if strategies with perfect recall, i.e., history-dependent, are considered. In this paper, we show that, if restricted to co-safe properties, a subset of PCTL properties capable to specify a wide range of properties in practice including reachability ones, the problem turns to be decidable, even when the class of general strategies is considered. We also give an algorithm for solving robust stochastic planning, where a winning strategy is tolerant to some perturbations of probabilities in the model. Our result indicates that satisfiability of co-safe PCTL is decidable as well.

Feng, Y. & Ying, M. 2015, 'Toward automatic verification of quantum cryptographic protocols',

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

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

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

Zhou, C. & Feng, Y. 2015, 'Extend transferable belief models with probabilistic priors',

View/Download from: UTS OPUS

*Website Proceedings of UAI 2015*, Conference on Uncertainty in Artificial Intelligence, Association for Uncertainty in Artificial Intelligence (AUAI), Amsterdam, Netherlands, pp. 1-10.View/Download from: UTS OPUS

In this paper, we extend Smets' transferable belief
model (TBM) with probabilistic priors. Our
first motivation for the extension is about evidential
reasoning when the underlying prior knowledge
base is Bayesian. We extend standard
Dempster models with prior probabilities to represent
beliefs and distinguish between two types
of induced mass functions on an extended Dempster
model: one for believing and the other essentially
for decision-making. There is a natural
correspondence between these two mass functions.
In the extended model, we propose two
conditioning rules for evidential reasoning with
probabilistic knowledge base. Our second motivation
is about the partial dissociation of betting
at the pignistic level from believing at the credal
level in TBM. In our extended TBM, we coordinate
these two levels by employing the extended
Dempster model to represent beliefs at the credal
level. Pignistic probabilities are derived not from
the induced mass function for believing but from
the one for decision-making in the model and
hence need not rely on the choice of frame of discernment.
Moreover, we show that the above two
proposed conditionings and marginalization (or
coarsening) are consistent with pignistic transformation
in the extended TBM.

Song, L., Feng, Y. & Zhang, L. 2015, 'Decentralized Bisimulation for Multiagent Systems',

View/Download from: UTS OPUS

*AAMAS '15 Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems*, International Conference on Autonomous Agents and Multiagent Systems, Istanbul, pp. 209-217.View/Download from: UTS OPUS

The notion of bisimulation has been introduced as a powerful way to abstract from details of systems in the formal verification community. When applying to multiagent systems, classical bisimulations will allow one agent to make decisions based on full histories of others. Thus, as a general concept, classical bisimulations are unrealistically powerful for such systems. In this paper, we define a coarser notion of bisimulation under which an agent can only make realistic decisions based on information available to it. Our bisimulation still implies trace distribution equivalence of the systems, and moreover, it allows a compositional abstraction framework of reasoning about the systems.

Deng, Y., Feng, Y. & Dal Lago, U. 2015, 'On coinduction and quantum lambda calculi',

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

*Leibniz International Proceedings in Informatics, LIPIcs*, International Conference on Concurrency Theory, CONCUR 2015, Madrid; Spain, pp. 427-440.View/Download from: UTS OPUS or Publisher's site

In the ubiquitous presence of linear resources in quantum computation, program equivalence in linear contexts, where programs are used or executed once, is more important than in the classical setting. We introduce a linear contextual equivalence and two notions of bisimilarity, a state-based and a distribution-based, as proof techniques for reasoning about higher-order quantum programs. Both notions of bisimilarity are sound with respect to the linear contextual equivalence, but only the distribution-based one turns out to be complete. The completeness proof relies on a characterisation of the bisimilarity as a testing equivalence. © Yuxin Deng, Yuan Feng, and Ugo Dal Lago; licensed under Creative Commons License CC-BY.

Feng, Y. & Zhang, L. 2014, 'When Equivalence and Bisimulation Join Forces in Probabilistic Automata',

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

*Lecture Notes in Computer Science*, Int. Symp. on Formal Methods, Springer International Publishing, National University of Singapore, pp. 247-262.View/Download from: UTS OPUS or Publisher's site

Probabilistic automata were introduced by Rabin in 1963 as language acceptors. Two automata are equivalent if and only if they accept each word with the same probability. On the other side, in the process algebra community, probabilistic automata were re-proposed by Segala in 1995 which are more general than Rabin's automata. Bisimulations have been proposed for Segala's automata to characterize the equivalence between them. So far the two notions of equivalences and their characteristics have been studied most independently. In this paper, we consider Segala's automata, and propose a novel notion of distribution-based bisimulation by joining the existing equivalence and bisimilarities. Our bisimulation bridges the two closely related concepts in the community, and provides a uniform way of studying their characteristics. We demonstrate the utility of our definition by studying distribution-based bisimulation metrics, which gives rise to a robust notion of equivalence for Rabin's automata.

Feng, Y. & Zhang, L. 2014, 'A nearly optimal upper bound for the self-stabilization time in Herman's algorithm',

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

*Lecture Notes in Computer Science*, the 25th International Conference on Concurrency Theory (CONCUR'14), pp. 342-356.View/Download from: UTS OPUS or Publisher's site

Self-stabilization algorithms are very important in designing fault-tolerant distributed systems. In this paper we consider Herman's self-stabilization algorithm and study its expected self-stabilization time. McIver and Morgan have conjectured the optimal upper bound being 0.148N 2, where N denotes the number of processors. We present an elementary proof showing a bound of 0.167N2, a sharp improvement compared with the best known bound 0.521N2. Our proof is inspired by McIver and Morgan's approach: we find a nearly optimal closed form of the expected stabilization time for any initial configuration, and apply the Lagrange multipliers method to give an upper bound of it. © 2014 Springer-Verlag.

Chen, T., Feng, Y., Rosenblum, D.S. & Su, G. 2014, 'Perturbation analysis in verification of Discrete-time Markov Chains',

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

*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)*, 25th International Conference, CONCUR, Springer Verlag, Rome, Italy, pp. 218-233.View/Download from: UTS OPUS or Publisher's site

Perturbation analysis in probabilistic verification addresses the robustness and sensitivity problem for verification of stochastic models against qualitative and quantitative properties. We identify two types of perturbation bounds, namely non-asymptotic bounds and asymptotic bounds. Non-asymptotic bounds are exact, pointwise bounds that quantify the upper and lower bounds of the verification result subject to a given perturbation of the model, whereas asymptotic bounds are closed-form bounds that approximate non-asymptotic bounds by assuming that the given perturbation is sufficiently small. We perform perturbation analysis in the setting of Discrete-time Markov Chains. We consider three basic matrix norms to capture the perturbation distance, and focus on the computational aspect. Our main contributions include algorithms and tight complexity bounds for calculating both non-asymptotic bounds and asymptotic bounds with respect to the three perturbation distances. © 2014 Springer-Verlag.

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

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

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

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

Ying, M., Feng, Y. & Yu, N. 2013, 'Quantum information-flow security - noninterference and access control',

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

*Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium*, IEEE Computer Security Foundations Symposium, IEEE Computer Society, Tulane University, New Orleans, Louisiana, USA, pp. 130-144.View/Download from: UTS OPUS or Publisher's site

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

Ying, S., Feng, Y., Yu, N. & Ying, M. 2013, 'Reachability probabilities of quantum Markov chains',

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

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

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

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

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

*Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming language*, annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM, Austin, Texas, USA, pp. 523-534.View/Download from: UTS OPUS or Publisher's site

Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the other hand, quantum protocol designers may commit much more faults than classical protocol designers since human intuition is much better adapted to the classical world than the quantum world. To offer formal techniques for modeling and verification of quantum protocols, several quantum extensions of process algebra have been proposed. One of the most serious issues in quantum process algebra is to discover a quantum generalization of the notion of bisimulation, which lies in a central position in process algebra, preserved by parallel composition in the presence of quantum entanglement, which has no counterpart in classical computation. Quite a few versions of bisimulation have been defined for quantum processes in the literature, but in the best case they are only proved to be preserved by parallel composition of purely quantum processes where no classical communications are involved. Many quantum cryptographic protocols, however, employ the LOCC (Local Operations and Classical Communications) scheme, where classical communications must be explicitly specified. So, a notion of bisimulation preserved by parallel composition in the circumstance of both classical and quantum communications is crucial for process algebra approach to verification of quantum cryptographic protocols. In this paper we introduce a novel notion of bisimulation for quantum processes and prove that it is congruent with respect to various process algebra combinators including parallel composition even when both classical and quantum communications are present.We also establish some basic algebraic laws for this bisimulation.

## Journal articles

Su, G., Feng, Y., Chen, T. & Rosenblum, D.S. 2016, 'Asymptotic Perturbation Bounds for Probabilistic Model Checking with Empirically Determined Probability Parameters',

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

*IEEE Transactions on Software Engineering*, vol. 42, no. 7, pp. 623-639.View/Download from: UTS OPUS or Publisher's site

© 2015 IEEE.Probabilistic model checking is a verification technique that has been the focus of intensive research for over a decade. One important issue with probabilistic model checking, which is crucial for its practical significance but is overlooked by the state-of-the-art largely, is the potential discrepancy between a stochastic model and the real-world system it represents when the model is built from statistical data. In the worst case, a tiny but nontrivial change to some model quantities might lead to misleading or even invalid verification results. To address this issue, in this paper, we present a mathematical characterization of the consequences of model perturbations on the verification distance. The formal model that we adopt is a parametric variant of discrete-time Markov chains equipped with a vector norm to measure the perturbation. Our main technical contributions include a closed-form formulation of asymptotic perturbation bounds, and computational methods for two arguably most useful forms of those bounds, namely linear bounds and quadratic bounds. We focus on verification of reachability properties but also address automata-based verification of omega-regular properties. We present the results of a selection of case studies that demonstrate that asymptotic perturbation bounds can accurately estimate maximum variations of verification results induced by model perturbations.

Li, L. & Feng, Y. 2015, 'On hybrid models of quantum finite automata',

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

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

© 2015 Elsevier Inc. All rights reserved. In the literature, there exist several interesting hybrid models of quantum finite automata (QFA) which have both quantum and classical states. This paper describes these models in a uniform way: a hybrid QFA can be seen as a two-component communication system consisting of a quantum component and a classical one, and the existing hybrid QFA differ from each other mainly in the specific communication pattern: classical-quantum, or quantum-classical, or two-way. We clarify the relationship between these hybrid QFA and some other models; in particular, it is shown that hybrid QFA can be simulated exactly by QFA with general quantum operations. As corollaries, some results in the literature concerning the language recognition power and the equivalence problem of hybrid QFA follow directly from these relationships clarified in this paper.

Chen, W., Cao, Y., Wang, H. & Feng, Y. 2015, 'Minimum guesswork discrimination between quantum states',

View/Download from: UTS OPUS

*Quantum Information & Computation*, vol. 15, no. 9-10, pp. 737-758.View/Download from: UTS OPUS

Error probability is a popular and well-studied optimization criterion in
discriminating non-orthogonal quantum states. It captures the threat from an
adversary who can only query the actual state once. However, when the adversary
is able to use a brute-force strategy to query the state, discrimination
measurement with minimum error probability does not necessarily minimize the
number of queries to get the actual state. In light of this, we take Massey's
guesswork as the underlying optimization criterion and study the problem of
minimum guesswork discrimination. We show that this problem can be reduced to a
semidefinite programming problem. Necessary and sufficient conditions when a
measurement achieves minimum guesswork are presented. We also reveal the
relation between minimum guesswork and minimum error probability. We show that
the two criteria generally disagree with each other, except for the special
case with two states. Both upper and lower information-theoretic bounds on
minimum guesswork are given. For geometrically uniform quantum states, we
provide sufficient conditions when a measurement achieves minimum guesswork.
Moreover, we give the necessary and sufficient condition under which making no
measurement at all would be the optimal strategy.

Feng, Y. & Zhang, L. 2015, 'A nearly optimal upper bound for the self-stabilization time in Herman's algorithm',

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

*Distributed Computing*, vol. 28, pp. 233-244.View/Download from: UTS OPUS or Publisher's site

Self-stabilization algorithms are very important in designing fault-tolerant distributed systems. In this paper we consider Herman's self-stabilization algorithm and study its expected termination time. McIver and Morgan have conjectured the optimal upper bound being (Formula presented.), where (Formula presented.) denotes the number of processors. We present an elementary proof showing a bound of (Formula presented.), a sharp improvement compared with the best known bound (Formula presented.). Our proof is inspired by McIver and Morgan's approach: we find a nearly optimal closed form of the expected stabilization time for any initial configuration, and apply the Lagrange multipliers method to give an upper bound.

Li, L. & Feng, Y. 2015, 'Quantum Markov chains: Description of hybrid systems, decidability of equivalence, and model checking linear-time properties',

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

*Information and Computation*, vol. 244, pp. 229-244.View/Download from: UTS OPUS or Publisher's site

© 2015 Elsevier Inc.In this paper, we study a model of quantum Markov chains that is a quantum analogue of Markov chains and is obtained by replacing probabilities in transition matrices with quantum operations. We show that this model is very suited to describe hybrid systems that consist of a quantum component and a classical one. Indeed, hybrid systems are often encountered in quantum information processing. Thus, we further propose a model called hybrid quantum automata (HQA) that can be used to describe the hybrid systems receiving inputs (actions) from the outer world. We show the language equivalence problem of HQA is decidable in polynomial time. Furthermore, we apply this result to the trace equivalence problem of quantum Markov chains, and thus it is also decidable in polynomial time. Finally, we discuss model checking linear-time properties of quantum Markov chains, and show the quantitative analysis of regular safety properties can be addressed successfully.

Ying, M., Li, Y., Yu, N. & Feng, Y. 2014, 'Model-Checking Linear-Time Properties of Quantum Systems',

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

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

Feng, Y., Deng, Y. & Ying, M. 2014, 'Symbolic Bisimulation for Quantum Processes.',

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

*ACM Trans. Comput. Log.*, vol. 15, pp. 14-14.View/Download from: UTS OPUS or Publisher's site

Feng, Y., Yu, N. & Ying, M. 2013, 'Model Checking Quantum Markov Chains',

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

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

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

Feng, Y. & Zhang, L. 2013, 'A Tighter Bound For The Self-stabilization Time In Herman's Algorithm',

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

*Information Processing Letters*, vol. 113, no. 13, pp. 486-488.View/Download from: UTS OPUS or Publisher's site

We study the expected self-stabilization time of Herman's algorithm. For N processors the lower bound is 4/27N(2) (0.148N(2)), and an upper bound of 0.64N(2) is presented in Kiefer et al. (2011) [4]. In this paper we give a tighter upper bound 0.521N(2).

Ying, M., Yu, N., Feng, Y. & Duan, R. 2013, 'Verification of quantum programs',

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

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

This paper develops verification methodology for quantum programs, and the contribution of the paper is two-fold. Sharir, Pnueli and Hart [M. Sharir, A. Pnueli, S. Hart, Verification of probabilistic programs, SIAM Journal of Computing 13 (1984) 292314] presented a general method for proving properties of probabilistic programs, in which a probabilistic program is modeled by a Markov chain and an assertion on the output distribution is extended to an invariant assertion on all intermediate distributions. Their method is essentially a probabilistic generalization of the classical Floyd inductive assertion method. In this paper, we consider quantum programs modeled by quantum Markov chains which are defined by super-operators. It is shown that the SharirPnueliHart method can be elegantly generalized to quantum programs by exploiting the SchrödingerHeisenberg duality between quantum states and observables. In particular, a completeness theorem for the SharirPnueliHart verification method of quantum programs is established.

Ying, M., Feng, Y., Duan, R., Li, Y. & Yu, N. 2012, 'Quantum Programming: From Theories To Implementations',

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

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

This paper surveys the new field of programming methodology and techniques for future quantum computers, including design of sequential and concurrent quantum programming languages, their semantics and implementations. Several verification methods for qu

Feng, Y., Duan, R. & Ying, M. 2012, 'Bisimulation For Quantum Processes',

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

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

Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the oth

Deng, Y. & Feng, Y. 2012, 'Open Bisimulation for Quantum Processes',

*CoRR*, vol. abs/1201.0416. Ying, M. & Feng, Y. 2011, 'A Flowchart Language For Quantum Programming',

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

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

Several high-level quantum programming languages have been proposed in the previous research. In this paper, we define a low-level flowchart language for quantum programming, which can be used in implementation of high-level quantum languages and in desi

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

View/Download from: Publisher's site

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

Ying, M. & Feng, Y. 2010, 'Quantum loop programs',

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

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

Loop is a powerful program construct in classical computation, but its power is still not exploited fully in quantum computation. The exploitation of such power definitely requires a deep understanding of the mechanism of quantum loop programs. In this paper, we introduce a general scheme of quantum loops and describe its computational process. The function computed by a quantum loop is defined, and a denotational semantics and a weakest precondition semantics of a quantum loop are given. The notions of termination and almost termination are proposed for quantum loops. This paper only consider the case of finite-dimensional state spaces. Necessary and sufficient conditions for termination and almost termination of a general quantum loop on any mixed input state are presented. A quantum loop is said to be (almost) terminating if it (almost) terminates on any input state. We show that a quantum loop is almost terminating if and only if it is uniformly almost terminating. It is observed that a small disturbance either on the unitary transformation in the loop body or on the measurement in the loop guard can make any quantum loop (almost) terminating, provided that some dimension restriction is satisfied. Moreover, a representation of the function computed by a quantum loop is given in terms of finite summations of matrices. To illustrate the notions and results obtained in this paper, two simple classes of quantum loop programs, one qubit quantum loops, and two qubit quantum loops defined by controlled gates, are carefully examined, and to show their expressive power, quantum loops are applied in describing quantum walks.

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

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

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

In this paper, we study the distinguishability of multipartite quantum states by separable operations. We first present a necessary and sufficient condition for a finite set of orthogonal quantum states to be distinguishable by separable operations. An analytical version of this condition is derived for the case of (D - 1) pure states, where D is the total dimension of the state space under consideration. A number of interesting consequences of this result are then carefully investigated. Remarkably, we show there exists a large class of 2 circle times 2 separable operations not being realizable by local operations and classical communication. Before our work, only a class of 3 circle times 3 nonlocal separable operations was known [Bennett et al, Phys. Rev. A 59, 1070 (1999)]. We also show that any basis of the orthogonal complement of a multipartite pure state is indistinguishable by separable operations if and only if this state cannot be a superposition of one or two orthogonal product states, i.e., has an orthogonal Schmidt number not less than three, thus generalize the recent work about indistinguishable bipartite subspaces [Watrous, Phys. Rev. Lett. 95, 080505 (2005)]. Notably, we obtain an explicit construction of indistinguishable subspaces of dimension 7 (or 6) by considering a composite quantum system consisting of two qutrits (resp., three qubits), which is slightly better than the previously known indistinguishable bipartite subspace with dimension 8.

Ying, M., Feng, Y., Duan, R. & Ji, Z. 2009, 'An Algebra Of Quantum Processes',

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

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

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

Ying, M. & Feng, Y. 2009, 'An Algebraic Language For Distributed Quantum Computing',

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

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

A classical circuit can be represented by a circuit graph or equivalently by a Boolean expression. The advantage of a circuit graph is that it can help us to obtain an intuitive understanding of the circuit under consideration, whereas the advantage of a Boolean expression is that it is suited to various algebraic manipulations. In the literature, however, quantum circuits are mainly drawn as circuit graphs, and a formal language for quantum circuits that has a function similar to that of Boolean expressions for classical circuits is still missing. Certainly, quantum circuit graphs will become unmanageable when complicated quantum computing problems are encountered, and in particular, when they have to be solved by employing the distributed paradigm where complex quantum communication networks are involved. In this paper, we design an algebraic language for formally specifying quantum circuits in distributed quantum computing. Using this language, quantum circuits can be represented in a convenient and compact way, similar to the way in which we use Boolean expressions in dealing with classical circuits. Moreover, some fundamental algebraic laws for quantum circuits expressed in this language are established. These laws form a basis of rigorously reasoning about distributed quantum computing and quantum communication protocols.

Feng, Y. & Shi, Y. 2009, 'Characterising Locally Indistinguishable Orthogonal Product States',

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

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

Bennett et al [Physical Review A, vol.59, no. 2, p. 1070, 1999] identified a set or orthogonal product states in the Hilbert space C-3 circle times C-3 such that reliably distinguishing those states requires nonlocal quantum operations. While more examples have been found for this counterintuitive "nonlocality without entanglement" phenomenon, a complete and computationally verifiable characterization for all such sets of states remains unknown. In this paper, we give such a characterization for both C-3 circle times C-3 and C-2 circle times C-2 circle times C-2. As a consequence, we show that in both spaces, there is no additional set of a fundamentally different structure than those of the known instances.

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

View/Download from: UTS OPUS

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

Multipartite quantum states that cannot be uniquely determined by their reduced states of all proper subsets of the parties exhibit some inherit `high-order' correlation. This paper elaborates this issue by giving necessary and sufficient conditions for a pure multipartite state to be locally undetermined, and moreover, characterizing precisely all the pure states sharing the same set of reduced states with it. Interestingly, local determinability of pure states is closely related to a generalized notion of Schmidt decomposition. Furthermore, we find that locally undetermined states have some applications to the well-known consensus problem in distributed computation. To be specific, given some physically separated agents, when communication between them, either classical or quantum, is unreliable and they are not allowed to use local ancillary quantum systems, then there exists a totally correct and completely fault-tolerant protocol for them to reach a consensus if and only if they share a priori a locally undetermined quantum state

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

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

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

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

Duan, R., Feng, Y. & Ying, M. 2008, 'Local Distinguishability Of Multipartite Unitary Operations',

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

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

We show that any two different unitary operations acting on an arbitrary multipartite quantum system can be perfectly distinguished by local operations and classical communication when a finite number of runs is allowed. Intuitively, this result indicate

Ying, M., Chen, J.F., Feng, Y. & Duan, R. 2007, 'Commutativity Of Quantum Weakest Preconditions',

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

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

The notion of quantum weakest precondition was introduced by D'Hondt and P. Panangaden [E. D'Hondt, P. Panangaden, Quantum weakest preconditions, Mathematical Structures in Computer Science 16 (2006) 429-451], and they presented a representation of weake

Duan, R., Feng, Y., Ji, Z. & Ying, M. 2007, 'Distinguishing Arbitrary Multipartite Basis Unambiguously Using Local Operations And Classical Communication',

View/Download from: UTS OPUS

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

We show that an arbitrary basis of a multipartite quantum state space consisting of K distant parties such that the kth party has local dimension d(k) always contains at least N=Sigma(K)(k=1)(d(k)-1)+1 members that are unambiguously distinguishable using

Duan, R., Feng, Y. & Ying, M. 2007, 'Entanglement Is Not Necessary For Perfect Discrimination Between Unitary Operations',

View/Download from: UTS OPUS

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

We show that a unitary operation (quantum circuit) secretly chosen from a finite set of unitary operations can be determined with certainty by sequentially applying only a finite amount of runs of the unknown circuit. No entanglement or joint quantum ope

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

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

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

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

Feng, Y., Duan, R., Ji, Z. & Ying, M. 2007, 'Proof Rules For The Correctness Of Quantum Programs',

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

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

We apply the notion of quantum predicate proposed by D'Hondt and Panangaden to analyze a simple language fragment which may describe the quantum part of a future quantum computer in Knill's architecture. The notion of weakest liberal precondition semanti

Duan, R., Feng, Y., Ji, Z. & Ying, M. 2007, 'Distinguishing arbitrary multipartite basis unambiguously using local operations and classical communication (vol 98, art no 230602, 2007)',

View/Download from: Publisher's site

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

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

View/Download from: Publisher's site

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

Ji, Z., Feng, Y., Duan, R. & Ying, M. 2006, 'Boundary Effect Of Deterministic Dense Coding',

View/Download from: UTS OPUS

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

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

Ji, Z., Feng, Y., Duan, R. & Ying, M. 2006, 'Identification And Distance Measures Of Measurement Apparatus',

View/Download from: UTS OPUS

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

We propose simple schemes that can perfectly identify projective measurement apparatuses secretly chosen from a finite set. Entanglement is used in these schemes both to make possible the perfect identification and to improve the efficiency significantly

Feng, Y., Duan, R. & Ji, Z. 2006, 'Optimal Dense Coding With Arbitrary Pure Entangled States',

View/Download from: UTS OPUS

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

We examine dense coding with an arbitrary pure entangled state sharing between the sender and the receiver. Upper bounds on the average success probability in approximate dense coding and on the probability of conclusive results in unambiguous dense codi

Duan, R., Feng, Y. & Ying, M. 2006, 'Partial Recovery Of Quantum Entanglement',

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

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

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

Feng, Y., Duan, R. & Ying, M. 2006, 'Relation Between Catalyst-Assisted Transformation And Multiple-Copy Transformation For Bipartite Pure States',

View/Download from: UTS OPUS

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

We show that in some cases, catalyst-assisted entanglement transformation cannot be implemented by multiple-copy transformation for pure states. This fact, together with the result we obtained in R. Y. Duan, Y. Feng, X. Li, and M. S. Ying, Phys. Rev. A 7

Duan, R., Ji, Z., Feng, Y. & Ying, M. 2006, 'Some Issues In Quantum Information Theory',

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

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

Quantum information theory is a new interdisciplinary research field related to quantum mechanics, computer science, information theory, and applied mathematics. It provides completely new paradigms to do information processing tasks by employing the pri

Zhang, C., Feng, Y. & Ying, M. 2006, 'Unambiguous Discrimination Of Mixed Quantum States',

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

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

The problem of unambiguous discrimination between mixed quantum states is addressed by isolating the part of each mixed state which has no contribution to discrimination and by employing the strategy of set discrimination of pure states. A necessary and

Feng, Y., Duan, R. & Ying, M. 2005, 'Catalyst-Assisted Probabilistic Entanglement Transformation',

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

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

We are concerned with catalyst-assisted probabilistic entanglement transformations. A necessary and sufficient condition is presented under which there exist partial catalysts that can increase the maximal transforming probability of a given entanglement

Feng, Y., Duan, R. & Ji, Z. 2005, 'Condition And Capability Of Quantum State Separation',

View/Download from: UTS OPUS

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

The linearity of quantum operations puts many fundamental constraints on the information processing tasks we can achieve on a quantum system whose state is not exactly known, just as we observe in quantum cloning and quantum discrimination. In this paper

Duan, R., Feng, Y., Ji, Z. & Ying, M. 2005, 'Efficiency Of Deterministic Entanglement Transformation',

View/Download from: UTS OPUS

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

We prove that sufficiently many copies of a bipartite entangled pure state can always be transformed into some copies of another one with certainty by local quantum operations and classical communication. The efficiency of such a transformation is charac

Ji, Z., Feng, Y. & Ying, M. 2005, 'Local Cloning Of Two Product States',

View/Download from: UTS OPUS

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

Local quantum operations and classical communication (LOCC) put considerable constraints on many quantum information processing tasks such as cloning and discrimination. Surprisingly, however, discrimination of any two pure states survives such constrain

Duan, R., Feng, Y., Li, X. & Ying, M. 2005, 'Multiple-Copy Entanglement Transformation And Entanglement Catalysis',

View/Download from: UTS OPUS

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

We prove that any multiple-copy entanglement transformation [S. Bandyopadhyay, V. Roychowdhury, and U. Sen, Phys. Rev. A 65, 052315 (2002)] can be implemented by a suitable entanglement-assisted local transformation [D. Jonathan and M. B. Plenio, Phys. R

Duan, R., Feng, Y., Li, X. & Ying, M. 2005, 'Trade-Off Between Multiple-Copy Transformation And Entanglement Catalysis',

View/Download from: UTS OPUS

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

We demonstrate that multiple copies of a bipartite entangled pure state may serve as a catalyst for certain entanglement transformations while a single copy cannot. Such a state is termed a

Duan, R., Feng, Y. & Ying, M. 2005, 'Entanglement-Assisted Transformation Is Asymptotically Equivalent To Multiple-Copy Transformation',

View/Download from: UTS OPUS

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

We show that two ways of manipulating quantum entanglement-namely, entanglement-assisted local transformation [D. Jonathan and M. B. Plenio, Phys. Rev. Lett. 83, 3566 (1999)] and multiple-copy transformation [S. Bandyopadhyay, V. Roychowdhury, and U. Sen

Feng, Y. & Ying, M. 2004, 'Process Algebra Approach To Reasoning About Concurrent Actions',

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

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

A reasonable transition rule is proposed for synchronized actions and some equational properties of bisimilarity and weak bisimilarity in the process algebra for reasoning about concurrent actions are presented.

Duan, R., Ji, Z., Feng, Y. & Ying, M. 2004, 'Quantum Operation Quantum Fourier Transform And Semi-Definite Programming',

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

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

We analyze a class of quantum operations based on a geometrical representation of d-level quantum system (or qudit for short). A sufficient and necessary condition of complete positivity, expressed in terms of the quantum Fourier transform, is found for

Feng, Y., Duan, R. & Ying, M. 2004, 'When Catalysis Is Useful For Probabilistic Entanglement Transformation',

View/Download from: UTS OPUS

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

We determine all 2x2 quantum states that can serve as useful catalysts for a given probabilistic entanglement transformation, in the sense that they can increase the maximal transformation probability. When higher-dimensional catalysts are considered, a

Feng, Y., Zhang, S., Duan, R. & Ying, M. 2002, 'Lower Bound On Inconclusive Probability Of Unambiguous Discrimination',

View/Download from: UTS OPUS

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

We derive a lower bound on the inconclusive probability of unambiguous discrimination among n linearly independent quantum states by using the constraint of no signaling. It improves the bound presented in the. paper of Zhang, Feng, Sun, and Ying [Phys.

Sun, X., Zhang, S., Feng, Y. & Ying, M. 2002, 'Mathematical Nature Of And A Family Of Lower Bounds For The Success Probability Of Unambiguous Discrimination',

View/Download from: UTS OPUS

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

Unambiguous discrimination is a strategy to the discrimination problem that identifies the state with certainty, leaving a possibility of undecidability. This paper points out that the optimal success probability of unambiguous discrimination is mathemat

Feng, Y., Zhang, S. & Ying, M. 2002, 'Probabilistic Cloning And Deleting Of Quantum States',

View/Download from: UTS OPUS

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

We construct a probabilistic cloning and deleting machine which, taking several copies of an input quantum state, can output a linear superposition of multiple cloning and deleting states. Since the machine can perform cloning and deleting in a single un

Feng, Y., Zhang, S., Sun, X. & Ying, M. 2002, 'Universal And Original-Preserving Quantum Copying Is Impossible',

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

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

We show that an arbitrary quantum state cannot be universally 1 --> 2 copied keeping the original copy unchanged. Indeed, the density operator of the additional copy after the copying transformation is nothing but the scale product of the identity matrix

Zhang, S., Feng, Y., Sun, X. & Ying, M. 2001, 'Upper Bound For The Success Probability Of Unambiguous Discrimination Among Quantum States',

View/Download from: UTS OPUS

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

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

Quantum processes describe concurrent communicating systems that may involve
quantum information. We propose a notion of open bisimulation for quantum
processes and show that it provides both a sound and complete proof methodology
for a natural extensional behavioural equivalence between quantum processes. We
also give a modal characterisation of open bisimulation, by extending the
Hennessy-Milner logic to a quantum setting.

**Selected Peer-Assessed Projects**