2) Inconsistency Measures in Knowledge and Information Systems

Kedian Mu together with his collaborators, have made several original contributions to the area of inconsistency measures in knowledge and information systems with application to managing non-canonical software requirements. In particular, an innovative approach to measuring the responsibility of each formula in a knowledge base for the inconsistency of that base was proposed in [Mu, IJAR (2015)], which can be well explained in the context of causal models. The anonymous reviewers of this article have pointed out that the use of causality is an entirely new method for this type of measurement, and it clearly advances the state of the art. In [Mu-Hong-Jin-Liu, IJAR (2013)], Kedian Mu and his collaborators proposed a measure-driven logical framework for managing non-canonical software requirements, including inconsistency, redundancy, and incompleteness. This is the first work to provide an integrated theory for measuring inconsistency, incompleteness, and redundancy, and there is a substantial interest in various fields.

2. Formal Methods and Software (SUN Meng, XIA Bican)

1) Verification and Testing of Complex Systems

Model-based testing approaches are usually based on some specific state-based models like automata or LTS and have been successfully applied in many areas. However, it is difficult to apply general model-based techniques for connector testing because the causality between inputs and outputs are made implicit in the constraint automata semantics for connectors. In [Sun-Aichernig-Arbab-Astefanoaei-deBoer-Rutten, SCP (2012)], the design semantics for connectors was proposed based on Unifying Theories of Programming (UTP), and an algorithm for generating test cases of connectors based on this UTP model was developed. Both soundness and completeness of this algorithm have been proved. Users can prove refinement and equivalence relations between connectors and construct test cases for connectors by using term rewriting techniques in JTom, or using theorem proving techniques in Coq. In [Li-Chen-Wang-Sun, TASE (2015)] an off-line conformance testing framework for timed connectors was developed, which leads to the best paper award in TASE 2015. Hybrid systems exhibit both continuous and discrete behavior. Analyzing hybrid systems is known to be very hard. Inspired by the idea of concolic testing (of programs), Meng Sun and his collaborators investigate whether random sampling and symbolic execution can be combined to effectively verify hybrid systems in [Kong-Li-Chen-Sun-Sun-Wang, FM (2016)]. A sufficient condition is identified under which such a combination is more effective than random sampling. Furthermore, different strategies of combining random sampling and symbolic execution are analyzed and an algorithm which allows us to dynamically switch between them so as to reduce the overall cost was proposed. The method has been implemented as a web-based checker named HyChecker.

2) Symbolic Computation and Program Verification

Interpolation-based techniques have been widely and successfully applied in the verification of hardware and software, e.g., in bounded-model checking, CEGAR, SMT, etc., in which the hardest part is how to synthesize interpolants. Various work for discovering interpolants for propositional logic, quantifier-free fragments of first-order theories and their combinations have been proposed. However, little work focuses on discovering polynomial interpolants in the literature. In [Dai-Xia-Zhan, CAV (2013)], Xia and his collaborators provide an approach for constructing non-linear interpolants based on semidefinite programming, and show how to apply such results to the verification of programs by examples. In [Hong-Tang-Xia, JSC (2015)] Xia et al. consider the problem of counting (stable) equilibriums of an important family of algebraic differential equations modeling multistable biological regulatory systems. The problem can be solved, in principle, using real quantifier elimination algorithms, in particular real root classification algorithms. However, it is well known that they can handle only very small cases due to the enormous computing time requirements. Xia and his collaborators present a special algorithm which is much more efficient than the general methods. Its efficiency comes from the exploitation of certain interesting structures of the family of differential equations.

