Context-bounded verification of thread pools

Thread pooling is a common programming idiom in which a fixed set of worker threads are maintained to execute tasks concurrently. The workers repeatedly pick tasks and execute them to completion. Each task is sequential, with possibly recursive code, and tasks communicate over shared memory. Executing a task can lead to more new tasks being spawned. We consider the safety verification problem for thread-pooled programs. We parameterize the problem with two parameters: the size of the thread pool as well as the number of context switches for each task. The size of the thread pool determines the number of workers running concurrently. The number of context switches determines how many times a worker can be swapped out while executing a single task---like many verification problems for multithreaded recursive programs, the context bounding is important for decidability. We show that the safety verification problem for thread-pooled, context-bounded, Boolean programs is EXPSPACE-complete, even if the size of the thread pool and the context bound are given in binary. Our main result, the EXPSPACE upper bound, is derived using a sequence of new succinct encoding techniques of independent language-theoretic interest. In particular, we show a polynomial-time construction of downward closures of languages accepted by succinct pushdown automata as doubly succinct nondeterministic finite automata. While there are explicit doubly exponential lower bounds on the size of nondeterministic finite automata accepting the downward closure, our result shows these automata can be compressed. We show that thread pooling significantly reduces computational power: in contrast, if only the context bound is provided in binary, but there is no thread pooling, the safety verification problem becomes 3EXPSPACE-complete. Given the high complexity lower bounds of related problems involving binary parameters, the relatively low complexity of safety verification with thread-pooling comes as a surprise.

High Influencing Pattern Discovery over Time Series Data

A spatial co-location pattern denotes a subset of spatial features whose instances frequently appear nearby. High influence co-location pattern mining is used to find co-location patterns with high influence in specific aspects. Studies of such pattern mining usually rely on spatial distance for measuring nearness between instances, a method that cannot be applied to an influence propagation process concluded from epidemic dispersal scenarios. To discover meaningful patterns by using fruitful results in this field, we extend existing approaches and propose a mining framework. We first defined a new concept of proximity to depict semantic nearness between instances of distinct features, thus applying a star-shaped materialized model to mine influencing patterns. Then, we designed attribute descriptors to perceive attributes of instances and edges from time series data, and we calculated the attribute weights via an analytic hierarchy process, thereby computing the influence between instances and the influence of features in influencing patterns. Next, we constructed influencing metrics and set a threshold to discover high influencing patterns. Since the metrics do not satisfy the downward closure property, we propose two improved algorithms to boost efficiency. Extensive experiments conducted on real and synthetic datasets verified the effectiveness, efficiency, and scalability of our method.

A Synopsis Based Approach for Itemset Frequency Estimation over Massive Multi-Transaction Stream

The streams where multiple transactions are associated with the same key are prevalent in practice, e.g., a customer has multiple shopping records arriving at different time. Itemset frequency estimation on such streams is very challenging since sampling based methods, such as the popularly used reservoir sampling, cannot be used. In this article, we propose a novel k -Minimum Value (KMV) synopsis based method to estimate the frequency of itemsets over multi-transaction streams. First, we extract the KMV synopses for each item from the stream. Then, we propose a novel estimator to estimate the frequency of an itemset over the KMV synopses. Comparing to the existing estimator, our method is not only more accurate and efficient to calculate but also follows the downward-closure property. These properties enable the incorporation of our new estimator with existing frequent itemset mining (FIM) algorithm (e.g., FP-Growth) to mine frequent itemsets over multi-transaction streams. To demonstrate this, we implement a KMV synopsis based FIM algorithm by integrating our estimator into existing FIM algorithms, and we prove it is capable of guaranteeing the accuracy of FIM with a bounded size of KMV synopsis. Experimental results on massive streams show our estimator can significantly improve on the accuracy for both estimating itemset frequency and FIM compared to the existing estimators.

Forward analysis for WSTS, part I: completions

We define representations for downward-closed subsets of a rich family of well-quasi-orders, and more generally for closed subsets of an even richer family of Noetherian topological spaces. This includes the cases of finite words, of multisets, of finite trees, notably. Those representations are given as finite unions of ideals, or more generally of irreducible closed subsets. All the representations we explore are computable, in the sense that we exhibit algorithms that decide inclusion, and compute finite unions and finite intersections. The origin of this work lies in the need for computing finite representations of sets of successors of the downward closure of one state, or more generally of a downward-closed set of states, in a well-structured transition system, and this is where we start: we define adequate notions of completions of well-quasi-orders, and more generally, of Noetherian spaces. For verification purposes, we argue that the required completions must be ideal completions, or more generally sobrifications, that is, spaces of irreducible closed subsets.

An Algorithm for Mining High Utility Sequential Patterns with Time Interval

