Can supervise: YES
© 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  and also a semantic model of quantum programs . 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.
© 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: UTS OPUS or Publisher's site
© 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: 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.
Feng, Y., Hart, J.N., Patterson, R.J. & Lowe, A. 2015, 'Electrospinning of TiO2 nanofibers: The influence of Li and Ca doping and vacuum calcination', Materials Letters, vol. 139, pp. 31-34.View/Download from: Publisher's site
© 2014 Elsevier B.V. All rights reserved. Pure, Li-doped and Ca-doped titanium dioxide nanofibers have been successfully produced by combining sol gel synthesis and electrospinning. The influence of lithium and calcium doping and calcination under vacuum on morphology, including grain size, nanofiber diameter and continuity, was observed by SEM. The phase composition was analyzed by X-ray diffraction. It was found that lithium doping increased the grain size, decreased the fiber diameter and resulted in a higher percentage of the rutile phase, while calcium doping had the opposite effects.
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.
Chen, W., Cao, Y., Wang, H. & Feng, Y. 2015, 'Minimum guesswork discrimination between quantum states', Quantum Information and Computation, vol. 15, no. 9-10, pp. 737-758.
© Rinton Press. 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.
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 & 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.
© 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: 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.
Feng, Y. & Fan, W. 2014, 'A system dynamics-based simulation model of production line with cross-trained workers', Journal of Statistical Computation and Simulation, vol. 84, no. 6, pp. 1190-1212.View/Download from: UTS OPUS or Publisher's site
In order to promote efficiency of the production line from one car engine parts plant, we built the simulation model based on System Dynamics. However, the standard System Dynamics method cannot precisely describe and simulate the situation when we introduced the management policy of cross-training, which was applied by the plant to promote efficiency, into production. Therefore, we revised and updated the simulation model to adapt to our requirement of simulating the policy of cross-training. Moreover, thinking that the workers will use more energy to get familiar with operation accompanied by the application of cross-training, it is necessary for us to consider the effect of worker learning and forgetting and the heterogeneity within worker pool into our model to make it more close to reality. At last, we conducted experiments to test how the production line would be optimized under different cross-training tactics, worker management policies and worker team structures. © 2013 Taylor & Francis.
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: UTS OPUS or Publisher's site
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) . In this paper we give a tighter upper bound 0.521N(2).
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
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., 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.
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
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
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
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.
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
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.
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.
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: 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.
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, 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, 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: 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
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: 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
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: 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
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
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
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
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
The problem of unambiguous discrimination between mixed quantum states is addressed by isolating the part of each mixed state which has no contribution to discrimination and by employing the strategy of set discrimination of pure states. A necessary and
Duan, R, 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
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
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
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
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
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
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, 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 & 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.
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
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
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: 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
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
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
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.
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.
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.
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: UTS OPUS or Publisher's site
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: UTS OPUS or Publisher's site
© 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: UTS OPUS or Publisher's site
© 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: 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.
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
© 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. & Fan, W. 2015, 'A hybrid simulation approach to dynamic multi-skilled workforce planning of production line', Proceedings - Winter Simulation Conference, pp. 1632-1643.View/Download from: Publisher's site
© 2014 IEEE. Workers cross-trained with multiple tasks can improve the workforce flexibility for the plant to handle variations in workload. Therefore, it is necessary to study the dynamic multi-skilled workforce planning problem of production line with the application of cross-training method. The conclusion is helpful to economize the cost of human resources when workload is low and enhance the productivity in the opposite case. This paper studies the dynamic multi-skilled workforce planning problem by exploring the effect of worker pool size and cross-training level on the performance of production line through simulation. A hybrid simulation model is built as the platform to study this problem with Discrete-event Simulation (DES) method and Agent-based Simulation (ABS) method. Besides, the effect of worker learning and forgetting is inevitably considered accompanied with the introduction of cross-training method and its impact on production line will be illustrated.
Feng, Y. & Ying, M. 2015, 'Toward Automatic Verification of Quantum Cryptographic Protocols.', CONCUR, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 441-455.View/Download from: UTS OPUS or Publisher's site
Zhou, C. & Feng, Y. 2015, 'Extend transferable belief models with probabilistic priors', Uncertainty in Artificial Intelligence - Proceedings of the 31st Conference, UAI 2015, pp. 962-971.
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.
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: 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 & 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: 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.
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: 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, '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/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.
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.
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/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.
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: 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 & 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: 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.
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, 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: UTS OPUS or Publisher's site
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, 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: 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, International Conference on Concurrency Theory, 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, ACM-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.