In [Gan-Dai-Xia-Zhan-Kapur-Chen, IJCAR (2016)], Xia and his collaborators developed an algorithm for generating interpolants for formulas which are conjunctions of quadratic polynomial inequalities (both strict and nonstrict). The algorithm is based on a key observation that quadratic polynomial inequalities can be linearized if they are concave. A generalization of Motzkin’s transposition theorem is proved, which is used to generate an interpolant between two mutually contradictory conjunctions of polynomial inequalities, using semi-definite programming in time complexity (n³+nm), where n is the number of variables and m is the number of inequalities (This complexity analysis assumes that despite the numerical nature of approximate SDP algorithms, they are able to generate correct answers in a fixed number of calls). Using the framework for combining interpolants for a combination of quantifier-free theories which have their own interpolation algorithms, a combination algorithm is given for the combined theory of concave quadratic polynomial inequalities and the equality theory over uninterpreted functions (EUF).

 

3. Cryptography and Information Security (XU Maozhi)

The Gallant-Lambert-Vanstone (GLV) method is a very efficient technique for accelerating point multiplication on elliptic curves with efficiently computable endomorphisms. Galbraith et al. (Galbraith-Lin-Scott, J. Cryptology (2011)) showed that point multiplication exploiting the 2-dimensional GLV method on a large class of curves over 𝔽_p² was faster than the standard method on general elliptic curves over 𝔽_p, and left as an open problem to study the case of 4-dimensional GLV on special curves (e.g., j (E) = 0) over 𝔽_p² . Maozhi Xu and his collaborators studied the above problem in [Hu-Longa-Xu, DCC (2012)]. They show how to get the 4-dimensional GLV decomposition with proper decomposed coefficients, and thus reduce the number of doublings for point multiplication on these curves to only a quarter. The resulting implementation shows that the 4-dimensional GLV method on a GLS curve runs in about 0.78 the time of the 2-dimensional GLV method on the same curve and in between 0.78−0.87 the time of the 2-dimensional GLV method using the standard method over 𝔽_p. In particular, our implementation reduces by up to 27% the time of the previously fastest implementation of point multiplication on x86-64 processors due to Longa and Gebotys (CHES 2010).

Cyclic codes with two zeros and their dual codes as a practically and theoretically interesting class of linear codes have been studied for many years and find many applications. The determination of the weight distributions of such codes is an open problem. Generally, the weight distributions of cyclic codes are difficult to determine. Utilizing a class of elliptic curves, the work by Maozhi Xu and his collaborators in [Wang-Tang-Qi-Yang-Xu, TIT (2012)] determines the weight distributions of dual codes of q-ary cyclic codes with two zeros for a few more cases, where q is an odd prime power.

Galbraith, Lin and Scott (EUROCRYPT 2009) constructed a class of elliptic curves over 𝔽_p² (a.k.a GLS curves) on which the Gallant-Lambert-Vanstone (GLV) method can be employed for fast scalar multiplication. In [Hu-Zhang-Xu, IPL (2016)], Maozhi Xu and his collaborators give an alternative way to implement the quadratic extension field arithmetic for GLS curves, and exploit some explicit decomposition to support 4 dimensional GLV method on GLS curves with special complex multiplication (CM). Such techniques usually bring more computational benefits compared with previous methods. Specially, we give a fair comparison between the cost of 4 GLV based scalar multiplication on GLS curve with CM discriminant −8 and that on the Jacobian of its isogenous FKT genus 2 curve. Our implementations indicate that scalar multiplication on the Jacobian of hyperelliptic curve in Scholten model has competitive efficiency with that on its isogenous GLS curve in twisted Edwards model.

4. Image Reconstruction (JIANG Ming, YANG Jiansheng, MAO Heng)

1) Propagation Model (JIANG Ming)

Radiative transfer equation has a long history and has recently found its applications in optical imaging technology, mainly for imaging through the non-transparent, non-homogeneous and non-isotropic in vivo tissue. There have been three different formulations of the radiative transfer equation for media with spatially varying refractive index. Because the radiative transfer equation demonstrates macroscopic phenomena of light propagation, the intensity law of geometric optics is the criterion to validate these formulations. In [Ming Jiang, Physical Review A (2014)], we reviewed the different formulations and compute the steady-state intensity for each of the radiative transfer equations in a non-absorption and non-scattering medium with a spatially variant refraction index without light sources. By checking each one of the intensities with the intensity law from geometric optics, we find only one formulation consistent with the intensity law of geometric optics.

