PSL (property specification language) is a property specification language to describe parallel systems and can be divided into two parts,FL (foundation language) and OBE (optional branching extension). Since OBE is essentially the temporal logic CTL (computation tree logic),and PSL formulas with clock statements can be easily rewritten to unclocked formulas,this paper plays an emphasis on the unclocked FL logic. In order to be model-checked,each FL formula needs to be translated into a verifiable form,usually as an automaton (nondeterministic automaton). The translation into nondeterministic automata can be realized mainly by the construction of alternating automata. The translation rules for the two-way alternating automata from unclocked FL logic are explained in detail in this paper. The core logic of the construction rules is not only limited to an extension of LTL (linear temporal logic) with regular expressions,but considers overall FL operators adequately. A translation method from two-way alternating automata to nondeterministic automata is also provided. Finally,a translation tool from PSL formulas to the above two automata has been written. The complexity of the construction rules for the two-way alternating automata grows linearly with the length of the FL formulas,and at the same time,the correctness of the rules is verified. It is also proved that the two-way alternating automata and its corresponding nondeterministic automata accept the same language. The work above has important theoretical and application values for the modeling and model checking for the complex parallel systems.

This paper presents an efficient hybrid simulated annealing algorithm for three dimensional container loading problem (3D-CLP). The 3D-CLP is the problem of loading a subset of a given set of rectangular boxes into a rectangular container so that the stowed volume is maximized. The algorithm introduced in this paper is based on three important algorithms. First, complex block generating, complex block can contain any number boxes of different types, which differs from the traditional algorithm. Second, basic heuristic, which is a new construction heuristic algorithm used to generate a feasible packing solution from a packing sequence. Third, simulated annealing algorithm, based on the complex block and basic heuristic, it encodes a feasible packing solution as a packing sequence, and searches in the encoding space to find an approximated optimal solution. 1500 benchmark instances with weakly and strongly heterogeneous boxes are considered in this paper. The computational results show that the volume utilization of hybrid algorithm outperforms current excellent algorithms for the considered problem.

Property specification language (PSL) is a specification language which has been accepted as an industrial standard. In PSL, SEREs are used as additional formula constructs. In this paper, we present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. Then, we extend the LTL symbolic model checking algorithm to that of APSL, and then present a tableau based APSL verification technique, which can be easily implemented via the BDD based symbolic approach. Moreover, we implement an extension of NuSMV, and this adapted version supports symbolic model checking of APSL. Experimental results show that this variant of PSL can be efficiently verified. Henceforth, symbolic model checking PSL can be carried out by a transformation from PSL to APSL and symbolic model checking APSL.

This paper presents a model based on discrete no-fit polygon for the two-dimensional irregular packing problem.Burke et al. have presented an effective BLF algorithm to solve the irregular packing problem, however, their algorithm might generate invalid results for some special cases.To solve this problem, a model based on discrete no-fit polygon is proposed, and its correctness has been strictly proved.Only points and intervals are only considered by this model, which greatly decreases the geometry complexity of the original problem and makes the problem easily solved by many heuristic strategies.Computational results show that the algorithm based on discrete no-fit polygon model is very efficient.

This paper incorporates time constraints in the Horn logic model, and this extended model can verify Wide-Mouthed-Frog protocol quickly. It discusses relations between the constraint system and Horn model, abstracts the constraint system, and gives the proofs of some propositions and theorems. We also give the algorithm about how to compute the abstract constraint, and analyze its complexity. As a case study we discuss the verification of Wide-Mouthed-Frog protocol whose attack can be found quickly in new model. Therefore, the method in this paper is very effective in verification of time sensitive security protocols. In the future, we will use this method to verify some complex protocols, such as Kerberos protocol etc.

Task assignment is one of the key technologies of workflow management.We analyzed the current academic researches and workflow products,found that the description of task assignment is very weak.We provide a new rule-based workflow task assignment description model to promote the expressing power,flexibility,and ease of use.The key features of the task assignment model are business rule based and using bidirectional navigation in the organization model and the workflow model.Especially,the organization model is very close to the actual business environment,not just the roles and employees.