Mining High Utility Sequential Patterns (HUSP) is an emerging topic in data mining which attracts many researchers. The HUSP mining algorithms can extract sequential patterns having high utility (importance) in a quantitative sequence database. In real world applications, the time intervals between elements are also very important. However, recent HUSP mining algorithms cannot extract sequential patterns with time intervals between elements. Thus, in this paper, we propose an algorithm for mining high utility sequential patterns with the time interval problem. We consider not only sequential patterns’ utilities, but also their time intervals. The sequence weight utility value is used to ensure the important downward closure property. Besides that, we use four time constraints for dealing with time interval in the sequence to extract more meaningful patterns. Experimental results show that our proposed method is efficient and effective in mining high utility sequential pattern with time intervals.

A Weighted Frequent Item-Set Mining using WD-FIM Algorithm

Smart systems are the one of the most significant inventions of our times. These systems rely on powerful information mining techniques to achieve intelligence in decision making. Frequent item set mining (FIM), has become one of the most significant research area of data mining. The information present in databases is in-general ambiguous and uncertain. In such databases, one should think of weighted FIM to discover item sets which are significant from end user’s perspective. Be that as it may, with introduction of weight-factor for FIM makes the weighted continuous item sets may not fulfil the descending conclusion property anymore. Subsequently, the pursuit space of successive item set can't be limited by descending conclusion property which prompts a poor time effectiveness. In this paper, we introduce two properties for FIM, first one is, weight judgment downward closure property (WD-FIM), it is for weighted FIM and the second one is existence property for its subsets. In view of above two properties, the WD-FIM calculation is proposed to limit the looking through space of the weighted regular item sets and improve the time effectiveness. In addition, the culmination and time productivity of WD-FIM calculation are examined hypothetically. At last, the exhibition of the proposed WD-FIM calculation is confirmed on both engineered and genuine data sets

A Systematic Survey on High Utility Itemset Mining

High utility itemset mining considers unit profits and quantities of items in a transaction database to extract more applicable and more useful association rules. Downward closure property, which causes significant pruning in frequent itemset mining, is not established in the utility of itemsets and so the mining problem will require alternative solutions to reduce its search space and to enhance its efficiency. Using an anti-monotonic upper bound of the utility function and exploiting efficient data structures for storing and compacting the dataset to perform efficient pruning strategies are the main solutions to address high utility itemset mining problem. Different mining methods and techniques have attempted to improve performance of extracting high utility itemsets and their several variants, including high-average utility itemsets, top-k high utility itemsets, and high utility itemsets with negative values, using more efficient data structures, more appropriate anti-monotonic upper bounds, and stronger pruning strategies. This paper aims to represent a comprehensive systematic review for high utility itemset mining techniques and to classify them based on their problem-solving approaches.

An Intelligent Decision in Smart Systems Using A Weighted Frequent Itemset Mining Algorithm

Intelligent decision is the key technology of smart systems. Data mining technology has been playing an increasingly important role in decision making activities. The introduction of weight makes the weighted frequent itemsets not satisfy the downward closure property any longer. As a result, the search space of frequent itemsets cannot be narrowed according to downward closure property which leads to a poor time efficiency. In this paper, the weight judgment downward closure property for weighted frequent itemsets and the existence property of weighted frequent subsets are introduced and proved first. The Fuzzy-based WARM satisfies the downward closure property and prunes the insignificant rules by assigning the weight to the itemset. This reduces the computation time and execution time. This paper presents an Enhanced Fuzzy-based Weighted AssociationRuleMining(E-FWARM) algorithm for efficient mining of the frequent itemsets. The pre-filtering method is applied to the input dataset to remove the item having low variance. Data discretization is performed and E-FWARM is applied for mining the frequent itemsets. The experimental results show that the proposed E-FWARM algorithm yields maximum frequent items, association rules, accuracy and minimum execution time than the existing algorithms.

Regular pattern mining on multidimensional databases

Extracting general patterns from a multidimensional database is a tricky task. Designing an algorithm to seek the frequency or no. of occurring patterns and really first-class transaction dimension of a mining pattern, general patterns from a multidimensional database is the objective of the task. Analysis prior to mining required patterns from database hence, Apriori algorithm is used. After the acquiring patterns, they have been improved to many further patterns. Nevertheless, to mine the required patterns from a multidimensional database we use FP development algorithm. Here, now we have carried out a pop-growth procedure to mine fashionable patterns from multidimensional database established on their repute values. Utilizing this opportunity, we studied about recognizing patterns which give the reputation of every object or movements inside the entire database. Whereas Apriori and FP-growth algorithm is determined by the aid or frequency measure of an object set. As a result, to acquire required patterns utilizing these programs one has to mine FP-growth tree recursively which involves extra time consumption. We have utilized a mining process, which is meant for multidimensional recognized patterns. It overcomes the limitations of present mining ways by implementing lazy pruning method followed by showing downward closure property.