2) Aerosol Retrieval (JIANG Ming)

Atmospheric aerosols serve as an important factor in air quality and to public health. Aerosol retrieval is to estimate the distribution of aerosol optical depth (AOD) from remote-sensing observations, which is technically an optical tomography problem. In [Ming Jiang, Journal of the American Statistical Association (2013)], by using the radiances observed by NASA’s Multi-angle Imaging Spectroradiometer (MISR), we established a hierarchical Bayesian model for aerosol retrieval and component identification at an improved resolution from MISR’s operational 17.6 km to 4.4 km. We assessed our retrieval performance using ground-based measurements from the AERONET and satellite images from Google Earth.

3) CT Reconstruction (JIANG Ming, YANG Jiansheng)

Interior SPECT problem is a classical ill-posed problem in imaging field. We developed an approach for solving the computed tomography (CT) interior problem based on the high order TV (HOT) minimization, assuming that a region of interest (ROI) is piecewise polynomial. In [Jiansheng Yang, Inverse Problems (2012)], we generalized this finding from the CT field to the single photon emission computed tomography (SPECT) field, and proved that if an ROI is piecewise polynomial, then the ROI can be uniquely reconstructed from the SPECT projection data associated with the ROI through the HOT minimization. Also, we proposed a new formulation of HOT, which has an explicit formula for any n-order piecewise polynomial function, while the original formulation has no explicit formula for n≥2. This work is selected to the Highlights Collections of 2012 of Inverse Problems.

Regularization technique with priors or other regularization approaches within the general Bayesian inference are necessary, while the imaging and image reconstruction problems are typical ill-posed inverse problems. With collaborators, we developed the theory and algorithms of higher order total variations in [Ming Jiang, Inverse Problems, 2014], which is a non-trivial extension of the widely used total variations regularization, and has applied it successfully to interior tomography of x-ray CT and SPECT. One recent work is the regularization properties of the Mumford-Shah functional, which can be used to reconstruct image and its segmentation simultaneously. The advantage of the Mumford-Shah functional is that it is a coupled image and edge prior. The coupled edge prior can help improve the reconstructed image quality, which is missed in other conventional priors. This work is selected to the Highlights Collections of 2014 of Inverse Problems.

4) Bioluminescence Tomography (MAO Heng)

Bioluminescence tomography (BLT) is a promising optical molecular imaging technique on the frontier of biomedical optics. In [Heng Mao, Biomedical Optics Express (2013)], a generalized hybrid algorithm has been proposed based on the graph cuts algorithm and gradient-based algorithms. The graph cuts algorithm is adopted to estimate a reliable source support without prior knowledge, and different gradient-based algorithms are sequentially used to acquire an accurate and fine source distribution according to the reconstruction status. Furthermore, multilevel meshes for the internal sources are used to speed up the computation and improve the accuracy of reconstruction. Numerical simulations have been performed to validate this proposed algorithm and demonstrate its high performance in the multi-source situation even if the detection noises, optical property errors and phantom structure errors are involved in the forward imaging.

5. Pattern Recognition (MA Jinwen, GAN Rui)

1) Semantic Segmentation (GAN Rui)

