## Biography

Prof Yuan Feng received his Bachelor of Science and Ph.D. in Computer Science from Tsinghua University, China in 1999 and 2004, respectively. He is currently a professor at the Centre for Quantum Software and Information (QSI), University of Technology Sydney (UTS), Australia. Before joining UTS in 2009, he was an associate professor at Tsinghua University. His research interests include quantum information and quantum computation, quantum programming theory, and probabilistic systems.

Prof Feng has published more than 70 research papers in international top journals and mainstream conferences. These include eight publications in the prestigious IEEE Transactions journals (five in IEEE-TIT, two in IEEE-TSE, and one in IEEE-TC, all being the pre-eminent journals in their respective areas), five publications in PRL (Physical Review Letters, one of the most prestigious physics journals), four in ACM Transactions journals (three in ACM-TOCL, the pre-eminent journal in computational logic, and one in ACM-TOPLAS, the most prestigious journal in programming theory. TOPLAS only accepts the very best papers of the year, and publishes less than 20 papers each year), one at POPL, the most prestigious international conference in programming language theory, and six at CONCUR, the most prestigious international conference in concurrency theory. He was awarded an ARC (Australian Research Council) Future Fellowship, four Australian Research Council (ARC) discovery grants, and two international research grants over the last 10 years.

#### Can supervise: YES

#### Publications

Zhou, X, Li, S & Feng, Y 2020, 'Quantum Circuit Transformation Based on Simulated Annealing and Heuristic Search', *IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems*.View/Download from: Publisher's site

#### View description

IEEE Quantum algorithm design usually assumes access to a perfect quantum computer with ideal properties like full connectivity, noise-freedom and arbitrarily long coherence time. In Noisy Intermediate-Scale Quantum (NISQ) devices, however, the number of qubits is highly limited and quantum operation error and qubit coherence are not negligible. Besides, the connectivity of physical qubits in a quantum processing unit (QPU) is also strictly constrained. Thereby, additional operations like SWAP gates have to be inserted to satisfy this constraint while preserving the functionality of the original circuit. This process is known as quantum circuit transformation. Adding additional gates will increase both the size and depth of a quantum circuit and therefore cause further decay of the performance of a quantum circuit. Thus it is crucial to minimize the number of added gates. In this paper, we propose an efficient method to solve this problem. We first choose by using simulated annealing an initial mapping which fits well with the input circuit and then, with the help of a heuristic cost function, stepwise apply the best selected SWAP gates until all quantum gates in the circuit can be executed. Our algorithm runs in time polynomial in all parameters including the size and the qubit number of the input circuit, and the qubit number in the QPU. Its space complexity is quadratic to the number of edges in the QPU. Experimental results on extensive realistic circuits confirm that the proposed method is efficient and the number of added gates of our algorithm is, on average, only 57% of that of state-of-the-art algorithms on IBM Q20 (Tokyo), the most recent IBM quantum device.

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

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

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

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

#### View description

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

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

#### View description

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

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

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

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

Deng, Y & Feng, Y 2017, 'Probabilistic bisimilarity as testing equivalence', *Information and Computation*, vol. 257, pp. 58-64.View/Download from: Publisher's site

#### View description

© 2017 Elsevier Inc. Larsen and Skou initiated the study of probabilistic bisimilarity and its characterisation in terms of tests. Later on, van Breugel et al. showed that, for labelled Markov processes with continuous state spaces, probabilistic bisimilarity nicely coincides with a simple notion of testing equivalence. Their proof employs advanced machinery from topology. In the discrete case of finite-state reactive probabilistic processes, we prove that coincidence result with an elementary and more accessible proof.

Feng, Y & Zhang, L 2017, 'Precisely deciding CSL formulas through approximate model checking for CTMCs', *Journal of Computer and System Sciences*, vol. 89, pp. 361-371.View/Download from: Publisher's site

#### View description

