Open Access. Powered by Scholars. Published by Universities.®

Physical Sciences and Mathematics Commons

Open Access. Powered by Scholars. Published by Universities.®

Articles 1 - 30 of 37

Full-Text Articles in Physical Sciences and Mathematics

Scalable Multi-Core Model Checking Fairness Enhanced Systems, Yang Liu, Jun Sun, Jin Song Dong Dec 2009

Scalable Multi-Core Model Checking Fairness Enhanced Systems, Yang Liu, Jun Sun, Jin Song Dong

Research Collection School Of Computing and Information Systems

Rapid development in hardware industry has brought the prevalence of multi-core systems with shared-memory, which enabled the speedup of various tasks by using parallel algorithms. The Linear Temporal Logic (LTL) model checking problem is one of the difficult problems to be parallelized or scaled up to multi-core. In this work, we propose an on-the-fly parallel model checking algorithm based on the Tarjan’s strongly connected components (SCC) detection algorithm. The approach can be applied to general LTL model checking or with different fairness assumptions. Further, it is orthogonal to state space reduction techniques like partial order reduction. We enhance our PAT …


Coherent Phrase Model For Efficient Image Near-Duplicate Retrieval, Yiqun Hu, Xiangang Cheng, Liang-Tien Chia, Xing Xie, Deepu Rajan, Ah-Hwee Tan Dec 2009

Coherent Phrase Model For Efficient Image Near-Duplicate Retrieval, Yiqun Hu, Xiangang Cheng, Liang-Tien Chia, Xing Xie, Deepu Rajan, Ah-Hwee Tan

Research Collection School Of Computing and Information Systems

This paper presents an efficient and effective solution for retrieving image near-duplicate (IND) from image database. We introduce the coherent phrase model which incorporates the coherency of local regions to reduce the quantization error of the bag-of-words (BoW) model. In this model, local regions are characterized by visual phrase of multiple descriptors instead of visual word of single descriptor. We propose two types of visual phrase to encode the coherency in feature and spatial domain, respectively. The proposed model reduces the number of false matches by using this coherency and generates sparse representations of images. Compared to other method, the …


Static Validation Of C Preprocessor Macros, Andreas Saebjornsen, Lingxiao Jiang, Daniel Quinlan, Zhendong Su Nov 2009

Static Validation Of C Preprocessor Macros, Andreas Saebjornsen, Lingxiao Jiang, Daniel Quinlan, Zhendong Su

Research Collection School Of Computing and Information Systems

The widely used C preprocessor (CPP) is generally considered a source of difficulty for understanding and maintaining C/C++ programs. The main reason for this difficulty is CPP’s purely lexical semantics, i.e., its treatment of both input and output as token streams. This can easily lead to errors that are difficult to diagnose, and it has been estimated that up to 20% of all macros are erroneous. To reduce such errors, more restrictive, replacement languages for CPP have been proposed to limit expanded macros to be valid C syntactic units. However, there is no practical tool that can effectively validate CPP …


Mining Hierarchical Scenario-Based Specifications, David Lo, Shahar Maoz Nov 2009

Mining Hierarchical Scenario-Based Specifications, David Lo, Shahar Maoz

Research Collection School Of Computing and Information Systems

Scalability over long traces, as well as comprehensibility and expressivity of results, are major challenges for dynamic analysis approaches to specification mining. In this work we present a novel use of object hierarchies over traces of inter-object method calls, as an abstraction/refinement mechanism that enables user-guided, top-down or bottom-up mining of layered scenario-based specifications, broken down by hierarchies embedded in the system under investigation. We do this using data mining methods that provide statistically significant sound and complete results modulo user-defined thresholds, in the context of Damm and Harel’s live sequence charts (LSC); a visual, modal, scenario-based, inter-object language. Thus, …


Minimum Latency Broadcasting In Multiradio, Multichannel, Multirate Wireless Meshes, Junaid Qadir, Chuntung Chou, Archan Misra, Joo Ghee Lim Nov 2009

Minimum Latency Broadcasting In Multiradio, Multichannel, Multirate Wireless Meshes, Junaid Qadir, Chuntung Chou, Archan Misra, Joo Ghee Lim

Research Collection School Of Computing and Information Systems

