UTS site search


Mingsheng YingProf Mingsheng Ying

Yuan Feng
Yuan Feng

Floyd-Hoare Logic for Quantum Programs

Floyd-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”.
Mingsheng YingProfessor Mingsheng Ying

Yuan FengA/Prof
Yuan Feng

Runyao Duan Prof
Runyao Duan

Bisimulation for Quantum Processes

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

Runyao Duan Prof
Runyao Duan

Sanjiang Li
Sanjiang Li

Igniting the Study of Quantum Zero-error Communication

Since 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.
Sanjiang LiA/Prof
Sanjiang Li

Qualitative Spatial Reasoning

Direction 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 Prof
Dacheng Tao

Ensemble Manifold Regularisation

How 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:
  1. learns both the composite manifold and the semi-supervised learner jointly;
  2. is fully automatic for learning the intrinsic manifold hyper-parameters implicitly;
  3. is conditionally optimal for intrinsic manifold approximation under a mild and reasonable assumption; and
  4. is scalable for a large number of candidate manifold hyper-parameters, from the perspectives of both time and space.
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 ZhuProf
Xingquan Zhu

Real-time Learning and Classification for Big Data Streams

Many 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:
  1. streaming feature selections from feature streams;
  2. active sampling and instance selection for data streams;
  3. real-time classification for data streams; and
  4. structured pattern search and classification for graph streams.
The above research outcomes have been published extensively in premier journals and conference proceedings in related fields, including IEEE Transactions on Pattern Analysis and Machine Intelligence, IEEE Transactions on Knowledge and Data Engineering, ACM International Conference on Knowledge Discovery and Data Mining (SIG KDD), amongst others.