Professor Mingsheng Ying

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

A rigorous paradigm coordinating components is important in the design stage of large-scale software engineering. In this paper we propose a new Architecture Description Language, called ACDL, to represent the centralized-mode architectural connection in which all components are linked by a single connector. Following one usual approach to architectural description, in which component types and components are distinguished, and connectors integrate behaviors of components by specifying their coordination protocols, ACDL describes connectors in such a way that connectors are insensitive to the numbers of attached same-type components. Based on ACDL, we develop analytic techniques to facilitate the system checking of temporal properties of an architecture. In particular, our method shows to what extent one can add, delete and replace components without making the whole system lose desired temporal properties, and improves the system checking in several ways, for example enhancing the use of previous checking results to deal with new checking problems.

Ying, M., Duan, R., Feng, Y. & Ji, Z. 2010, 'Predicate Transformer Semantics of Quantum Programs' in Simon Gay, Ian Mackie (eds), Semantic Techniques in Quantum Computation, Cambridge University Press, Cambridge, pp. 311-360.
View/Download from: UTSePress
View description>>

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

Ying, M. 2007, 'Quantum logic and automata theory' in Kurt Engesser, Dov M. Gabbay, Daniel Lehmann (eds), Handbook of Quantum Logic and Quantum Structures, Elsevier, London, UK, pp. 619-754.
View/Download from: UTSePress | Publisher's site
View description>>

An axiomatization of a mathematical theory consists of a system of basic notions as well as a set of axioms about these notions. The mathematical theory is then the set of theorems which can be derived from the axioms. Obviously, one needs a certain logic providing the tools of reasoning in the derivation of these theorems from the axioms. As pointed out by A. Heyting [1963, p. 5], in the early stages of the axiomatic viewpoint, logic was used in an unanalyzed form. In a later stage, in the study of the foundations of mathematics beginning early in the twentieth century, it was realized that a major part of mathematics has to exploit the full power of classical (Boolean) logic [Hatcher, 1982], the strongest in the family of existing logics. For example, group theory is based on first-order logic, and point-set topology is built on a fragment of second-order logic. However, some mathematicians, including the big names of L. E. J. Brouwer, H. Poincare, L. Kronecker and H. Weyl, have taken a constructive position which is in more or less explicit opposition to certain forms of mathematical reasoning used by the majority of the mathematical community. Some of them even endeavoured to establish so-called constructive mathematics, i.e. the part of mathematics that can be rebuilt on constructivist principles. The logic employed in the development of constructive mathematics is intuitionistic logic [Troelstra and van Dalen, 1988], which is genuinely weaker than classical logic.

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

Yu, N., Duan, R. & Ying, M. 2012, 'Four Locally Indistinguishable Ququad-Ququad Orthogonal Maximally Entangled States', Physical Review Letters, vol. 109, no. 2, pp. 020506-1-020506-5.
View/Download from: Publisher's site
View description>>

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

Yu, N. & Ying, M. 2012, 'Reachability and Termination Analysis of Concurrent Quantum Programs', Lecture Notes in Computer Science, vol. 7454, pp. 69-83.
View/Download from: Publisher's site
View description>>

We introduce a Markov chain model of concurrent quantum programs. This model is a quantum generalization of Hart, Sharir and Pnueli+s probabilistic concurrent programs. Some characterizations of the reachable space, uniformly repeatedly reachable space and termination of a concurrent quantum program are derived by the analysis of their mathematical structures. Based on these characterizations, algorithms for computing the reachable space and uniformly repeatedly reachable space and for deciding the termination are given.

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

In this paper, we define a probabilistic version of filtration and use it to provide a finite approximation of Markov processes. In order to measure the approximation, we employ probability logic to construct the final Markov process and define a metric on the set of Markov processes through this logic. Moreover, we show that the set endowed with this metric is a Polish space. Finally we point to some questions connecting approximation to uniformity and approximate bisimilarity as topics for future research.

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

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

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: UTSePress | 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

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