We address the problem of minimizing the worst-case broadcast delay in multi-radio multi-channel multi-rate (MR2-MC) wireless mesh networks (WMN). The problem of 'efficient' broadcast in such networks is especially challenging due to the numerous interrelated decisions that have to be made. The multi-rate transmission capability of WMN nodes, interference between wireless transmissions, and the hardness of optimal channel assignment adds complexity to our considered problem. We present four heuristic algorithms to solve the minimum latency broadcast problem for such settings and show that the 'best' performing algorithms usually adapt themselves to the available radio interfaces and channels. We also study …


Mining Quantified Temporal Rules: Formalism, Algorithms, And Evaluation, David Lo, Ganesan Ramalingam, Venkatesh-Prasad Ranganath, Kapil Vaswani Oct 2009

Mining Quantified Temporal Rules: Formalism, Algorithms, And Evaluation, David Lo, Ganesan Ramalingam, Venkatesh-Prasad Ranganath, Kapil Vaswani

Research Collection School Of Computing and Information Systems

Libraries usually impose constraints on how clients should use them. Often these constraints are not well-documented. In this paper, we address the problem of recovering such constraints automatically, a problem referred to as specification mining. Given some client programs that use a given library, we identify constraints on the library usage that are (almost) satisfied by the given set of clients.The class of rules we target for mining combines simple binary temporal operators with state predicates (involving equality constraints) and quantification. This is a simple yet expressive subclass of temporal properties that allows us to capture many common API usage …


Analysis Of Tradeoffs Between Buffer And Qos Requirements In Wireless Networks, Raphael Rom, Hwee-Pink Tan Oct 2009

Analysis Of Tradeoffs Between Buffer And Qos Requirements In Wireless Networks, Raphael Rom, Hwee-Pink Tan

Research Collection School Of Computing and Information Systems

In this paper, we consider the scheduling problem where data packets from K input-flows need to be delivered to K corresponding wireless receivers over a heterogeneous wireless channel. Our objective is to design a wireless scheduler that achieves good throughput and fairness performance while minimizing the buffer requirement at each wireless receiver. This is a challenging problem due to the unique characteristics of the wireless channel. We propose a novel idea of exploiting both the long-term and short-term error behavior of the wireless channel in the scheduler design. In addition to typical first-order Quality of Service (QoS) metrics such as …


Verifying Stateful Timed Csp Using Implicit Clocks And Zone Abstraction, Jun Sun, Yang Liu, Jin Song Dong, Xian Zhang Sep 2009

Verifying Stateful Timed Csp Using Implicit Clocks And Zone Abstraction, Jun Sun, Yang Liu, Jin Song Dong, Xian Zhang

Research Collection School Of Computing and Information Systems

In this work, we study model checking of compositional real-time systems. A system is modeled using mutable data variables as well as a compositional timed process. Instead of explicitly manipulating clock variables, a number of compositional timed behavioral patterns are used to capture quantitative timing requirements, e.g. delay, timeout, deadline, timed interrupt, etc. A fully automated abstraction technique is developed to build an abstract finite state machine from the model. The idea is to dynamically create/delete clocks, and maintain/solve a constraint on the clocks. The abstract machine weakly bi-simulates the model and, therefore, LTL model checking or trace-refinement checking are …


Admission Control For Differentiated Services In Future Generation Cdma Networks, Hwee-Pink Tan, Rudesindo Núñez-Queija, Adriana F. Gabor, Onno J. Boxma Sep 2009

Admission Control For Differentiated Services In Future Generation Cdma Networks, Hwee-Pink Tan, Rudesindo Núñez-Queija, Adriana F. Gabor, Onno J. Boxma

Research Collection School Of Computing and Information Systems

Future Generation CDMA wireless systems, e.g., 3G, can simultaneously accommodate flow transmissions of users with widely heterogeneous applications. As radio resources are limited, we propose an admission control rule that protects users with stringent transmission bit-rate requirements (“streaming traffic”) while offering sufficient capacity over longer time intervals to delay-tolerant users (“elastic traffic”). While our strategy may not satisfy classical notions of fairness, we aim to reduce congestion and increase overall throughput of elastic users. Using time-scale decomposition, we develop approximations to evaluate the performance of our differentiated admission control strategy to support integrated services with transmission bit-rate requirements in a …


