Mar 2008, Volume 2 Issue 1
    

  • Select all
  • ZHANG Jian, ZHANG Wenhui, ZHAN Naijun, SHEN Yidong, CHEN Haiming, ZHANG Yunquan, WANG Yongji, WU Enhua, WANG Hongan, ZHU Xueyang
    The State Key Laboratory of Computer Science (SKLCS) is committed to basic research in computer science and software engineering. The research topics of the laboratory include: concurrency theory, theory and algorithms for real-time systems, formal specifications based on context-free grammars, semantics of programming languages, model checking, automated reasoning, logic programming, software testing, software process improvement, middleware technology, parallel algorithms and parallel software, computer graphics and human-computer interaction. This paper describes these topics in some detail and summarizes some results obtained in recent years.
  • SATO Masahiko, IGARASHI Atsushi, SAKURAI Takafumi, KAMEYAMA Yukiyoshi
    The notion of meta-variable plays a fundamental role when we define formal systems such as logical and computational calculi. Yet it has been usually understood only informally as is seen in most textbooks of logic. Based on our observations of the usages of meta-variables in textbooks, we propose two formal systems that have the notion of meta-variable.In both calculi, each variable is given a level (non-negative integer), which classifies variables into object variables (level 0), meta-variables (level 1), metameta-variables (level 2) and so on. Then, simple arity systems are used to exclude meaningless terms like a meta-level function operating on the metameta-level. A main difference of the two calculi lies in the definitions of substitution. The first calculus uses textual substitution, which can often be found in definitions of quantified formulae: when a term is substituted for a meta-variable, free object-level variables in the term may be captured. The second calculus is based on the observation that predicates can be regarded as meta-level functions on object-level terms, hence uses capture-avoiding substitution.We show that both calculi enjoy a number of properties including Church-Rosser and Strong Normalization, which are indispensable when we use them as frameworks to define logical systems.
  • CHEN Yixiang, WU Hengyang
    The aim of this paper is to extend the probabilistic choice in probabilistic programs to sub-probabilistic choice, i.e., of the form Graphic
    ZHOU Wenqin, J. JEFFREY David
    Gaussian elimination and LU factoring have been greatly studied from the algorithmic point of view, but much less from the point view of the best output format. In this paper, we give new output formats for fraction free LU factoring and for QR factoring. The formats and the algorithms used to obtain them are valid for any matrix system in which the entries are taken from an integral domain, not just for integer matrix systems. After discussing the new output format of LU factoring, the complexity analysis for the fraction free algorithm and fraction free output is given. Our new output format contains smaller entries than previously suggested forms, and it avoids the gcd computations required by some other partially fraction free computations. As applications of our fraction free algorithm and format, we demonstrate how to construct a fraction free QR factorization and how to solve linear systems within a given domain.
  • CHEN Lifei, JIANG Qingshan
    Clustering high dimensional data has become a challenge in data mining due to the curse of dimensionality. To solve this problem, subspace clustering has been defined as an extension of traditional clustering that seeks to find clusters in subspaces spanned by different combinations of dimensions within a dataset. This paper presents a new subspace clustering algorithm that calculates the local feature weights automatically in an EM-based clustering process. In the algorithm, the features are locally weighted by using a new unsupervised weighting method, as a means to minimize a proposed clustering criterion that takes into account both the average intra-clusters compactness and the average inter-clusters separation for subspace clustering. For the purposes of capturing accurate subspace information, an additional outlier detection process is presented to identify the possible local outliers of subspace clusters, and is embedded between the E-step and M-step of the algorithm. The method has been evaluated in clustering real-world gene expression data and high dimensional artificial data with outliers, and the experimental results have shown its effectiveness.
  • XIAO Chuangbai, YU Jing, SU Kaina
    The topic of super-resolution image reconstruction has recently received considerable attention among the research community. Super-resolution image reconstruction methods attempt to create a single high-resolution image from a number of low-resolution images (or a video sequence). The method of projections onto convex sets (POCS) for super-resolution image reconstruction attracts many researchers’ attention. In this paper, we propose an improvement to reduce the amount of Gibbs artifacts presenting on the edges of the high-resolution image reconstructed by the POCS method. The proposed method weights the blur PSF centered at an edge pixel with an exponential function, and consequently decreases the coefficients of the PSF in the direction orthogonal to the edge. Experiment results show that the modification reduces effectively the visibility of Gibbs artifacts on edges and improves obviously the quality of the reconstructed high-resolution image.
  • WANG Lingling, ZHANG Guoyin, MA Chunguang
    Deniable ring authentication allows a member of an ad-hoc sunset of participants to authenticate a message without revealing which member has issued the signature, and the verifier cannot transfer the signature to any third party. It is an important cryptographic primitive for privacy and anonymous communication. Unfortunately, the size of the signature of the proposed deniable ring authentication is dependent on the size of the ring. It is inefficient especially when the size of the ring is large. In this paper, we propose an ID-based version of deniable ring authentication. We present a generic construction which uses dynamic accumulators to construct ID-based deniable ring authentication with constant-size signature. We also give an ID-based deniable ring authentication based on bilinear pairings, which is proved to be secure in the random oracle model.