A subspace of a multipartite Hilbert space is said to be locally indistinguishable if any orthonormal basis of this subspace cannot be perfectly distinguished by local operations and classical communication. Previously it was shown that any m . n bipartite system with m > 2 and n > 2 has a locally indistinguishable subspace. However, it has been an open problem since 2005 whether there is a locally indistinguishable bipartite subspace with a qubit subsystem.We settle this problem in negative by showing that any 2 . n bipartite subspace contains a basis that is locally distinguishable. As an interesting application, we show that any quantum channel with two Kraus operators has optimal environment-assisted classical capacity.

Chen, J. & Ying, M. 2010, 'Ancilla-assisted discrimination of quantum gates', Quantum Information and Computation, vol. 10, no. 1, pp. 160-177.
View/Download from: UTSePress
View description>>

The intrinsic idea of superdense coding is to find as many gates as possible such that they can be perfectly discriminated. In this paper, we consider a new scheme of discrimination of quantum gates, called ancilla-assisted discrimination, in which a set of quantum gates on a $d-$dimensional system are perfectly discriminated with assistance from an $r-$dimensional ancilla system. The main contribution of the present paper is two-fold: (1) The number of quantum gates that can be discriminated in this scheme is evaluated. We prove that any $rd+1$ quantum gates cannot be perfectly discriminated with assistance from the ancilla, and there exist $rd$ quantum gates which can be perfectly discriminated with assistance from the ancilla. (2) The dimensionality of the minimal ancilla system is estimated. We prove that there exists a constant positive number $c$ such that for any $k\leq cr$ quantum gates, if they are $d$-assisted discriminable, then they are also $r$-assisted discriminable, and there are $c^{\prime}r\textrm{}(c^{\prime}>c)$ different quantum gates which can be discriminated with a $d-$dimensional ancilla, but they cannot be discriminated if the ancilla is reduced to an $r-$dimensional system. Thus, the order $O(r)$ of the number of quantum gates that can be discriminated with assistance from an $r-$dimensional ancilla is optimal. The results reported in this paper represent a preliminary step toward understanding the role ancilla system plays in discrimination of quantum gates as well as the power and limit of superdense coding.

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

We study the local distinguishability of general multiqubit states and show that local projective measurements and classical communication are as powerful as the most general local measurements and classical communication. Remarkably, this indicates that

Ji, Z., Chen, J., Wei, Z. & Ying, M. 2010, 'The LU-LC conjecture is false', Quantum Information and Computation, vol. 10, no. 1, pp. 97-108.
View/Download from: UTSePress
View description>>

The LU-LC conjecture is an important open problem concerning the structure of entanglement of states described in the stabilizer formalism. It states that two local unitary equivalent stabilizer states are also local Clifford equivalent. If this conjecture were true, the local equivalence of stabilizer states would be extremely easy to characterize. Unfortunately, however, based on the recent progress made by Gross and Van den Nest, we find that the conjecture is false.

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

A bipartite state, which is secretly chosen from a finite set of known entangled pure states, cannot immediately be useful in standard quantum information processing tasks. To effectively make use of the entanglement contained in this unknown state, we i

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

Direction relations between extended spatial objects are important commonsense knowledge. Recently, Goyal and Egenhofer proposed a relation model, known as the cardinal direction calculus (CDC), for representing direction relations between connected plane regions. The CDC is perhaps the most expressive qualitative calculus for directional information, and has attracted increasing interest from areas such as artificial intelligence, geographical information science, and image retrieval. Given a network of CDC constraints, the consistency problem is deciding if the network is realizable by connected regions in the real plane. This paper provides a cubic algorithm for checking the consistency of complete networks of basic CDC constraints, and proves that reasoning with the CDC is in general an NP-complete problem. For a consistent complete network of basic CDC constraints, our algorithm returns a Ô++canonicalÔ++ solution in cubic time. This cubic algorithm is also adapted to check the consistency of complete networks of basic cardinal constraints between possibly disconnected regions.

Ying, M. & Feng, Y. 2010, 'Quantum loop programs', Acta Informatica, vol. 47, no. 4, pp. 221-250.
View/Download from: UTSePress | 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.