Game Action Based Power Management For Multiplayer Online Game, Bhojan Anand, A. L. Ananda, Mun Choon Chan, Long Thanh Le, Rajesh Krishna Balan Aug 2009

Game Action Based Power Management For Multiplayer Online Game, Bhojan Anand, A. L. Ananda, Mun Choon Chan, Long Thanh Le, Rajesh Krishna Balan

Research Collection School Of Computing and Information Systems

Current mobile devices embrace a wide range of functionalities including high speed network support, hardware accelerated 3D graphics, and multimedia capabilities. These capabilities have boosted the interest for enabling multiplayer online games (MOG) support on such devices. However, the lack of similar growth in battery technology limits the usability of these devices for MOGs. In this paper, we present energy conservation techniques for highly interactive MOGs. These are games, such as first-person shooters, where crisp user interaction is paramount to the overall game experience. Hence, conserving energy while preserving crisp user interaction becomes a critical consideration in this domain. We …


Extracting Paraphrases Of Technical Terms From Noisy Parallel Software Corpus, Xiaoyin Wang, David Lo, Jing Jiang, Lu Zhang, Hong Mei Aug 2009

Extracting Paraphrases Of Technical Terms From Noisy Parallel Software Corpus, Xiaoyin Wang, David Lo, Jing Jiang, Lu Zhang, Hong Mei

Research Collection School Of Computing and Information Systems

In this paper, we study the problem of extracting technical paraphrases from a parallel software corpus, namely, a collection of duplicate bug reports. Paraphrase acquisition is a fundamental task in the emerging area of text mining for software engineering. Existing paraphrase extraction methods are not entirely suitable here due to the noisy nature of bug reports. We propose a number of techniques to address the noisy data problem. The empirical evaluation shows that our method significantly improves an existing method by upto 58%


Data Mining For Software Engineering, Tao Xie, Suresh Thummalapenta, David Lo, Chao Liu Aug 2009

Data Mining For Software Engineering, Tao Xie, Suresh Thummalapenta, David Lo, Chao Liu

Research Collection School Of Computing and Information Systems

To improve software productivity and quality, software engineers are increasingly applying data mining algorithms to various software engineering tasks. However, mining SE data poses several challenges. The authors present various algorithms to effectively mine sequences, graphs, and text from such data.


Formal Verification Of Scalable Nonzero Indicators, Jun Sun, Yang Liu, Jun Sun, Jin Song Dong, Wei Chen, Yanhong A. Liu Jul 2009

Formal Verification Of Scalable Nonzero Indicators, Jun Sun, Yang Liu, Jun Sun, Jin Song Dong, Wei Chen, Yanhong A. Liu

Research Collection School Of Computing and Information Systems

Concurrent algorithms are notoriously difficult to design correctly, and high performance algorithms that make little or no use of locks even more so. In this paper, we describe a formal verification of a recent concurrent data structure Scalable NonZero Indicators. The algorithm supports incrementing, decrementing, and querying the shared counter in an efficient and linearizable way without blocking. The algorithm is highly non-trivial and it is challenging to prove the correctness. We have proved that the algorithm satisfies linearizability, by showing a trace refinement relation from the concrete implementation to its abstract specification. These models are specified in CSP and …


Identifying Bug Signatures Using Discriminative Graph Mining, Hong Cheng, David Lo, Yang Zhou, Xiaoyin Wang, Xifeng Yan Jul 2009

Identifying Bug Signatures Using Discriminative Graph Mining, Hong Cheng, David Lo, Yang Zhou, Xiaoyin Wang, Xifeng Yan

Research Collection School Of Computing and Information Systems

