UTS site search

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

Chapters

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/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', Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Fundamental Approaches to Software Engineering (FASE), Springer, Eindhoven, The Netherlands, 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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.
Chen, W., Gao, Y., Wang, H. & Feng, Y. 2015, 'MINIMUM GUESSWORK DISCRIMINATION BETWEEN QUANTUM STATES', QUANTUM INFORMATION & COMPUTATION, vol. 15, no. 9-10, pp. 737-758.
Feng, Y., Deng, Y. & Ying, M. 2014, 'Symbolic bisimulation for quantum processes', ACM Transactions on Computational Logic (TOCL), vol. 15, pp. 14-14.
View/Download from: UTS OPUS
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: UTS OPUS or Publisher's site
Feng, Y., Deng, Y. & Ying, M. 2014, 'Symbolic Bisimulation for Quantum Processes.', 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', 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', 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', 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', 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', 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', 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', ACM SIGPLAN NOTICES, vol. 46, no. 1, pp. 523-534.
View/Download from: Publisher's site
Ying, M. & Feng, Y. 2010, 'Quantum loop programs', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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)', 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)', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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', 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
Deng, Y. & Feng, Y., 'Open Bisimulation for Quantum Processes'.
View/Download from: UTS OPUS
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.