Ying, M. 2010, 'Quantum Computation, Quantum Theory And AI', Artificial Intelligence Journal, vol. 174, no. 2, pp. 162-176.
View/Download from: UTSePress | Publisher's site
View description>>

The main purpose of this paper is to examine some (potential) applications of quantum computation in AI and to review the interplay between quantum theory and AI. For the readers who are not familiar with quantum computation, a brief introduction to it i

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

A2 circle times 2 unitary operation is called a perfect entangler if it can generate a maximally entangled state from some unentangled input. We study the following question: How many runs of a given two-qubit entangling unitary operation are required to

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: UTSePress | 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.

Duan, R., Feng, Y. & Ying, M. 2009, 'Perfect Distinguishability of Quantum Operations', Physical Review Letters, vol. 103, no. 21, pp. 210501-1-210501-4.
View/Download from: UTSePress | Publisher's site
View description>>

We provide a feasible necessary and sufficient condition for when an unknown quantum operation (quantum device) secretly selected from a set of known quantum operations can be identified perfectly within a finite number of queries, and thus complete the characterization of the perfect distinguishability of quantum operations. We further design an optimal protocol which can achieve the perfect discrimination between two quantum operations by a minimal number of queries. Interestingly, we find that an optimal perfect discrimination between two isometries is always achievable without auxiliary systems or entanglement.

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: UTSePress
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., 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: UTSePress | 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.

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: UTSePress | 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.

Chen, J.F., Duan, R., Ji, Z., Ying, M. & Yu, J.X. 2008, 'Existence Of Universal Entangler', Journal of Mathematical Physics, vol. 49, no. 1, pp. 1-7.
View/Download from: UTSePress | Publisher's site
View description>>

A gate is called an entangler if it transforms some (pure) product states to entangled states. A universal entangler is a gate which transforms all product states to entangled states. In practice, a universal entangler is a very powerful device for gener

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: UTSePress | 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: UTSePress | 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.

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

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

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

We consider the possibility of using stabilizer states to perform deterministic dense coding among multiple senders and a single receiver. In the model we studied, the utilized stabilizer state is partitioned into several subsystems and then each subsyst

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

We study the possibility of performing perfect teleportation of unknown quantum states from multiple senders to a single receiver with a previously shared stabilizer state. In the model we considered, the utilized stabilizer state is partitioned into sev

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

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

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

To effectively represent possibility arising from states and dynamics of a system, fuzzy discrete-event systems (DESs) as a generalization of conventional DESs have been introduced recently. Supervisory-control theory based on event feedback has been well established for such systems. Noting that the system state description, from the viewpoint of specification, seems more convenient, we investigate the state-based control of fuzzy DESs in this paper. An approach to finding all fuzzy states that are reachable by controlling the system is presented first. After introducing the notion of controllability for fuzzy states, a necessary and sufficient condition for a set of fuzzy states to be controllable is then provided. It was also found that event- and state-based controls are not equivalent, and the relationship between them was further discussed. Finally, we examine the possibility of driving a fuzzy DES under control from a given initial state to a prescribed set of fuzzy states and then keeping it there indefinitely

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: UTSePress | Publisher's site
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. & Ying, M. 2007, 'Entanglement Is Not Necessary For Perfect Discrimination Between Unitary Operations', Physical Review Letters, vol. 98, no. 10, pp. 1-4.
View/Download from: UTSePress | 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 ope

Feng, Y., Duan, R., Ji, Z. & Ying, M. 2007, 'Probabilistic Bisimulations For Quantum Processes', Information And Computation, vol. 205, no. 11, pp. 1608-1639.
View/Download from: UTSePress | 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: UTSePress | 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

Wang, G. & Ying, M. 2007, 'Multipartite Unlockable Bound Entanglement In The Stabilizer Formalism', Physical Review A, vol. 75, no. 5, pp. 1-8.
View/Download from: UTSePress | Publisher's site
View description>>

We find an interesting relationship between multipartite bound entangled states and the stabilizer formalism. We prove that, if a set of commuting operators from the generalized Pauli group on n qudits satisfy certain constraints, then the maximally mixe