Semantic segmentation is a fundamental but difficult problem in computer vision. Compared with image classification, it provides a pixel-wise semantic understanding of the image, through which the scene is parsed in terms of object categories, locations and shapes. Deep networks have made a series of breakthroughs on the task of image classification. In [Rui Gan, IEEE CVPR (2017)], we described a fast and accurate semantic image segmentation approach that encodes not only segmentation specified features but also high-order context compatibilities and boundary guidance constraints. We introduce a structured patch prediction technique to make a trade-off between classification discriminability and boundary sensibility for features. Both label and feature contexts are embedded to ensure recognition accuracy and compatibility, while the complexity of the high order cliques is reduced by a distance-aware sampling and pooling strategy. The proposed joint model also employs a guidance CRF to further enhance the segmentation performance. The message passing step is augmented with the guided filtering which enables an efficient and joint training of the whole system in an end-to-end fashion. Our proposed joint model outperforms the state-of-art on Pascal VOC 2012 and Cityscapes, with mIoU(%) of 82.5 and 79.2 respectively. It also reaches a leading performance on ADE20K, which is the dataset of the scene parsing track in ILSVRC 2016.

2) Bayesian Texture Classification (MA Jinwen )

Texture classification is an important but difficult task in image processing and pattern recognition. From different aspects, there have been established a variety of texture classification methods during the last three decades. In fact, they can be broadly divided into two categories, namely, spatial-domain methods and transformed-domain methods, which are also referred to as filter-based methods or signal-processing methods. In [Jinwen Ma, IEEE Trans. on Image Processing (2012)], we proposed a novel Bayesian texture classifier based on the adaptive model-selection learning of Poisson mixtures on the contourlet features of texture images. The adaptive model-selection learning of Poisson mixtures is carried out by the recently established adaptive gradient Bayesian Ying-Yang harmony learning algorithm for Poisson mixtures. It is demonstrated by the experiments that our proposed Bayesian classifier significantly improves the texture classification accuracy in comparison with several current state-of-the-art texture classification approaches.

3) Human Detection (MA Jinwen)

Human Detection is a primary issue among object detection, due to the specificity of human bodies in our daily lives. Unlike pedestrian detection, human detection is still a challenging problem because of the large variations in visual appearance, which can be caused by various viewpoints and scales in photo-taking, different clothes and poses on target people, changeful illumination and large intra-class variations. In [Jinwen Ma, IEEE CVPR (2015)], we presented effective combination models with certain combination features for human detection. Specifically, we combine certain complementary features/models together with effective organization/fusion methods. Actually, the HOG features, colour features and bar-shape features are combined together with a cell-based histogram structure to form the so-called HOG-III features. Moreover, the detections from different models are fused together with the new proposed weighted-NMS algorithm, which enhances the probable “true” activations as well as suppresses the overlapped detections. The experiments on PASCAL VOC datasets demonstrate that, both the HOG-III features and the weighted-NMS fusion algorithm are effective and efficient. When applied to human detection task with the Grammar model and Poselet model, they can boost the detection performance significantly. Also, when extended to detection of the whole VOC 20 object categories with the deformable part-based model and deep CNN-based model, they still show competitive improvements.

4) Drug Combination Discovery (MA Jinwen)

Ideal drug combinations expected by clinicians are combinations of Food and Drug Administration (FDA)-approved drugs or existing bioactive compounds that have entered clinical trials and passed safety tests. These drug combinations could be used by patients without toxic side effects. Drug combination prediction has been a challenging task in computational biology, despite a few studies in the area. In [Jinwen Ma, Bioinformatics (2014)], we propose a novel systematic computational tool Drug Combo Ranker to prioritize synergistic drug combinations and uncover their mechanisms of action. We first build a drug functional network based on their genomic profiles, and partition the network into numerous drug network communities by using a Bayesian non-negative matrix factorization approach. As drugs within overlapping community share common mechanisms of action, we next uncover potential targets of drugs by applying a recommendation system on drug communities. We meanwhile build disease-specific signaling networks based on patients’ genomic profiles and interactome data. We then identify drug combinations by searching drugs whose targets are enriched in the complementary signaling modules of the disease signaling network. The novel method was evaluated on lung adenocarcinoma and endocrine receptor positive breast cancer, and compared with other drug combination approaches. These case studies discovered a set of effective drug combinations top ranked in our prediction list, and mapped the drug targets on the disease signaling network to highlight.