Adak, C, Chaudhuri, BB & Blumenstein, M 2019, 'An Empirical Study on Writer Identification and Verification From Intra-Variable Individual Handwriting', IEEE ACCESS, vol. 7, pp. 24738-24758.
View/Download from: UTS OPUS or Publisher's site
Alaei, F, Alaei, A, Pal, U & Blumenstein, M 2019, 'A comparative study of different texture features for document image retrieval', Expert Systems with Applications, vol. 121, pp. 97-114.
View/Download from: UTS OPUS or Publisher's site
View description>>
© 2018 Elsevier Ltd Due to the rapid increase of different digitised documents, there has been significant attention dedicated to document image retrieval over the past two decades. Finding discriminative and effective features is a fundamental task for providing a fast and more accurate retrieval system. Texture features are generally fast to compute and are suitable for large volume data. Thus, in this study, the effectiveness of texture features widely used in the literature of content-based image retrieval is investigated on document images. Twenty-six different texture feature extraction methods from four main categories of texture features, statistical, transform, model, and structural-based approaches, are considered in this research work to compare their performance on the problem of document image retrieval. Three document image datasets, MTDB, ITESOFT, and CLEF_IP with various content and page layouts are used to evaluate the twenty-six texture-based features on document image retrieval systems. The retrieval results are computed in terms of precision, recall and F-score, and a comparative analysis of the results is also provided. Feature dimensions and time complexity of the texture-based feature methods are further compared. Finally, some conclusions are drawn and suggestions are made about future research directions.
Chubb, CT, Tomamichel, M & Korzekwa, K 2019, 'Moderate deviation analysis of majorization-based resource interconversion', PHYSICAL REVIEW A, vol. 99, no. 3.
View/Download from: Publisher's site
Guo, GC & Ying, M 2019, 'Preface to special topic on quantum computing', National Science Review, vol. 6, no. 1, p. 20.
View/Download from: Publisher's site
Halasi, Z, Maróti, A, Pyber, L & Qiao, Y 2019, 'An improved diameter bound for finite simple groups of Lie type', Bulletin of the London Mathematical Society.
View/Download from: Publisher's site
View description>>
© 2019 London Mathematical Society For a finite group (Formula presented.), let (Formula presented.) denote the maximum diameter of a connected Cayley graph of (Formula presented.). A well-known conjecture of Babai states that (Formula presented.) is bounded by (Formula presented.) in case (Formula presented.) is a non-abelian finite simple group. Let (Formula presented.) be a finite simple group of Lie type of Lie rank (Formula presented.) over the field (Formula presented.). Babai's conjecture has been verified in case (Formula presented.) is bounded, but it is wide open in case (Formula presented.) is unbounded. Recently, Biswas and Yang proved that (Formula presented.) is bounded by (Formula presented.). We show that in fact (Formula presented.) holds. Note that our bound is significantly smaller than the order of (Formula presented.) for (Formula presented.) large, even if (Formula presented.) is large. As an application, we show that more generally (Formula presented.) holds for any subgroup (Formula presented.) of (Formula presented.), where (Formula presented.) is a vector space of dimension (Formula presented.) defined over the field (Formula presented.).
Harper, R, Hincks, I, Ferrie, C, Flammia, ST & Wallman, JJ 2019, 'Statistical analysis of randomized benchmarking', Physical Review A, vol. 99, no. 5.
View/Download from: Publisher's site
View description>>
© 2019 American Physical Society. Randomized benchmarking and variants thereof, which we collectively call RB+, are widely used to characterize the performance of quantum computers because they are simple, scalable, and robust to state-preparation and measurement errors. However, experimental implementations of RB+ allocate resources suboptimally and make ad-hoc assumptions that undermine the reliability of the data analysis. In this paper, we propose a simple modification of RB+ which rigorously eliminates a nuisance parameter and simplifies the experimental design. We then show that, with this modification and specific experimental choices, RB+ efficiently provides estimates of error rates with multiplicative precision. Finally, we provide a simplified rigorous method for obtaining credible regions for parameters of interest and a heuristic approximation for these intervals that performs well in currently relevant regimes.
Ivanyos, G & Qiao, Y 2019, 'Algorithms based on *-algebras, and their applications to isomorphism of polynomials with one secret, group isomorphism, and polynomial identity testing', SIAM Journal on Computing, vol. 48, no. 3, pp. 926-963.
View/Download from: UTS OPUS or Publisher's site
View description>>
© 2019 Society for Industrial and Applied Mathematics. We consider two basic algorithmic problems concerning tuples of (skew-)symmetric matrices. The first problem asks us to decide, given two tuples of (skew-)symmetric matrices (B1,..., Bm) and (C1,..., Cm), whether there exists an invertible matrix A such that for every i ∈ {1,..., m}, AtBiA = Ci. We show that this problem can be solved in randomized polynomial time over finite fields of odd size, the reals, and the complex numbers. The second problem asks us to decide, given a tuple of square matrices (B1,..., Bm), whether there exist invertible matrices A and D, such that for every i ∈ {1,..., m}, ABiD is (skew-)symmetric. We show that this problem can be solved in deterministic polynomial time over fields of characteristic not 2. For both problems we exploit the structure of the underlying ∗-algebras (algebras with an involutive antiautomorphism) and utilize results and methods from the module isomorphism problem. Applications of our results range from multivariate cryptography to group isomorphism and to polynomial identity testing. Specifically, these results imply efficient algorithms for the following problems. (1) Test isomorphism of quadratic forms with one secret over a finite field of odd size. This problem belongs to a family of problems that serves as the security basis of certain authentication schemes proposed by Patarin [J. Patarin, in Advances in Cryptology, EUROCRYPT'96, Springer, Berlin, 1996, pp. 33-48]. (2) Test isomorphism of p-groups of class 2 and exponent p (p odd) with order p in time polynomial in the group order, when the commutator subgroup is of order pO(). (3) Deterministically reveal two families of singularity witnesses caused by the skew-symmetric structure. This represents a natural next step for the polynomial identity testing problem, in the direction set up by the recent resolution of the noncommutative rank problem [A. Garg et al., in Proceedings of the 57th Annual IEEE Sy...
Ji, Z 2019, 'The complexity-theoretic Bell inequality', National Science Review, vol. 6, no. 1, p. 21.
View/Download from: Publisher's site
Kaljahi, MA, Palaiahnakote, S, Anisi, MH, Idris, MYI, Blumenstein, M & Khan, MK 2019, 'A scene image classification technique for a ubiquitous visual surveillance system', Multimedia Tools and Applications, pp. 1-28.
View/Download from: UTS OPUS or Publisher's site
View description>>
© 2018 Springer Science+Business Media, LLC, part of Springer Nature The concept of smart cities has quickly evolved to improve the quality of life and provide public safety. Smart cities mitigate harmful environmental impacts and offences and bring energy-efficiency, cost saving and mechanisms for better use of resources based on ubiquitous monitoring systems. However, existing visual ubiquitous monitoring systems have only been developed for a specific purpose. As a result, they cannot be used for different scenarios. To overcome this challenge, this paper presents a new ubiquitous visual surveillance mechanism based on classification of scene images. The proposed mechanism supports different applications including Soil, Flood, Air, Plant growth and Garbage monitoring. To classify the scene images of the monitoring systems, we introduce a new technique, which combines edge strength and sharpness to detect focused edge components for Canny and Sobel edges of the input images. For each focused edge component, a patch that merges nearest neighbor components in Canny and Sobel edge images is defined. For each patch, the contribution of the pixels in a cluster given by k-means clustering on edge strength and sharpness is estimated in terms of the percentage of pixels. The same percentage values are considered as a feature vector for classification with the help of a Support Vector Machine (SVM) classifier. Experimental results show that the proposed technique outperforms the state-of-the-art scene categorization methods. Our experimental results demonstrate that the SVM classifier performs better than rule and template-based methods.
Kaljahi, MA, Shivakumara, P, Idris, MYI, Anisi, MH, Lu, T, Blumenstein, M & Noor, NM 2019, 'An automatic zone detection system for safe landing of UAVs', Expert Systems with Applications, vol. 122, pp. 319-333.
View/Download from: UTS OPUS or Publisher's site
View description>>
© 2019 Elsevier Ltd As the demand increases for the use Unmanned Aerial Vehicles (UAVs) to monitor natural disasters, protecting territories, spraying, vigilance in urban areas, etc., detecting safe landing zones becomes a new area that has gained interest. This paper presents an intelligent system for detecting regions to navigate a UAV when it requires an emergency landing due to technical causes. The proposed system explores the fact that safe regions in images have flat surfaces, which are extracted using the Gabor Transform. This results in images of different orientations. The proposed system then performs histogram operations on different Gabor-oriented images to select pixels that contribute to the highest peak, as Candidate Pixels (CP), for the respective Gabor-oriented images. Next, to group candidate pixels as one region, we explore Markov Chain Codes (MCCs), which estimate the probability of pixels being classified as candidates with neighboring pixels. This process results in Candidate Regions (CRs) detection. For each image of the respective Gabor orientation, including CRs, the proposed system finds a candidate region that has the highest area and considers it as a reference. We then estimate the degree of similarity between the reference CR with corresponding CRs in the respective Gabor-oriented images using a Chi square distance measure. Furthermore, the proposed system chooses the CR which gives the highest similarity to the reference CR to fuse with that reference, which results in the establishment of safe landing zones for the UAV. Experimental results on images from different situations for safe landing detection show that the proposed system outperforms the existing systems. Furthermore, experimental results on relative success rates for different emergency conditions of UAVs show that the proposed intelligent system is effective and useful compared to the existing UAV safe landing systems.
Khare, V, Shivakumara, P, Chan, CS, Lu, T, Meng, LK, Woon, HH & Blumenstein, M 2019, 'A novel character segmentation-reconstruction approach for license plate recognition', Expert Systems with Applications, vol. 131, pp. 219-239.
View/Download from: UTS OPUS or Publisher's site
View description>>
© 2019 Elsevier Ltd Developing an automatic license plate recognition system that can cope with multiple factors is challenging and interesting in the current scenario. In this paper, we introduce a new concept called partial character reconstruction to segment characters of license plates to enhance the performance of license plate recognition systems. Partial character reconstruction is proposed based on the characteristics of stroke width in the Laplacian and gradient domain in a novel way. This results in character components with incomplete shapes. The angular information of character components determined by PCA and the major axis are then studied by considering regular spacing between characters and aspect ratios of character components in a new way for segmenting characters. Next, the same stroke width properties are used for reconstructing the complete shape of each character in the gray domain rather than in the gradient domain, which helps in improving the recognition rate. Experimental results on benchmark license plate databases, namely, MIMOS, Medialab, UCSD data, Uninsbria data Challenged data, as well as video databases, namely, ICDAR 2015, YVT video, and natural scene data, namely, ICDAR 2013, ICDAR 2015, SVT, MSRA, show that the proposed technique is effective and useful.
Korzekwa, K, Chubb, CT & Tomamichel, M 2019, 'Avoiding Irreversibility: Engineering Resonant Conversions of Quantum Resources', PHYSICAL REVIEW LETTERS, vol. 122, no. 11.
View/Download from: UTS OPUS or Publisher's site
Li, Y, Lei, L & Li, S 2019, 'Computation tree logic model checking based on multi-valued possibility measures', Information Sciences, vol. 485, pp. 87-113.
View/Download from: UTS OPUS or Publisher's site
View description>>
© 2019 Elsevier Inc. Multi-valued model checking has been studied extensively recently, but important uncertain information contained in systems of multi-valued logics has not been considered in previous work and, as a consequence, some serious deficiencies arise. To make up for these deficiencies, this paper considers the possibility information implied in multi-valued systems. Precisely, we investigate computation tree logic model checking based on multi-valued possibility measures. We model multi-valued logic systems by multi-valued Kripke structures (MvKSs) and specify their verification properties by multi-valued computation tree logic (MvCTL) formulae. Based on generalized possibility measures and generalized necessity measures, an MvCTL model checking method is proposed, the pseudocode of the corresponding model checking algorithm is presented, and its time complexity is analyzed in detail. Furthermore, after detailed comparisons with χCTL (introduced in Chechik et al. [10]) and the classical CTL, we show that MvCTL is more general than χCTL, but cannot be reduced to the classical CTL. The conditions on lattice and MvKS under which MvCTL is equivalent to χCTL are given. Finally, some examples and a case study are given to illustrate the MvCTL model-checking method.
Liu, S, Li, Y & Duan, R 2019, 'Distinguishing unitary gates on the IBM quantum processor', Science China Information Sciences, vol. 62, no. 7.
View/Download from: UTS OPUS or Publisher's site
View description>>
© 2019, Science China Press and Springer-Verlag GmbH Germany, part of Springer Nature. An unknown unitary gate, which is secretly chosen from several known ones, can always be distinguished perfectly. In this paper, we implement such a task on IBM’s quantum processor. More precisely, we experimentally demonstrate the discrimination of two qubit unitary gates, the identity gate and the 23π-phase shift gate, using two discrimination schemes — the parallel scheme and the sequential scheme. We program these two schemes on the ibmqx4, a 5-qubit superconducting quantum processor via IBM cloud, with the help of the QSI modules. We report that both discrimination schemes achieve success probabilities at least 85%.
Liu, Y, Lan, C, Blumenstein, M & Li, J 2019, 'Bi-level error correction for PacBio long reads', IEEE/ACM Transactions on Computational Biology and Bioinformatics.
View/Download from: Publisher's site
View description>>
IEEE The latest sequencing technologies such as the Pacific Biosciences (PacBio) and Oxford Nanopore machines can generate long reads at the length of thousands of nucleic bases which is much longer than the reads at the length of hundreds generated by Illumina machines. However, these long reads are prone to much higher error rates, for example 15%, making downstream analysis and applications very difficult. Error correction is a process to improve the quality of sequencing data. Hybrid correction strategies have been recently proposed to combine Illumina reads of low error rates to fix sequencing errors in the noisy long reads with good performance. In this paper, we propose a new method named Bicolor, a bi-level framework of hybrid error correction for further improving the quality of PacBio long reads. At the first level, our method uses a de Bruijn graph-based error correction idea to search paths in pairs of solid < formula > < tex > $k$ < /tex > < /formula > -mers iteratively with an increasing length of < formula > < tex > $k$ < /tex > < /formula > -mer. At the second level, we combine the processed results under different parameters from the first level. In particular, a multiple sequence alignment algorithm is used to align those similar long reads, followed by a voting algorithm which determines the final base at each position of the reads. We compare the superior performance of Bicolor with three state-of-the-art methods on three real data sets. Results demonstrate that Bicolor always achieves the highest identity ratio. Bicolor also achieves a higher alignment ratio ( < formula > < tex > $ & #x003E; 1.3\%$ < /tex > < /formula > ) and a higher number of aligned reads than the current methods on two data sets. On the third data set, our method is closely competitive to the current methods in terms of number of aligned reads and genome coverage. The C++ source codes of our algorithm are freely available at https://github.com/yuansliu/Bicolor.
Mandal, R, Roy, PP, Pal, U & Blumenstein, M 2019, 'Bag-of-visual-words for signature-based multi-script document retrieval', Neural Computing and Applications, pp. 1-25.
View/Download from: Publisher's site
View description>>
© 2018 The Natural Computing Applications Forum An end-to-end architecture for multi-script document retrieval using handwritten signatures is proposed in this paper. The user supplies a query signature sample, and the system exclusively returns a set of documents that contain the query signature. In the first stage, a component-wise classification technique separates the potential signature components from all other components. A bag-of-visual-words powered by SIFT descriptors in a patch-based framework is proposed to compute the features and a support vector machine (SVM)-based classifier was used to separate signatures from the documents. In the second stage, features from the foreground (i.e., signature strokes) and the background spatial information (i.e., background loops, reservoirs etc.) were combined to characterize the signature object to match with the query signature. Finally, three distance measures were used to match a query signature with the signature present in target documents for retrieval. The ‘Tobacco’ (The Legacy Tobacco Document Library (LTDL). University of California, San Francisco, 2007. http://legacy.library.ucsf.edu/) document database and an Indian script database containing 560 documents of Devanagari (Hindi) and Bangla scripts were used for the performance evaluation. The proposed system was also tested on noisy documents, and the promising results were obtained. A comparative study shows that the proposed method outperforms the state-of-the-art approaches.
Paler, A, Herr, D & Devitt, SJ 2019, 'Really small shoe boxes: On realistic quantum resource estimation', Computer, vol. 52, no. 6, pp. 27-37.
View/Download from: UTS OPUS or Publisher's site
View description>>
© 2019 IEEE. The reliable resource estimation and benchmarking of quantum algorithms is a critical component of the development cycle of viable quantum applications for quantum computers of all sizes. Determining resource bottlenecks in algorithms, especially when resource intensive error correction protocols are required, is crucial to reduce the cost of implementing viable algorithms on actual quantum hardware.
Razzak, MI, Blumenstein, M & Xu, G 2019, 'Multiclass Support Matrix Machines by Maximizing the Inter-Class Margin for Single Trial EEG Classification.', IEEE transactions on neural systems and rehabilitation engineering : a publication of the IEEE Engineering in Medicine and Biology Society, vol. 27, no. 6, pp. 1117-1127.
View/Download from: UTS OPUS or Publisher's site
View description>>
Accurate classification of Electroencephalogram (EEG) signals plays an important role in diagnoses of different type of mental activities. One of the most important challenges, associated with classification of EEG signals is how to design an efficient classifier consisting of strong generalization capability. Aiming to improve the classification performance, in this paper, we propose a novel multiclass support matrix machine (M-SMM) from the perspective of maximizing the inter-class margins. The objective function is a combination of binary hinge loss that works on C matrices and spectral elastic net penalty as regularization term. This regularization term is a combination of Frobenius and nuclear norm, which promotes structural sparsity and shares similar sparsity patterns across multiple predictors. It also maximizes the inter-class margin that helps to deal with complex high dimensional noisy data. The extensive experiment results supported by theoretical analysis and statistical tests show the effectiveness of the M-SMM for solving the problem of classifying EEG signals associated with motor imagery in brain-computer interface applications.
Rohde, P & Tan, S-H 2019, 'The resurgence of the linear optics quantum interferometer - recent advances & applications', Review in Physics.
Roy, S 2019, 'Fundamental noisy multiparameter quantum bounds', SCIENTIFIC REPORTS, vol. 9.
View/Download from: UTS OPUS or Publisher's site
Saqib, M, Khan, SD, Sharma, N & Blumenstein, M 2019, 'Crowd Counting in Low-Resolution Crowded Scenes Using Region-Based Deep Convolutional Neural Networks', IEEE Access, vol. 7, pp. 35317-35329.
View/Download from: UTS OPUS or Publisher's site
View description>>
© 2013 IEEE. Crowd counting and density estimation is an important and challenging problem in the visual analysis of the crowd. Most of the existing approaches use regression on density maps for the crowd count from a single image. However, these methods cannot localize individual pedestrian and therefore cannot estimate the actual distribution of pedestrians in the environment. On the other hand, detection-based methods detect and localize pedestrians in the scene, but the performance of these methods degrades when applied in high-density situations. To overcome the limitations of pedestrian detectors, we proposed a motion-guided filter (MGF) that exploits spatial and temporal information between consecutive frames of the video to recover missed detections. Our framework is based on the deep convolution neural network (DCNN) for crowd counting in the low-to-medium density videos. We employ various state-of-the-art network architectures, namely, Visual Geometry Group (VGG16), Zeiler and Fergus (ZF), and VGGM in the framework of a region-based DCNN for detecting pedestrians. After pedestrian detection, the proposed motion guided filter is employed. We evaluate the performance of our approach on three publicly available datasets. The experimental results demonstrate the effectiveness of our approach, which significantly improves the performance of the state-of-the-art detectors.
Wang, Q & Ying, M 2019, 'Quantum Büchi Automata', CoRR, vol. abs/1804.08982.
Wang, X, Fang, K & Duan, R 2019, 'Semidefinite Programming Converse Bounds for Quantum Communication', IEEE Transactions on Information Theory, vol. 65, no. 4, pp. 2583-2592.
View/Download from: Publisher's site
View description>>
© 2018 IEEE. We derive several efficiently computable converse bounds for quantum communication over quantum channels in both the one-shot and asymptotic regime. First, we derive one-shot semidefinite programming (SDP) converse bounds on the amount of quantum information that can be transmitted over a single use of a quantum channel, which improve the previous bound from [Tomamichel/Berta/Renes, Nat. Commun. 7, 2016]. As applications, we study quantum communication over depolarizing channels and amplitude damping channels with finite resources. Second, we find an SDP-strong converse bound for the quantum capacity of an arbitrary quantum channel, which means the fidelity of any sequence of codes with a rate exceeding this bound will vanish exponentially fast as the number of channel uses increases. Furthermore, we prove that the SDP-strong converse bound improves the partial transposition bound introduced by Holevo and Werner. Third, we prove that this SDP strong converse bound is equal to the so-called max-Rains information, which is an analog to the Rains information introduced in [Tomamichel/Wilde/Winter, IEEE Trans. Inf. Theory 63:715, 2017]. Our SDP strong converse bound is weaker than the Rains information, but it is efficiently computable for general quantum channels.
Xie, A & Li, S 2019, 'On constructing the largest and smallest uninorms on bounded lattices', Fuzzy Sets and Systems.
View/Download from: Publisher's site
View description>>
© 2019 Elsevier B.V. Uninorms on the unit interval are a common extension of triangular norms (t-norms)and triangular conorms (t-conorms). As important aggregation operators, uninorms play a very important role in fuzzy logic and expert systems. Recently, several researchers have studied constructions of uninorms on more general bounded lattices. In particular, Çaylı (2019)gave two methods for constructing uninorms on a bounded lattice L with e∈L∖{0,1}, which is based on a t-norm T e on [0,e]and a t-conorms S e on [e,1]that satisfy strict boundary conditions. In this paper, we propose two new methods for constructing uninorms on bounded lattices. Our constructed uninorms are indeed the largest and the smallest among all uninorms on L that have the same restrictions T e and S e on [0,e]and, respectively, [e,1]. Moreover, our constructions does not require the boundary condition, and thus completely solved an open problem raised by Çaylı.
Ying, M 2019, 'Toward automatic verification of quantum programs', Formal Aspects of Computing, vol. 31, no. 1, pp. 3-25.
View/Download from: UTS OPUS or Publisher's site
View description>>
© 2018, British Computer Society. This paper summarises the results obtained by the author and his collaborators in a program logic approach to the verification of quantum programs, including quantum Hoare logic, invariant generation and termination analysis for quantum programs. It also introduces the notion of proof outline and several auxiliary rules for more conveniently reasoning about quantum programs. Some problems for future research are proposed at the end of the paper.
Ying, M & Feng, Y 2019, 'Model-checking quantum systems', National Science Review, vol. 6, no. 1, pp. 28-31.
View/Download from: UTS OPUS or Publisher's site
Zhou, L, Ying, S, Yu, N & Ying, M 2019, 'Quantum Coupling and Strassen Theorem.', CoRR, vol. abs/1803.10393.
Zhu, EY, Zhuang, Q, Hsieh, MH & Shor, PW 2019, 'Superadditivity in trade-off capacities of quantum channels', IEEE Transactions on Information Theory, vol. 2018.
View/Download from: UTS OPUS or Publisher's site
View description>>
IEEE In this article, we investigate the additivity phenomenon in the quantum dynamic capacity region of a quantum channel for trading the resources of classical communication, quantum communication, and entanglement. Understanding such an additivity property is important if we want to optimally use a quantum channel for general communication purposes. However, in a lot of cases, the channel one will be using only has an additive single or double resource capacity region, and it is largely unknown if this could lead to a strictly superadditive double or triple resource capacity region, respectively. For example, if a channel has additive classical and quantum capacities, can the classical-quantum capacity region be strictly superadditive? In this work, we answer such questions affirmatively. We give proof-of-principle requirements for these channels to exist. In most cases, we can provide an explicit construction of these quantum channels. The existence of these superadditive phenomena is surprising in contrast to the result that the additivity of both classical-entanglement and classical-quantum capacity regions imply the additivity of the triple resource capacity region for a given channel.
Lee, T, Ray, M & Santha, M 2019, 'Strategies for quantum races', Innovations in Theoretical Computer Science, UCSD.
View/Download from: UTS OPUS
Liu, J, Zhan, B, Wang, S, Ying, S, Liu, T, Li, Y, Ying, M & Zhan, N 2019, 'Formal verification of quantum algorithms using quantum hoare logic', Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 187-207.
View/Download from: Publisher's site
View description>>
© The Author(s) 2019. We formalize the theory of quantum Hoare logic (QHL) [TOPLAS 33(6),19], an extension of Hoare logic for reasoning about quantum programs. In particular, we formalize the syntax and semantics of quantum programs in Isabelle/HOL, write down the rules of quantum Hoare logic, and verify the soundness and completeness of the deduction system for partial correctness of quantum programs. As preliminary work, we formalize some necessary mathematical background in linear algebra, and define tensor products of vectors and matrices on quantum variables. As an application, we verify the correctness of Grover’s search algorithm. To our best knowledge, this is the first time a Hoare logic for quantum programs is formalized in an interactive theorem prover, and used to verify the correctness of a nontrivial quantum algorithm.
Saqib, M, Daud Khan, S, Sharma, N, Scully-Power, P, Butcher, P, Colefax, A & Blumenstein, M 2019, 'Real-Time Drone Surveillance and Population Estimation of Marine Animals from Aerial Imagery', International Conference Image and Vision Computing New Zealand.
View/Download from: UTS OPUS or Publisher's site
View description>>
© 2018 IEEE. Video analysis is being rapidly adopted by marine biologists to asses the population and migration of marine animals. Manual analysis of videos by human observers is labor intensive and prone to error. The automatic analysis of videos using state-of-the-art deep learning object detectors provides a cost-effective way for the study of marine animals population and their ecosystem. However, there are many challenges associated with video analysis such as background clutter, illumination, occlusions, and deformation. Due to the high-density of objects in the images and sever occlusion, current state-of-the-art object often results in multiple detections. Therefore, customized Non-Maxima-Suppression is proposed after the detections to suppress false positives which significantly improves the counting and mean average precision of the detections. An end-to-end deep learning framework of Faster-RCNN [1] was adopted for detections with base architectures of VGG16 [2], VGGM [3] and ZF [4].
Wu, D, Chen, J, Sharma, N, Pan, S, Long, G & Blumenstein, M 2019, 'Adversarial Action Data Augmentation for Similar Gesture Action Recognition', The 2019 International Joint Conference on Neural Networks (IJCNN), Budapest, Hungary.
Wu, D, Sharma, N & Blumenstein, M 2018, 'An End-to-End Hierarchical Classification Approach for Similar Gesture Recognition', 2018 International Conference on Image and Vision Computing New Zealand (IVCNZ 2018), International Conference on Image and Vision Computing New Zealand, IEEE, New Zealand, pp. 73-78.
View/Download from: UTS OPUS or Publisher's site
View description>>
© 2018 IEEE. Human action recognition from the RGB video is widely applied on varies real applications. Many works have been done by researchers in computer vision and machine learning area to address the challenges and complexity involved in video-based human action recognition. Deep learning approaches including Convolutional Neural Networks (CNN) and Recurrent Neural Networks (RNN) have been introduced in the human action recognition research area. However, due to the drawbacks of the CNNs, recognizing actions with similar gestures and describing complex actions is still very challenging. Hence, an end-to-end hierarchical classification architecture has been proposed in this paper to resolve the confusion between similar gesture. The proposed approach firstly classifies the whole dataset and generates the accuracy for each class in stage 1. Based on the confusion matrix obtained from stage-1, the approach combines the most confused similar gesture pairs into one class, and classify them along with all other class, in the stage-2. In stage 3, similar gesture pairs will be classified by binary classifiers, which will increase the performance of each class and the overall accuracy. We apply and evaluate the developed models to recognize the similar human actions on the both KTH and UCF101 dataset. The result shows that the proposed approach can boost the classification performance on both the datasets. The proposed architecture is robust and any classification technique can be used in stage 1 and stage 2.
Wu, D, Sharma, N & Blumenstein, M 2019, 'Similar Gesture Recognition using Hierarchical Classification Approach in RGB Videos', 2018 International Conference on Digital Image Computing: Techniques and Applications, DICTA 2018.
View/Download from: UTS OPUS or Publisher's site
View description>>
© 2018 IEEE. Recognizing human actions from the video streams has become one of the very popular research areas in computer vision and deep learning in the recent years. Action recognition is wildly used in different scenarios in real life, such as surveillance, robotics, healthcare, video indexing and human-computer interaction. The challenges and complexity involved in developing a video-based human action recognition system are manifold. In particular, recognizing actions with similar gestures and describing complex actions is a very challenging problem. To address these issues, we study the problem of classifying human actions using Convolutional Neural Networks (CNN) and develop a hierarchical 3DCNN architecture for similar gesture recognition. The proposed model firstly combines similar gesture pairs into one class, and classify them along with all other class, as a stage-1 classification. In stage-2, similar gesture pairs are classified individually, which reduces the problem to binary classification. We apply and evaluate the developed models to recognize the similar human actions on the HMDB51 dataset. The result shows that the proposed model can achieve high performance in comparison to the state-of-the-art methods.
Zhou, L, Yu, N & Ying, M 2019, 'An applied quantum hoare logic', Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 1149-1162.
View/Download from: Publisher's site
View description>>
© 2019 Association for Computing Machinery. We derive a variant of quantum Hoare logic (QHL), called applied quantum Hoare logic (aQHL for short), by: (1) restricting QHL to a special class of preconditions and postconditions, namely projections, which can significantly simplify verification of quantum programs and are much more convenient when used in debugging and testing; and (2) adding several rules for reasoning about robustness of quantum programs, i.e. error bounds of outputs. The effectiveness of aQHL is shown by its applications to verify two sophisticated quantum algorithms: HHL (Harrow-Hassidim-Lloyd) for solving systems of linear equations and qPCA (quantum Principal Component Analysis).