Wei, Z. & Ying, M. 2007, 'Quantum Adiabatic Computation And Adiabatic Conditions', Physical Review A, vol. 76, no. 2, pp. 1-4.
View/Download from: UTSePress | Publisher's site
View description>>

Recently, quantum adiabatic computation has attracted more and more attention in the literature. It is a novel quantum computation model based on adiabatic approximation, and the analysis of a quantum adiabatic algorithm depends highly on the adiabatic c

Ying, M., Chen, J.F., Feng, Y. & Duan, R. 2007, 'Commutativity Of Quantum Weakest Preconditions', Information Processing Letters, vol. 104, no. 4, pp. 152-158.
View/Download from: UTSePress | 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

Ying, M. 2007, 'Topology, randomness and noise in process calculus', Frontiers of Electrical and Electronic Engineering in China, vol. 2, no. 2, pp. 127-131.
View/Download from: UTSePress | Publisher's site
View description>>

Formal models of communicating and concurrent systems are one of the most important topics in formal methods, and process calculus is one of the most successful formal models of communicating and concurrent systems. In the previous works, the author systematically studied topology in process calculus, probabilistic process calculus and pi-calculus with noisy channels in order to describe approximate behaviors of communicating and concurrent systems as well as randomness and noise in them. This article is a brief survey of these works.

Zhang, C., Wang, G. & Ying, M. 2007, 'Discrimination Between Pure States And Mixed States', Physical Review A, vol. 75, no. 6, pp. 1-6.
View/Download from: UTSePress | Publisher's site
View description>>

In this paper, we discuss the problem of determining whether a quantum system is in a pure state, or in a mixed state. We apply two strategies to settle this problem: the unambiguous discrimination and the maximum confidence discrimination. We prove that

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

Fuzzy discrete-event systems as a generalization of (crisp) discrete-event systems have been introduced in order that it is possible to effectively represent uncertainty, imprecision, and vagueness arising from the dynamic of systems. A fuzzy discrete-ev

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

Due to the appearance of uncontrollable events in discrete-event systems, one may wish to replace the behavior leading to the uncontrollability of pre-specified language by some quite similar one. To capture this similarity, we introduce metric to tradit

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

Wang, G. & Ying, M. 2006, 'Unambiguous Discrimination Among Quantum Operations', Physical Review A, vol. 73, no. 4, pp. 1-5.
View/Download from: UTSePress | Publisher's site
View description>>

We address the problem of unambiguous discrimination among a given set of quantum operations. The necessary and sufficient condition for them to be unambiguously distinguishable is derived in the cases of single use and multiple uses, respectively. For t

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

Deutsch-Jozsa algorithm has been implemented via a quantum adiabatic evolution by S. Das et al. [S. Das, R. Kobes, G. Kunstatter, Phys. Rev. A 65 (2002) 062310]. This adiabatic algorithm gives rise to a quadratic speed up over classical algorithms. We sh

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

Recently, some quantum algorithms have been implemented by quantum adiabatic evolutions. In this Letter, we discuss the accurate relation between the running time and the distance of the initial state and the final state of a kind of quantum adiabatic ev

Wei, Z. & Ying, M. 2006, 'Majorization In Quantum Adiabatic Algorithms', Physical Review A, vol. 74, no. 4, pp. 1-7.
View/Download from: UTSePress | Publisher's site
View description>>

The majorization theory has been applied to analyze the mathematical structure of quantum algorithms. An empirical conclusion by numerical simulations obtained in the previous literature indicates that step-by-step majorization seems to appear universall

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

Since quantifiers have the ability of summarizing the properties of a class of objects without enumerating them, linguistic quantification is a very important topic in the field of high level knowledge representation and reasoning. This paper introduces

Zhang, C., Feng, Y. & Ying, M. 2006, 'Unambiguous Discrimination Of Mixed Quantum States', Physics Letters A, vol. 353, no. 4, pp. 300-306.
View/Download from: UTSePress | 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