Bug localization has attracted a lot of attention recently. Most existing methods focus on pinpointing a single statement or function call which is very likely to contain bugs. Although such methods could be very accurate, it is usually very hard for developers to understand the context of the bug, given each bug location in isolation. In this study, we propose to model software executions with graphs at two levels of granularity: methods and basic blocks. An individual node represents a method or basic block and an edge represents a method call, method return or transition (at the method or basic …


Towards Expressive Specification And Efficient Model Checking, Jin Song Dong, Jun Sun Jul 2009

Towards Expressive Specification And Efficient Model Checking, Jin Song Dong, Jun Sun

Research Collection School Of Computing and Information Systems

System modeling is important and highly non-trivial. The choice of specification language is an important factor in the success of the entire development. The language should cover several facets of the requirements and the model should precisely capture (up to abstraction of irrelevant details) an existing system or a system to be built. The language should have a semantic model suitable to study the behaviors of the system and to establish the validity of desired properties. A formal model can be the basis for a variety of system development activities, e.g., system simulation, visualization, verification or prototype synthesis.


Verification Of Population Ring Protocols In Pat, Yang Liu, Jun Pang, Jun Sun, Jianhua Zhao Jul 2009

Verification Of Population Ring Protocols In Pat, Yang Liu, Jun Pang, Jun Sun, Jianhua Zhao

Research Collection School Of Computing and Information Systems

The population protocol model has emerged as an elegant paradigm for describing mobile ad hoc networks, consisting of a number of nodes that interact with each other to carry out a computation. One essential property of self-stabilizing population protocols is that all nodes must eventually converge to the correct output value, with respect to all possible initial configurations. It has been shown that fairness constraints play a crucial role in designing population protocols. The Process Analysis Toolkit (PAT) has been developed to perform verifications under different fairness constraints efficiently. In particular, it can handle global fairness, which is required for …


Automatic Steering Of Behavioral Model Inference, David Lo, Leonardo Mariani, Mauro Pezze Jul 2009

Automatic Steering Of Behavioral Model Inference, David Lo, Leonardo Mariani, Mauro Pezze

Research Collection School Of Computing and Information Systems

Many testing and analysis techniques use finite state models to validate and verify the quality of software systems. Since the specification of such models is complex and time-consuming, researchers defined several techniques to extract finite state models from code and traces. Automatically generating models requires much less effort than designing them, and thus eases the verification and validation of large software systems. However, when models are inferred automatically, the precision of the mining process is critical. Behavioral models mined with imprecise processes can include many spurious behaviors, and can thus compromise the results of testing and analysis techniques that use …


Poster Abstract: Beamcast: Harnessing Beamforming Capabilities For Link Layer Multicast, Souvik Sen, Rahul Ghosh, Jie Xiong, Romit Roy Choudhury Jul 2009

Poster Abstract: Beamcast: Harnessing Beamforming Capabilities For Link Layer Multicast, Souvik Sen, Rahul Ghosh, Jie Xiong, Romit Roy Choudhury

Research Collection School Of Computing and Information Systems

Wireless multicast is an important service primitive for emerging applications such as live video, streaming audio and content telecasts. Transmission rate in such a link layer multicast is bottlenecked by the rate of the weakest client, leading to channel under-utilization. Attempts to increase the data rate results in lower reliability (due to higher bit error rate) and higher unfairness. This poster utilizes smart beamforming antennas to improve multicast performance in wireless LANs. The main idea is to satisfy majority of the (strong) clients with a high-rate omnidirectional transmission, followed by high-rate directional transmission(s) to cover the weaker ones. By selecting …


Integrating Specification And Programs For System Modeling And Verification, Jun Sun, Yang Liu, Jin Song Dong, Chunqing Chen Jul 2009

Integrating Specification And Programs For System Modeling And Verification, Jun Sun, Yang Liu, Jin Song Dong, Chunqing Chen

Research Collection School Of Computing and Information Systems

High level specification languages like CSP use mathematical objects as abstractions to represent systems and processes. System behaviors are described as process expressions combined with compositional operators, which are associated with elegant algebraic laws for system analysis. Nonetheless, modeling systems with non-trivial data and functional aspects using CSP remains difficult. In this work, we propose a modeling language named CSP# (short for communicating sequential programs) which integrates high-level modeling operators with low-level procedural codes, for the purpose of efficient mechanical system verification. We demonstrate that data operations can be modeled as terminating sequential programs, which can be composed using high-level …


Fair Model Checking With Process Counter Abstraction, Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu, Jin Song Dong Jun 2009

Fair Model Checking With Process Counter Abstraction, Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu, Jin Song Dong

Research Collection School Of Computing and Information Systems

Parameterized systems are characterized by the presence of a large (or even unbounded) number of behaviorally similar processes, and they often appear in distributed/concurrent systems. A common state space abstraction for checking parameterized systems involves not keeping track of process identifiers by grouping behaviorally similar processes. Such an abstraction, while useful, conflicts with the notion of fairness. Because process identifiers are lost in the abstraction, it is difficult to ensure fairness (in terms of progress in executions) among the processes. In this work, we study the problem of fair model checking with process counter abstraction. Even without maintaining the process …


Model Checking Linearizability Via Refinement, Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun Jun 2009

Model Checking Linearizability Via Refinement, Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun

Research Collection School Of Computing and Information Systems

Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that 1) all executions of concurrent operations be serializable, and 2) the serialized executions be correct with respect to the sequential semantics. This paper describes a new method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. Our method avoids the often difficult task of determining linearization points in implementations, but can also take advantage of linearization points if they are given. The method exploits model checking of finite state systems specified as concurrent …