© 2017 Elsevier Inc. The model checking problem of continuous-time Markov chains with respect to continuous-time stochastic logic was introduced and shown to be decidable by Aziz et al. [1,2 in 1996. Unfortunately, their proof is only constructive, but highly unpractical. Later in 2000, an efficient approximate algorithm was proposed by Baier et al. [3,5 for a sublogic with binary until. In this paper, we apply transcendental number theory and classical linear algebra to bridge the gap between the precise but unpractical algorithm, and the imprecise but efficient approximate algorithm. We prove that the approximate algorithm in [3,5 can be used as an off-the-shell tool for a precise model checking algorithm for binary until formulas. Further, we discuss extensions of our results to nested until and continuous-time Markov decision processes.

Su, G, Feng, Y, Chen, T & Rosenblum, DS 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: Publisher's site

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 description

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: Publisher's site

#### View description

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, 'On hybrid models of quantum finite automata', *Journal of Computer and System Sciences*, vol. 81, no. 7, pp. 1144-1158.View/Download from: Publisher's site

#### View description

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

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: Publisher's site

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

#### View description

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

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

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

#### View description

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

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

#### View description

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

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: Publisher's site

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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: Publisher's site

#### View description

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.

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

#### View description

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

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

#### View description

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

Duan, R, Feng, Y & Ying, M 2007, 'Entanglement Is Not Necessary For Perfect Discrimination Between Unitary Operations', *Physical Review Letters*, vol. 98, no. 10, pp. 1-4.

#### View description

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

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

Duan, R, Feng, Y & Ying, M 2007, 'Entanglement is not necessary for perfect discrimination between unitary operations.', *Physical review letters*, vol. 98, no. 10, p. 100503.View/Download from: Publisher's site

#### View description

We show that a unitary operation (quantum circuit) secretly chosen from a finite set of unitary operations can be determined with certainty by sequentially applying only a finite amount of runs of the unknown circuit. No entanglement or joint quantum operations are required in our scheme. We further show that our scheme is optimal in the sense that the number of the runs is minimal when discriminating only two unitary operations.

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

#### View description

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

Duan, R, Feng, Y, Ji, Z & Ying, M 2007, 'Distinguishing arbitrary multipartite basis unambiguously using local operations and classical communication (vol 98, art no 230602, 2007)', *PHYSICAL REVIEW LETTERS*, vol. 99, no. 1.View/Download from: Publisher's site

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

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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 description

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

#### View description

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

Duan, R, Feng, Y, Ji, Z & Ying, M 2005, 'Efficiency Of Deterministic Entanglement Transformation', *Physical Review A*, vol. 71, no. 2, pp. 1-7.

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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 description

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

#### View description

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

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

#### View description

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

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

#### View description

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

Feng, Y, Zhang, S & Ying, M 2002, 'Probabilistic Cloning And Deleting Of Quantum States', *Physical Review A*, vol. 65, no. 4, pp. 1-4.

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

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

#### View description

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

Zhang, S, Feng, Y, Sun, X & Ying, M 2001, 'Upper bound for the success probability of unambiguous discrimination among quantum states', *Physical Review A. Atomic, Molecular, and Optical Physics*, vol. 64, no. 6.

#### View description

The general prediction of n quantum states was examined. An upper bound for success probability of unambiguous discrimination was established. The bound coincides with the known extended IDP limit when two states are concerned.

Feng, Y & Zhang, L 2014, 'When Equivalence and Bisimulation Join Forces in Probabilistic Automata' in *Lecture Notes in Computer Science*, Springer International Publishing, pp. 247-262.View/Download from: Publisher's site

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

#### View description

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

Fu, C, Turrini, A, Huang, X, Song, L, Feng, Y & Zhang, L 2018, 'Model checking probabilistic epistemic logic for probabilistic multiagent systems', *Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)*, IJCAI International Joint Conference on Artificial Intelligence, IJCAI, Stockholm, Sweden, pp. 4757-4763.View/Download from: Publisher's site

#### View description

© 2018 International Joint Conferences on Artificial Intelligence.All right reserved. In this work we study the model checking problem for probabilistic multiagent systems with respect to the probabilistic epistemic logic PETL, which can specify both temporal and epistemic properties. We show that under the realistic assumption of uniform schedulers, i.e., the choice of every agent depends only on its observation history, PETL model checking is undecidable. By restricting the class of schedulers to be memoryless schedulers, we show that the problem becomes decidable. More importantly, we design a novel algorithm which reduces the model checking problem into a mixed integer non-linear programming problem, which can then be solved by using an SMT solver. The algorithm has been implemented in an existing model checker and experiments are conducted on examples from the IPPC competitions.

Feng, Y & Deng, Y 2017, 'Bisimulations for probabilistic linear lambda calculi', *2017 International Symposium on Theoretical Aspects of Software Engineering (TASE)*, International Symposium on Theoretical Aspects of Software Engineering, IEEE, Sophia Antipolis, France.View/Download from: Publisher's site

#### View description

We investigate a notion of probabilistic program equivalence under linear contexts. We show that both a statebased and a distribution-based bisimilarity are sound coinductive proof techniques for reasoning about higher-order probabilistic programs, but only the distribution-based one is complete for linear contextual equivalence. The completeness proof is novel and directly constructs linear contexts from transitions, rather than the traditional approach of characterizing bisimilarities as testing equivalences.

Feng, Y, Hahn, EM, Turrini, A & Ying, S 2017, 'Model checking ω-regular properties for quantum Markov chains', *28th International Conference on Concurrency Theory (CONCUR 2017)*, International Conference on Concurrency Theory, Leibniz International Proceedings in Informatics, Berlin, Germany.View/Download from: Publisher's site

#### View description

© Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, and Shenggang Ying. Quantum Markov chains are an extension of classical Markov chains which are labelled with super-operators rather than probabilities. They allow to faithfully represent quantum programs and quantum protocols. In this paper, we investigate model checking !-regular properties, a very general class of properties (including, e.g., LTL properties) of interest, against this model. For classical Markov chains, such properties are usually checked by building the product of the model with a language automaton. Subsequent analysis is then performed on this product. When doing so, one takes into account its graph structure, and for instance performs different analyses per bottom strongly connected component (BSCC). Unfortunately, for quantum Markov chains such an approach does not work directly, because super-operators behave differently from probabilities. To overcome this problem, we transform the product quantum Markov chain into a single super-operator, which induces a decomposition of the state space (the tensor product of classical state space and the quantum one) into a family of BSCC subspaces. Interestingly, we show that this BSCC decomposition provides a solution to the issue of model checking ω-regular properties for quantum Markov chains.

Su, G, Chen, T, Feng, Y & Rosenblum, DS 2017, 'ProEva: Runtime proactive performance evaluation based on continuous-time markov chains', *Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering, ICSE 2017*, International Conference on Software Engineering, IEEE, Buenos Aires, Argentina, pp. 484-495.View/Download from: Publisher's site

#### View description

© 2017 IEEE. Software systems, especially service-based software systems, need to guarantee runtime performance. If their performance is degraded, some reconfiguration countermeasures should be taken. However, there is usually some latency before the countermeasures take effect. It is thus important not only to monitor the current system status passively but also to predict its future performance proactively. Continuous-Time Markov chains (CTMCs) are suitable models to analyze time-bounded performance metrics (e.g., how likely a performance degradation may occur within some future period). One challenge to harness CTMCs is the measurement of model parameters (i.e., transition rates) in CTMCs at runtime. As these parameters may be updated by the system or environment frequently, it is difficult for the model builder to provide precise parameter values. In this paper, we present a framework called ProEva, which extends the conventional technique of time-bounded CTMC model checking by admitting imprecise, interval-valued estimates for transition rates. The core method of ProEva computes asymptotic expressions and bounds for the imprecise model checking output. We also present an evaluation of accuracy and computational overhead for ProEva.

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)*, International Symposium on Temporal Representation and Reasoning, IEEE, Kongens Lyngby, Denmark, pp. 41-50.View/Download from: Publisher's site

#### View description

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

Su, G, Chen, T, Feng, Y, Rosenblum, DS & Thiagarajan, PS 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, Springer, Eindhoven, The Netherlands, pp. 269-286.View/Download from: Publisher's site

#### View description

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

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

#### View description

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

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, Springer, Madrid; Spain, pp. 427-440.View/Download from: Publisher's site

#### View description

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, Hahn, EM, 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: Publisher's site

#### View description

© 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, '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, International Foundation for Autonomous Agents and Multiagent Systems, Istanbul, pp. 209-217.

#### View description

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.

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 description

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.

Zhou, C & Feng, Y 2015, 'Extend transferable belief models with probabilistic priors', *Proceedings of UAI 2015*, Conference in Uncertainty in Artificial Intelligence, Association for Uncertainty in Artificial Intelligence (AUAI), Amsterdam, Netherlands, pp. 1-10.

#### View description

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.

Zhou, C & Feng, Y 2015, 'Extend Transferable Belief Models with Probabilistic Priors', *UNCERTAINTY IN ARTIFICIAL INTELLIGENCE*, 31st Conference on Uncertainty in Artificial Intelligence (UAI), AUAI PRESS, Amsterdam, NETHERLANDS, pp. 962-971.

Chen, T, Feng, Y, Rosenblum, DS & 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)*, International Conference on Concurrency Theory, Springer Verlag, Rome, Italy, pp. 218-233.View/Download from: Publisher's site