Zhang, C., Ying, M. & Qiao, B. 2006, 'Universal Programmable Devices For Unambiguous Discrimination', Physical Review A, vol. 74, no. 4, pp. 1-9.
View/Download from: UTSePress | Publisher's site
View description>>

We discuss the problem of designing unambiguous programmable discriminators for any n unknown quantum states in an m-dimensional Hilbert space. The discriminator is a fixed measurement that has two kinds of input registers: the program registers and the

Cao, Y. & Ying, M. 2005, 'Supervisory Control Of Fuzzy Discrete Event Systems', IEEE Transactions on Systems, Man, and Cybernetic..., vol. 35, no. 2, pp. 366-371.
View/Download from: UTSePress | Publisher's site
View description>>

To cope with situations in which a plant's dynamics are not precisely known, we consider the problem of supervisory control for a class of discrete event systems modeled by fuzzy automata. The behavior of such discrete event systems is described by fuzzy

Duan, R., Feng, Y., Ji, Z. & Ying, M. 2005, 'Efficiency Of Deterministic Entanglement Transformation', Physical Review A, vol. 71, no. 2, pp. 1-7.
View/Download from: UTSePress | Publisher's site
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. & 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: UTSePress | Publisher's site
View description>>

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

Duan, R., Feng, Y., Li, X. & Ying, M. 2005, 'Multiple-Copy Entanglement Transformation And Entanglement Catalysis', Physical Review A, vol. 71, no. 4, pp. 1-11.
View/Download from: UTSePress | Publisher's site
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/Download from: UTSePress | Publisher's site
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: UTSePress | 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/Download from: UTSePress | Publisher's site
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

Ji, Z., Cao, H. & Ying, M. 2005, 'Optimal Conclusive Discrimination Of Two States Can Be Achieved Locally', Physical Review A, vol. 71, no. 3, pp. 1-5.
View/Download from: UTSePress | Publisher's site
View description>>

This paper constructs a local operation and classical communication protocol that achieves the global optimality of conclusive discrimination of any two pure states with arbitrary a priori probability. This can be interpreted that there is no

Li, S., Ying, M. & Li, Y. 2005, 'On Countable RCC Models', Fundamenta Informaticae, vol. 65, no. 4, pp. 329-351.
View/Download from: UTSePress
View description>>

Region Connection Calculus (RCC) is the most widely studied formalism of Qualitative Spatial Reasoning. It has been known for some time that each connected regular topological space provides an RCC model. These 'standard' models are inevitable uncountabl

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

Without additional resources, it is often impossible to transform one entangled quantum state into another with local quantum operations and classical communication. Jonathan and Plenio (Phys. Rev. Lett., vol. 83, p. 3566, 1999) presented an interesting

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

The (meta)logic underlying classical theory of computation is Boolean (two-valued) logic. Quantum logic was proposed by Birkhoff and von Neumann as a logic of quantum mechanics more than 60 years ago. It is currently understood as a logic whose truth val

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

Diagnostic systems depend on knowledge bases specifying the causal, structural or functional interactions among components of the diagnosed objects. A diagnostic specification in a diagnostic system is a semantic interpretation of a knowledge base. We in

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

It is assumed in the pi-calculus that communication channels are always noiseless. But it is usually not the case in the mobile systems that developers are faced with in the real life. In this paper, we introduce an extension of pi, called pi(N), in whic

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

It is shown that two copies are enough to distinguish a complete basis of maximally entangled states in canonical form by constructing an explicit protocol. In particular, in such a protocol, no auxiliary system is needed and the symmetrical roles of cer

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: UTSePress | 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: UTSePress
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, 'Unambiguous discrimination between mixed quantum states', Physical Review A, vol. 70, no. 1, pp. 012308-1-012308-4.
View/Download from: UTSePress | Publisher's site
View description>>

We prove that the states secretly chosen from a mixed state set can be perfectly discriminated if and only if they are orthogonal. The sufficient and necessary condition under which nonorthogonal mixed quantum states can be unambiguously discriminated is also presented. Furthermore, we derive a series of lower bounds on the inconclusive probability of unambiguous discrimination of states from a mixed state set with a priori probabilities.

