Formal specifications of software systems need to evolve in many ways during system development. Not only are changes required to refine the specification toward an implementation, they are also required in response to changes in requirements, or to incorporate different aspects of the system, e.g., fault tolerance or timing, initially ignored in order to simplify reasoning. This paper presents an approach for evolving Z specifications by the step-wise application of a number of simple rules. These rules not only document the evolution of the specification, but also make precise how properties of the system evolve with the specification. Hence, reasoning about these properties performed on the original specification need not be repeated on the new specification.
Model checking multi-agent systems (MAS) always suffers from the state explosion problem. In this paper we focus on an abstraction technique which is one of the major methods for overcoming this problem. For a multi-agent system, we present a novel abstraction procedure which reduces the state space by collapsing the global states in the system. The abstraction is automatically computed according to the property to be verified. The resulting abstract system simulates the concrete system, while the universal temporal epistemic properties are preserved. Our abstraction is an over-approximation. If some universal temporal epistemic property is not satisfied, then we need to identify spurious counterexamples. We further show how to reduce complex counterexamples to simple structures, i.e., paths and loops, such that the counterexamples can be checked and the abstraction can be refined efficiently. Finally, we illustrate the abstraction technique with a card game.
With the development of Internet and Web service technology, Web service composition has been an effective way to construct software applications; service selection is the crucial element in the composition process. However, the existing selection methods mostly generate static plans since they neglect the inherent stochastic and dynamic nature of Web services. As a result, Web service composition often inevitably terminates with failure. An indeterminacy-aware service selection algorithm based on an improved Markov decision process (IMDP) has been designed for reliable service composition, but it suffers from higher computation complexity. Therefore, an efficient method is proposed, which can reduce the computation cost by converting the service selection problem based on IMDP into solving a nonhomogeneous linear equation set. Experimental results demonstrate the success rate of service composition has been improved greatly, whilst also reducing computation cost.
Trajectory clustering and behavior pattern extraction are the foundations of research into activity perception of objects in motion. In this paper, a new framework is proposed to extract behavior patterns through trajectory analysis. Firstly, we introduce directional trimmed mean distance (DTMD), a novel method used to measure similarity between trajectories. DTMD has the attributes of anti-noise, self-adaptation and the capability to determine the direction for each trajectory. Secondly, we use a hierarchical clustering algorithm to cluster trajectories. We design a length-weighted linkage rule to enhance the accuracy of trajectory clustering and reduce problems associated with incomplete trajectories. Thirdly, the motion model parameters are estimated for each trajectory’s classification, and behavior patterns for trajectories are extracted. Finally, the difference between normal and abnormal behaviors can be distinguished.
As an effective image segmentation method, the standard fuzzy c-means (FCM) clustering algorithm is very sensitive to noise in images. Several modified FCM algorithms, using local spatial information, can overcome this problem to some degree. However, when the noise level in the image is high, these algorithms still cannot obtain satisfactory segmentation performance. In this paper, we introduce a non local spatial constraint term into the objective function of FCM and propose a fuzzy c-means clustering algorithm with non local spatial information (FCM_NLS). FCM_NLS can deal more effectively with the image noise and preserve geometrical edges in the image. Performance evaluation experiments on synthetic and real images, especially magnetic resonance (MR) images, show that FCM_NLS is more robust than both the standard FCM and the modified FCM algorithms using local spatial information for noisy image segmentation.
Computing moments on images is very important in the fields of image processing and pattern recognition. The non-symmetry and anti-packing model (NAM) is a general pattern representation model that has been developed to help design some efficient image representation methods. In this paper, inspired by the idea of computing moments based on the S-Tree coding (STC) representation and by using the NAM and extended shading (NAMES) approach, we propose a fast algorithm for computing lower order moments based on the NAMES representation, which takes
The random forests (RF) algorithm, which combines the predictions from an ensemble of random trees, has achieved significant improvements in terms of classification accuracy. In many real-world applications, however, ranking is often required in order to make optimal decisions. Thus, we focus our attention on the ranking performance of RF in this paper. Our experimental results based on the entire 36 UC Irvine Machine Learning Repository (UCI) data sets published on the main website of Weka platform show that RF doesn’t perform well in ranking, and is even about the same as a single C4.4 tree. This fact raises the question of whether several improvements to RF can scale up its ranking performance. To answer this question, we single out an improved random forests (IRF) algorithm. Instead of the information gain measure and the maximum-likelihood estimate, the average gain measure and the similarity-weighted estimate are used in IRF. Our experiments show that IRF significantly outperforms all the other algorithms used to compare in terms of ranking while maintains the high classification accuracy characterizing RF.
There has been considerable interest in designing algorithms for detecting community structure in real-world complex networks. A majority of these algorithms assume that communities are disjoint, placing each vertex in only one cluster. However, in nature, it is a matter of common experience that communities often overlap and members often play multiple roles in a network topology. To further investigate these properties of overlapping communities and heterogeneity within the network topology, a new method is proposed to divide networks into separate communities by spreading outward from each local important element and extracting its neighbors within the same group in each spreading operation. When compared with the state of the art, our new algorithm can not only classify different types of nodes at a more fine-grained scale successfully but also detect community structure more effectively. We also evaluate our algorithm using the standard data sets. Our results show that it performed well not only in the efficiency of algorithm, but also with a higher accuracy of partition results.
Most existing semi-supervised clustering algorithms are not designed for handling high-dimensional data. On the other hand, semi-supervised dimensionality reduction methods may not necessarily improve the clustering performance, due to the fact that the inherent relationship between subspace selection and clustering is ignored. In order to mitigate the above problems, we present a semi-supervised clustering algorithm using adaptive distance metric learning (SCADM) which performs semi-supervised clustering and distance metric learning simultaneously. SCADM applies the clustering results to learn a distance metric and then projects the data onto a low-dimensional space where the separability of the data is maximized. Experimental results on real-world data sets show that the proposed method can effectively deal with high-dimensional data and provides an appealing clustering performance.
Recognizing attack intention is crucial for security analysis. In recent years, a number of methods for attack intention recognition have been proposed. However, most of these techniques mainly focus on the alerts of an intrusion detection system and use algorithms of low efficiency that mine frequent attack patterns without reconstructing attack paths. In this paper, a novel and effective method is proposed, which integrates several techniques to identify attack intentions. Using this method, a Bayesian-based attack scenario is constructed, where frequent attack patterns are identified using an efficient data-mining algorithm based on frequent patterns. Subsequently, attack paths are rebuilt by re-correlating frequent attack patterns mined in the scenario. The experimental results demonstrate the capability of our method in rebuilding attack paths, recognizing attack intentions as well as in saving system resources. Specifically, to the best of our knowledge, the proposed method is the first to correlate complementary intrusion evidence with frequent pattern mining techniques based on the FP-Growth algorithm to rebuild attack paths and to recognize attack intentions.
An analytical model is proposed for input buffer router architecture Network-on-Chip (NoC) with finite size buffers. The model is developed based on M/G/1/K queuing theory and takes into consideration the restriction of buffer sizes in NoC. It analyzes the packet’s sojourn time in each buffer and calculates the packets average latency in NoC The validity of the model is verified through simulation. By comparing our analytical outcomes to the simulation results, we show that the proposed model successfully captures the performance characteristics of NoC, which provides an efficient performance analysis tool for NoC design.