This paper proves that the complexity of reasoning in the basic description logic(DL)ALC w.r.t.CBox is NExpTime-complete.This means that the reasoning in DL w.r.t.CBox is commonly difficult.Furthermore,we point out what kind of DLs is sensitive to the coding of number in cardinality restrictions.

Topic Detection and Tracking refers to automatic techniques for locating topically related materials in streams of data. As a core of it, story link detection is to determine whether two stories are about the same topic. Up to now, many representation models have been used in story link detection. But few of them are specific to stories. This paper proposes an event model based on the characters of stories. This model is used for story link detection and evaluated on the TDT4 Chinese corpus. The experimental results indicate that the system using the event model achieves a better performance than that using the baseline model. Furthermore, it shows a larger improvement to the former, especially when using uneven SVM as the multi-similarity integration strategy.

Semantic Role Labeling (SRL) as a Shallow Semantic Parsing causes more and more attention recently. The shortage of manually tagged data is one of main obstacles to supervised learning, which is even serious in SRL. Transductive SVM (TSVM) is a novel semi-supervised learning method special to small mount of tagged data. In this paper, we introduce an application of TSVM in Chinese SRL. To improve the performance of TSVM, some heuristics have been designed from the semantic perspective. The experiment results on Chinese Propbank showed that TSVM outperforms SVM in small tagged data, and after using heuristics, it performs further better.

Topic Detection and Tracking refers to automatic techniques for locating topically related materials in streams of data. As the core technology of it, story link detection is to determine whether two stories are about the same topic. To overcome the limitation of the story length and the topic dynamic evolution problem in data streams, this paper presents a method of applying dynamic information extending to improve the performance of link detection. The proposed method uses previous latest related story to extend current processing story, generates new dynamic models for computing the similarity between the current two stories. The work is evaluated on the TDT4 Chinese corpus, and the experimental results indicate that story link detection using this method can make much better performance on all evaluation metrics.

The tumor diagnosis method based on gene expression profiles will be developed into the fast and effective method in clinical domain in the near future. Although DNA microarray experiments provide us with huge amount of gene expression data, only a few of genes are related to tumor in gene expression profiles. Moreover, it is difficult to select informative genes related to tumor from gene expression profiles because of its characteristics such as high dimensionality, small sample set and many noises in gene expression profiles. According to its characteristic, a novel heuristic breadth-first search algorithm based on support vector machines is proposed, which can simultaneously find as many informative gene subsets as possible in which the number of informative genes is almost least but its classification performance is almost highest in spite of its time-consuming characteristic. Three tumor sample sets are examined by the novel approach and experiments show that the novel approach is feasible and effective in tumor classification. Experiment results show that 100% of 4-fold cross-validation accuracy has been achieved by only two, four and four genes for leukemia, colon tumor and SRBCT (Small Round Blue Cells Tumor) datasets, respectively, which is superior to the results of other tumor classification methods. To avoid the affect of different partition of sample set, the full-fold cross-validated method that can more objectively evaluate the classification performance of informative gene subset is proposed.

PSL is a kind of temporal logic which uses SEREs as additional formula constructs. We present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. In this paper, we extend the LTL symbolic model checking algorithm to that of APSL, and present a tableau based APSL verification approach. Moreover, we show how to implement this algorithm via the BDD based symbolic approach.

This paper researches the characteristic of time sensitive protocols and presents a method with simple operations to verify protocols with time stamps and avoid false attacks. Firstly, an extension of π calculus is given to model a time sensitive security protocol. And then, by appending linear arithmetic constraints to the Horn logic model, the extended Horn logic model of security protocols and the modified-version verification method with time constraints are represented. All operations and the strategy of verification are defined for our constraints system. Thirdly, a method is given to determine whether the constraints has a solution or not. Finally, as a result of an experiment, Denning-Sacco protocol with time stamps is verified. The experiment shows that our approach is an innovative and effective method on verifying time sensitive security protocols.