Feng, Y., Duan, R. & Ying, M. 2004, 'When Catalysis Is Useful For Probabilistic Entanglement Transformation', Physical Review A, vol. 69, no. 6, pp. 1-5.
View/Download from: UTSePress | Publisher's site
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

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

We prove, in a multipartite setting, that it is always feasible to exactly transform a genuinely m-partite entangled pure state with sufficient many copies to any other m-partite state via local quantum operation and classical communication. This result

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

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

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

We define q quantum finite automata (qQFAs) and q quantum regular grammars (qQRGs), and verify that they are exactly equivalent to those measure-once quantum finite automata (MO-QFAs) in the literature. In particular, we define q quantum pushdown automat

Su, G., Ying, M. & Zhang, C. 2012, 'Semantic Analysis of Component-aspect Dynamism for Connector-based Architecture Styles', Helsinki (Finland), August 2012 in 2012 Joint Working Conference on Software Architecture & 6th European Conference on Software Architecture, ed Tomi MannistoÂ, M. Ali Babar, Carlos E. Cuesta, and Juha Savolainen, IEEE Computer Society, US, pp. 151-160.
View description>>

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

Feng, Y., Duan, R. & Ying, M. 2011, 'Bisimulation for Quantum Processes', annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Austin, Texas, USA, January 2011 in Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming language, ed Sagiv, M, ACM, New York, NY, USA, pp. 523-534.
View/Download from: UTSePress | Publisher's site
View description>>

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

Ying, M. 2010, 'Foundations of quantum programming', Programming Languages and Systems, Shanghai, China, November 2010 in Programming Languages and Systems 8th Asian Symposium, APLAS 2010, ed Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen, Springer-Verlag, Berlin, pp. 16-20.
View/Download from: UTSePress | Publisher's site
View description>>

Progress in the techniques of quantum devices has made people widely believe that large-scale and functional quantum computers will be eventually built. By then, super-powered quantum computer will solve many problems affecting economic and social life t

Zhang, H. & Ying, M. 2010, 'Decidable fragments of first-order language under stable model semantics and circumscription', Conference on Artificial Intelligence, Atlanta, Georgia, July 2010 in 24th AAAI Conference on Artificial Intelligence 2010, ed NA, The AAAI Press, Menlo Park, California, pp. 375-380.
View/Download from: UTSePress
View description>>

The stable model semantics was recently generalized by Ferraris, Lee and Lifschitz to the full first-order language with a syntax translation approach that is very similar to McCarthy's circumscription. In this paper, we investigate the decidability and

Zhang, X., Liu, W., Li, S. & Ying, M. 2008, 'Reasoning with Cardinal Directions: An Efficient Algorithm', National Conference of the American Association for Artificial Intelligence, Chicago, Illinois, USA, July 2008 in Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence vol 1, ed Dieter Fox and Carla P. Gomes, AAAI Press, USA, pp. 387-392.
View/Download from: UTSePress
View description>>

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

Ying, M. 2005, 'A theory of computation based on quantum logic', IEEE International Conference on Granular Computing, Beijing, China, July 2009 in 2005 IEEE International Conference On Granular Computing, ed Hu, XH, Liu, Q, Skowron, A, Lin, TY, Yager, RR, Zhang, B, IEEE, New York, pp. 91-91.
View/Download from: UTSePress | Publisher's site
View description>>

Summary form only given. The (meta) logic underlying classical theory of computation is Boolean (two-valued) logic. Quantum logic was proposed by Birkhoff and von Neumann as a logic of quantum mechanics. It is currently understood as a logic whose truth values are taken from an orthomodular lattice. The major difference between Boolean logic and quantum logic is that the latter does not enjoy distributivity in general. The rapid development of quantum computation in recent years stimulates us to establish a theory of computation based on quantum logic. The present paper is the first step toward such a new theory and it focuses on the simplest models of computation, namely finite automata. We introduce the notion of orthomodular lattice-valued (quantum) automaton. The Kleene theorem about equivalence of regular expressions and finite automata is generalized into quantum logic. We also present a pumping lemma for orthomodular lattice-valued regular languages.