Adaptive In-Network Processing For Bandwidth And Energy Constrained Mission-Oriented Multi-Hop Wireless Networks, Sharanya Eswaran, Matthew Johnson, Archan Misra, Thomas La Porta Jun 2009

Adaptive In-Network Processing For Bandwidth And Energy Constrained Mission-Oriented Multi-Hop Wireless Networks, Sharanya Eswaran, Matthew Johnson, Archan Misra, Thomas La Porta

Research Collection School Of Computing and Information Systems

In-network processing, involving operations such as filtering, compression and fusion, is widely used in sensor networks to reduce the communication overhead. In many tactical and stream-oriented wireless network applications, both link bandwidth and node energy are critically constrained resources and in-network processing itself imposes non-negligible computing cost. In this work, we have developed a unified and distributed closed-loop control framework that computes both a) the optimal level of sensor stream compression performed by a forwarding node, and b) the best set of nodes where the stream processing operators should be deployed. Our framework extends the Network Utility Maximization (NUM) paradigm, …


Non-Redundant Sequential Rules - Theory And Algorithm, David Lo, Siau-Cheng Khoo, Limsoon Wong Jun 2009

Non-Redundant Sequential Rules - Theory And Algorithm, David Lo, Siau-Cheng Khoo, Limsoon Wong

Research Collection School Of Computing and Information Systems

A sequential rule expresses a relationship between two series of events happening one after another. Sequential rules are potentially useful for analyzing data in sequential format, ranging from purchase histories, network logs and program execution traces. In this work, we investigate and propose a syntactic characterization of a non-redundant set of sequential rules built upon past work on compact set of representative patterns. A rule is redundant if it can be inferred from another rule having the same support and confidence. When using the set of mined rules as a composite filter, replacing a full set of rules with a …


Mferio: The Design And Evaluation Of A Peer-To-Peer Mobile Payment System, Rajesh Krishna Balan, Narayanasamy Ramasubbu, Komsit Prakobphol, Nicolas Christin, Jason Hong Jun 2009

Mferio: The Design And Evaluation Of A Peer-To-Peer Mobile Payment System, Rajesh Krishna Balan, Narayanasamy Ramasubbu, Komsit Prakobphol, Nicolas Christin, Jason Hong

Research Collection School Of Computing and Information Systems

In this paper, we present the design and evaluation of a near-field communication-based mobile p2p payment application, called mFe-rio, that is designed to replace cash-based transactions. We first identify design criteria that payment systems should satisfy and then explain how mFerio, relative to those criteria, improves on the limitations of cash-based systems. We next describe mFerio's implementation and user interface design, focusing on the balance between usability and security. Finally, we present the results of a two-phase user study, involving a total of 104 people, that shows that mFerio has low cognitive load and is also fast, accurate, and easy …


A Formal Framework For Modeling And Validating Simulink Diagrams, Chunqing Chen, Jin Song Dong, Jun Sun May 2009

A Formal Framework For Modeling And Validating Simulink Diagrams, Chunqing Chen, Jin Song Dong, Jun Sun

Research Collection School Of Computing and Information Systems

Simulink has been widely used in industry to model and simulate embedded systems. With the increasing usage of embedded systems in real-time safety-critical situations, Simulink becomes deficient to analyze (timing) requirements with high-level assurance. In this article, we apply Timed Interval Calculus (TIC), a realtime specification language, to complement Simulink with TIC formal verification capability. We elaborately construct TIC library functions to model Simulink library blocks which are used to compose Simulink diagrams. Next, Simulink diagrams are automatically transformed into TIC models which preserve functional and timing aspects. Important requirements such as timing bounded liveness can be precisely specified in …