Fuzzy classification is an important application of fuzzy set theory and has been widely applied in many fields.Fuzzy classification rules are widely considered a well-suited representation of classification knowledge.This paper introduces a fuzzy classification model based on the proposed fuzzy kernel hyperball perceptron(FKHP) learning method.This classification model uses kernel function and perception method to automatically generate fuzzy partition and automatically create fuzzy classification rule. In constructing this model, firstly the patterns in the initial input space are mapped to high dimensional feature space by selecting a suitable kernel function.Then in the feature space, the hyperball which covers all training patterns of a class is founded for every class by the proposed FKHP algorithm. A hyperball is regarded as a fuzzy partition and a hyper-cone membership function is defined regarding the center and radius of the hyperball as parameters. An IF-THEN rule is created for a fuzzy partition,and a hyper-cone membership function is defined for a fuzzy partition. Finally, considering the possibility that each hyperball has folded regions,rules are tuned regarding the hyperball’s radius as tuning parameter.The model structure,the rule generated algorithm and the rule tunning policy are introduced in the paper.Since this classification model uses the theory of fuzzy set,kernel method and perception,the learning rate of rules is fast and the astringency of learning is fine, and the rules are strongly interpretable.This classification model is called FKHPBFCM(a FKHP-based fuzzy classification model).Experiments with the data sets of standard machine leaning database evaluate the performances of this model with comparison to experiment results of the methods of kernel hyperball perceptron(KHP) and support vector machine(SVM),and experiment results show this model has the faster classification training rate, better astringency and higher recognition rate.

Semantic parsing is a fundamental problem in natural language understanding. Shallow semantic parsing, as methodology, can be a novel strategy. the rationale and development of shallow semantic parsing is explored, and the definitions, corpus and approaches to semantic role labeling are introduced. A comparison is made between two semantic role systems in English and one in Chinese, and features of statistic methods are surveyed in a syntactic and semantic view.

Is a closed atom derivable from a definite logic progam? This derivation problem is undecidable. Focused on this problem there exist two categories approaches: the accurate approach that does not guarantee termination, and the terminated abstract approaches. Both approaches have its advantages and disadvantages. We present a novel derivation framework for the definite logic program. A dynamic approach to characterizing termination of fixpoint is presented, then which is used to approximately predict termination of fixpoint in advance. If the fixpoint is predicted termination, we use the non-terminational approach to the derivation problem, otherwise,the terminated abstract approach is used. With this termination predicting approach, we combine the non-termination accurate approaches and the termination abstract approaches together for solving the derivation problem more efficiently. And the experiment results demonstrates the effectiveness of our approach.

Based on the analyses of news stories and the experimental verification,this paper introduces a multi-vector model for story representation.The model represents the feature set as detail as possible.A fuzzy matching method is proposed to compute the relatedness between two named entity sub-vectors in the multi-vector model.To measure the similarity of the stories,all the features together with the named entity relatedness are integrated by Support Vector Machine(SVM).The proposed methods have been tested on TDT4 Chinese corpus for story link detection.The experiment results indicate that story link detection based on multi-vector model can improve the performance,and the relation information generated by fuzzy matching can contribute to the improvement.

随着分子生物学的研究进入以蛋白质组学为标志的后基因组时代,蛋白质相互作用成为蛋白质组学研究的一个重要主题.因为计算方法代价低和周期短的特点,它被广泛地用来分析相互作用数据从而指导生物学家的实验设计.从蛋白质相互作用网络的构建到分析两个方面综述了蛋白质相互作用研究中的各种计算方法:介绍了通过机器学习方法预测、文本挖掘和评估相互作用的各种技术;特别详细地阐述了相互作用网络的重要参数和典型生物模型,并对运用图论方法分析和计算的各种算法进行了深入的剖析;最后,对蛋白质相互作用的计算研究进行了总结和展望.