Achievements
Prof Mingsheng Ying A/Prof Yuan Feng | Floyd-Hoare Logic for Quantum ProgramsFloyd-Hoare logic is a logic system for reasoning rigorously about the correctness of computer programs. It was proposed by Tony Hoare in 1969 and seeded the work on the inductive assertion method of Robert Floyd in 1967. Its (relative) completeness was proved by Stephen Cook in 1978. Floyd-Hoare logic is the core of the subject of program verification, and at the centre of subjects on programming methodology and semantics of programming languages. It has been widely used in the software industry. To build a logical foundation for programming methodology for quantum computers, quite a few research groups tried to develop Floyd–Hoare logic for quantum programs, but did not fully succeed. Prof Mingsheng Ying established a full-fledged quantum Floyd-Hoare logic, and in particular proved its (relative) completeness (in ACM Transactions on Programming Languages and Systems, vol. 33, 2011, Article 19, 49 pages). One of the reviewers described this work as, “One of the landmarks in the development of the theory of quantum programming languages”. | |
Professor Mingsheng Ying
A/Prof Yuan Feng
Prof Runyao Duan | Bisimulation for Quantum ProcessesOne of the most serious issues in quantum process algebra is to discover a quantum generalisation of bisimulation, which lies in a central position in process algebra. Quite a few versions of bisimulation have been defined for quantum processes in the literature, but in the best research they are only proved to be preserved by parallel composition of purely quantum processes where no classical communication is involved. A notion of bisimulation preserved by parallel composition in the circumstance of both classical and quantum communication is crucial. However, because quantum states are not locally determined (entanglement) and quantum operations are normally non-commutative, this problem was very difficult, and remained open for quite a long time. A/Prof Yuan Feng, Prof Runyao Duan and Prof Mingsheng Ying completely solved this problem in the paper “Bisimulation for quantum processes”, published at ACM TOPLAS in 2012, the most prestigious international journal in programming language theory (a primary version of this paper was published in POPL2011). They also demonstrated the uniqueness of the solutions for recursive equations of quantum processes, which proves very useful in verifying complex quantum protocols. This breakthrough scientific work has led towards a comprehensive framework for modelling and reasoning about concurrent quantum systems, including distributed quantum computing systems and quantum communication protocols. | |
Prof Runyao Duan A/Prof Sanjiang Li | Igniting the Study of Quantum Zero-error CommunicationSince the seminal work of Prof C E Shannon in 1956, the study of zero-error communication and related topics has grown into a vast field called Zero-error Information Theory. Recently, there has been considerable interest in developing a quantum zero-error information theory by considering quantum effects in zero-error communication. In Physical Review Letters, vol. .101, 020501, 2008, Prof Runyao Duan and A/Prof Yaoyun Shi demonstrated that there are quantum channels for which a single use cannot transmit classical information perfectly, yet two uses can. This is the first non-trivial result in quantum zero-error information theory that fully demonstrates the quantum effect. Furthermore, in IEEE Transactions on Information Theory, vol. 59, 1164-1174, 2013, Prof Runyao Duan, Dr Simone Severini, and Prof Andreas Winter introduced a quantum generalisation of the celebrated Lovász theta function for quantum channels and found that this generalisation provides an upper bound for entanglement-assisted zero-error classical capacity. This research work has significantly advanced quantum zero-error information theory, and has triggered broad research interest. For instance, this research has lead to the notion of non-commutative graphs to characterise the zero-error communication behaviours of quantum channels. | |
A/Prof Sanjiang Li | Qualitative Spatial ReasoningDirection relations between extended spatial objects are important common-sense knowledge. Recently, Goyal and Egenhofer proposed a relation model, known as the cardinal direction calculus (CDC), to represent 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 the decision of whether a network is realisable by connected regions in the real plane. A/Prof Sanjiang Li and his colleagues provided a cubic algorithm that checks the consistency of complete networks of basic CDC constraints, and proved that reasoning with the CDC is, in general, an NP-complete problem. For a consistent complete network of basic CDC constraints, their 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. This result has been published by Artificial Intelligence in 2010: 174 (12–13) 951–983. | |
Prof Dacheng Tao | Ensemble Manifold RegularisationHow do we build a robust learner with a few labelled samples while vast amounts of unlabelled samples are readily available? Manifold regularisation based semi-supervised learning and its variants effectively address this problem for classification and regression of various resources, eg, images, videos, and documents. However, the incorporated regularisation creates multiple hyper-parameters for intrinsic manifold approximation, and this makes the algorithm difficult to manipulate and inefficient for learning, in practice. Prof Dacheng Tao, along with his colleagues, developed an automatic approximation of the intrinsic manifold for general semi-supervised learning problems. Unfortunately, it is not trivial to define an optimisation function to obtain optimal hyper-parameters. Usually, pure cross-validation is considered, but it does not necessarily scale up. A second problem derives from the sub-optimality incurred by discrete grid search and over-fitting problems. Therefore, Prof Tao developed an ensemble manifold regularisation (EMR) frame-work to approximate the intrinsic manifold by combining several initial guesses. Algorithmically, he carefully designed EMR so it:
Furthermore, Prof Tao proved the convergence property of EMR to the deterministic matrix at rate root-n. Extensive experiments over both synthetic and real datasets demonstrate the effectiveness of the proposed framework. The results have been published by IEEE Transactions on Pattern Analysis and Machine Intelligence, vol. 34 (6): 1227–1233, 2012. | |
Prof Xingquan Zhu | Real-time Learning and Classification for Big Data StreamsMany organisations, such as financial firms, are today actively trying to extract meaning from an explosion of structured and unstructured data: social media streams, smartphone data, videos. The fundamental challenge of big data is the enormous volume, dynamic change, and need for real-time response. When handling big data, our existing Knowledge Discovery and Data mining (KDD) frameworks severely lack scalability and real-time capacity, mainly because big data are treated as a static gigantic set, whereas data from applications such as social networks and surveillance videos are typically updated every single minute.Prof Xingquan Zhu and his colleagues’ research intends to deliver real-time learning and classification systems for big data streams. The key challenge is to harness the big data volumes in order to enable real-time learning and pattern mining. To date, Prof Zhu’s research has resulted in several important contributions, including:
|
-
Our Labs
Data Science (DSKD)
Decision Systems (DeSI)
Innovation (The Magic Lab)
Knowledge Infrastructure (KIL)
Quantum Computation (QCL)
Our Research
News
Events
Projects
Publications
Achievements
About QCIS
History
International Advisory Board
Joint Research Centres
Working With Us
Studying With Us
Reports & Statistics
--
Our People
Gallery -
Level 10
UTS Building 11
15 Broadway
Ultimo NSW 2007
Director:
Chengqi Zhang
Phone: +61 2 9514 7941
Email: Chengqi.Zhang@uts.edu.au