The Impact Of Process Choice In High Maturity Environments: An Empirical Analysis, Narayanasamy Ramasubbu, Rajesh Krishna Balan May 2009

The Impact Of Process Choice In High Maturity Environments: An Empirical Analysis, Narayanasamy Ramasubbu, Rajesh Krishna Balan

Research Collection School Of Computing and Information Systems

We present the results of a three year field study of the software development process choices made by project teams at two leading offshore vendors. In particular, we focus on the performance implications of project teams that chose to augment structured, plan-driven processes to implement the CMM level-5 Key Process Areas (KPAs) with agile methods. Our analysis of 112 software projects reveals that the decision to augment the firm-recommended, plan-driven approach with improvised, agile methods was significantly affected by the extent of client knowledge and involvement, newness of technology, and the project size. Furthermore this decision had a significant and …


Classification Of Software Behaviors For Failure Detection: A Discriminative Pattern Mining Approach, David Lo, Hong Cheng, Jiawei Han, Siau-Cheng Khoo, Chengnian Sun May 2009

Classification Of Software Behaviors For Failure Detection: A Discriminative Pattern Mining Approach, David Lo, Hong Cheng, Jiawei Han, Siau-Cheng Khoo, Chengnian Sun

Research Collection School Of Computing and Information Systems

Software is a ubiquitous component of our daily life. We often depend on the correct working of software systems. Due to the difficulty and complexity of software systems, bugs and anomalies are prevalent. Bugs have caused billions of dollars loss, in addition to privacy and security threats. In this work, we address software reliability issues by proposing a novel method to classify software behaviors based on past history or runs. With the technique, it is possible to generalize past known errors and mistakes to capture failures and anomalies. Our technique first mines a set of discriminative features capturing repetitive series …


Automatic Mining Of Functionally Equivalent Code Fragments Via Random Testing, Lingxiao Jiang, Zhendong Su May 2009

Automatic Mining Of Functionally Equivalent Code Fragments Via Random Testing, Lingxiao Jiang, Zhendong Su

Research Collection School Of Computing and Information Systems

Similar code may exist in large software projects due to some common software engineering practices, such as copying and pasting code and n-version programming. Although previous work has studied syntactic equivalence and small-scale, coarse-grained program-level and function-level semantic equivalence, it is not known whether significant fine-grained, code-level semantic duplications exist. Detecting such semantic equivalence is also desirable because it can enable many applications such as code understanding, maintenance, and optimization. In this paper, we introduce the first algorithm to automatically mine functionally equivalent code fragments of arbitrary size - down to an executable statement. Our notion of functional equivalence is …


The Digital Wallet: Opportunities And Prototypes, Rajesh Krishna Balan, Narayanasamy Ramasubbu Apr 2009

The Digital Wallet: Opportunities And Prototypes, Rajesh Krishna Balan, Narayanasamy Ramasubbu

Research Collection School Of Computing and Information Systems

Example digital wallet applications support secure P2P mobile cash transactions and alleviate point-of-sale confusion for consumers using multiple payment, discount, and loyalty cards.


Efficient Mining Of Closed Repetitive Gapped Subsequences From A Sequence Database, Bolin Ding, David Lo, Jiawei Han, Siau-Cheng Khoo Apr 2009

Efficient Mining Of Closed Repetitive Gapped Subsequences From A Sequence Database, Bolin Ding, David Lo, Jiawei Han, Siau-Cheng Khoo

Research Collection School Of Computing and Information Systems

There is a huge wealth of sequence data available, for example, customer purchase histories, program execution traces, DNA, and protein sequences. Analyzing this wealth of data to mine important knowledge is certainly a worthwhile goal. In this paper, as a step forward to analyzing patterns in sequences, we introduce the problem of mining closed repetitive gapped subsequences and propose efficient solutions. Given a database of sequences where each sequence is an ordered list of events, the pattern we would like to mine is called repetitive gapped subsequence, which is a subsequence (possibly with gaps between two successive events within it) …