#### View description

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 & Zhang, L 2014, 'A nearly optimal upper bound for the self-stabilization time in Herman's algorithm', *Lecture Notes in Computer Science*, International Conference on Concurrency Theory, Springer, Italy, pp. 342-356.View/Download from: Publisher's site

#### View description

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.

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: Publisher's site

#### View description

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, Yu, N & Ying, M 2013, 'Reachability Analysis of Recursive Quantum Markov Chains', *Lecture Notes in Computer Science*, International Symposium on Mathematical Foundations of Computer Science, Springer, IST Austria, pp. 385-396.View/Download from: Publisher's site

#### View description

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

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

#### View description

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

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

#### View description

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

Feng, Y, Fan, W & Qin, Y 2013, 'A discrete event simulation based production line optimization through Markov decision process', *Proceedings of Communications in Computer and Information Science*, Asian Simulation Conference, Springer, Singapore, Singapore, pp. 385-390.View/Download from: Publisher's site

#### View description

In this paper, we built simulation model of the production line from one car engine parts plant in Beijing, in order to find proper solutions to raise productivity. The method of Discrete Event Simulation was used to construct the simulation model on account of the fact that production line was a typical discrete event system. Besides, worker heterogeneity, stochastic environment and the effect of worker learning and forgetting were introduced into simulation model to make it closer to reality. We proposed different schedule policies to manage the running of production line with the verification from simulation experiments. Then, by taking advantage of the simulation results obtained previous, we built the optimization model by applying Markov Decision Process (MDP) to seek for the best policy promoting the productivity of production line. © Springer-Verlag Berlin Heidelberg 2013.

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

#### View description

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

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

#### Projects

**Selected projects**