An Efficient Scalable Runtime System for Macro Data Flow Processing Using S-Net

S-Net is a declarative coordination language and component technology aimed at radically facilitating software engineering for modern parallel compute systems by near-complete separation of concerns between application (component) engineering and concurrency orchestration. S-Net builds on the concept of stream processing to structure networks of communicating asynchronous components implemented in a conventional (sequential) language. In this paper we present the design, implementation and evaluation of a new and innovative runtime system for S-Net streaming networks. The Front runtime system outperforms the existing implementations of S-Net by orders of magnitude for stress-test benchmarks, significantly reduces runtimes of fully-fledged parallel applications with compute-intensive components and achieves good scalability on our 48-core test system.     

QUBLE: towards blending interactive visual subgraph search queries on large networks

In a previous paper, we laid out the vision of a novel graph query processing paradigm where instead of processing a visual query graph after its construction, it interleaves visual query formulation and processing by exploiting the latency offered by the gui to filter irrelevant matches and prefetch partial query results [8]. Our recent attempts at implementing this vision [8, 9] show significant improvement in system response time (srt) for subgraph queries. However, these efforts are designed specifically for graph databases containing a large collection of small or medium-sized graphs. In this paper, we propose a novel algorithm called quble (QUery Blender for Large nEtworks) to realize this visual subgraph querying paradigm on very large networks (e.g., protein interaction networks, social networks). First, it decomposes a large network into a set of graphlets and supergraphlets using a minimum cut-based graph partitioning technique. Next, it mines approximate frequent and small infrequent fragments (sifs) from them and identifies their occurrences in these graphlets and supergraphlets. Then, the indexing framework of [9] is enhanced so that the mined fragments can be exploited to index graphlets for efficient blending of visual subgraph query formulation and query processing. Extensive experiments on large networks demonstrate effectiveness of quble.     

gbase: an efficient analysis platform for large graphs

Graphs appear in numerous applications including cyber security, the Internet, social networks, protein networks, recommendation systems, citation networks, and many more. Graphs with millions or even billions of nodes and edges are common-place. How to store such large graphs efficiently? What are the core operations/queries on those graph? How to answer the graph queries quickly? We propose Gbase, an efficient analysis platform for large graphs. The key novelties lie in (1) our storage and compression scheme for a parallel, distributed settings and (2) the carefully chosen graph operations and their efficient implementations. We designed and implemented an instance of Gbase using Mapreduce/Hadoop. Gbase provides a parallel indexing mechanism for graph operations that both saves storage space, as well as accelerates query responses. We run numerous experiments on real and synthetic graphs, spanning billions of nodes and edges, and we show that our proposed Gbase is indeed fast, scalable, and nimble, with significant savings in space and time.     

Exploiting a hypergraph model for finding Golomb rulers

Golomb rulers are special rulers where for any two marks it holds that the distance between them is unique. They find applications in radio frequency selection, radio astronomy, data encryption, communication networks, and bioinformatics. An important subproblem in constructing “compact” Golomb rulers is Golomb Subruler  (GSR), which asks whether it is possible to make a given ruler Golomb by removing at most \(k\) marks. We initiate a study of GSR from a parameterized complexity perspective. In particular, we consider a natural hypergraph characterization of rulers and investigate the construction and structure of the corresponding hypergraphs. We exploit their properties to derive polynomial-time data reduction rules that reduce a given instance of GSR to an equivalent one with \({{\mathrm{O}}}(k^3)\)  marks. Finally, we complement a recent computational complexity study of GSR by providing a simplified reduction that shows NP-hardness even when all integers are bounded by a polynomial in the input length.     

An approach to the DIN Kernel Lisp definition

A DIN Kernel LISP Draft (DKLisp) has been developed by DIN as Reaction to Action D1 (N79), short term goal, of ISO WG16. It defines a subset language, as compatible as possible with the ANSICommon-Lisp draft, but also with theEuLisp draft. It combines the most important LISP main stream features in a single, compact, but nevertheless complete language definition, which thereby could be well suited as basis for a short term InternationalLisp Standard. Besides the functional and knowledge processing features, the expressive power of the language is well comparable with contemporary procedural languages, as e.g. C++ (of course without libraries). Important features ofDKLisp are:

to be a “Lisp-1,” but allowing an easy “Lisp-2” transformation;

to be a simple, powerful and standardized educationalLisp;

to omit all features, which are unclean or in heavy discussion;

DKLisp programs run nearly unchanged inCommon-Lisp;

DKLisp contains a simple object and package system;

DKLisp contains those data classes and control structures also common to most modernLisp and non-Lisp languages;

DKLisp offers a simple stream I/O;

DKLisp contains a clean unified hierarchical class/type system;

DKLisp contains the typical “Lisp-features” in an orthogonal way;

DKLisp allows and encourages really small but powerful implementations;

DKLisp comes in levels, so allowing ANSICommon-Lisp to be an extension ofDKLisp level-1.

The present is the second version of the proposal, namely version 1.2, with slight differences with respect to the one sent to ISO. Sources of such changes were the remarks generously sent by many readers of the previous attempt.     

The clock constraint specification language for building timed causality models

The uml Profile for Modeling and Analysis of Real-Time and Embedded (RTE) systems has recently been adopted by the OMG. Its Time Model extends the informal and simplistic Simple Time package proposed by Unified Modeling Language (UML2) and offers a broad range of capabilities required to model RTE systems including discrete/dense and chronometric/logical time. The Marte specification introduces a Time Structure inspired from several time models of the concurrency theory and proposes a new clock constraint specification language (ccsl) to specify, within the context of the uml, logical and chronometric time constraints. A semantic model in ccsl is attached to a (uml) model to give its timed causality semantics. In that sense, ccsl is comparable to the Ptolemy environment, in which directors give the semantics to models according to predefined models of computation and communication. This paper focuses on one historical model of computation of Ptolemy [Synchronous Data Flow (SDF)] and shows how to build SDF graphs by combining uml models and ccsl.     

Proving operational termination of membership equational programs

Reasoning about the termination of equational programs in sophisticated equational languages such as Elan, Maude, OBJ, CafeOBJ, Haskell, and so on, requires support for advanced features such as evaluation strategies, rewriting modulo, use of extra variables in conditions, partiality, and expressive type systems (possibly including polymorphism and higher-order). However, many of those features are, at best, only partially supported by current term rewriting termination tools (for instance mu-term, C i ME, AProVE, TTT, Termptation, etc.) while they may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive membership equational programs and such termination tools, and prove the correctness of such transformations. We also discuss a prototype tool performing the transformations on Maude equational programs and sending the resulting transformed theories to some of the aforementioned standard termination tools.     

Para Miner: a generic pattern mining algorithm for multi-core architectures

In this paper, we present Para Miner which is a generic and parallel algorithm for closed pattern mining. Para Miner is built on the principles of pattern enumeration in strongly accessible set systems. Its efficiency is due to a novel dataset reduction technique (that we call EL-reduction), combined with novel technique for performing dataset reduction in a parallel execution on a multi-core architecture. We illustrate Para Miner’s genericity by using this algorithm to solve three different pattern mining problems: the frequent itemset mining problem, the mining frequent connected relational graphs problem and the mining gradual itemsets problem. In this paper, we prove the soundness and the completeness of Para Miner. Furthermore, our experiments show that despite being a generic algorithm, Para Miner can compete with specialized state of the art algorithms designed for the pattern mining problems mentioned above. Besides, for the particular problem of gradual itemset mining, Para Miner outperforms the state of the art algorithm by two orders of magnitude.     

ANDES: efficient evaluation of NOT-twig queries in relational databases

Despite a large body of work on XPath query processing in relational environment, systematic study of queries containing not-predicates have received little attention in the literature. Particularly, several xml supports of industrial-strength commercial rdbms fail to efficiently evaluate such queries. In this paper, we present an efficient and novel strategy to evaluate not -twig queries in a tree-unaware relational environment. not -twig queries are XPath queries with ancestor–descendant and parent–child axis and contain one or more not-predicates. We propose a novel Dewey-based encoding scheme called Andes (ANcestor Dewey-based Encoding Scheme), which enables us to efficiently filter out elements satisfying a not-predicate by comparing their ancestor group identifiers. In this approach, a set of elements under the same common ancestor at a specific level in the xml tree is assigned same ancestor group identifier. Based on this scheme, we propose a novel sql translation algorithm for not-twig query evaluation. Experiments carried out confirm that our proposed approach built on top of an off-the-shelf commercial rdbms significantly outperforms state-of-the-art relational and native approaches. We also explore the query plans selected by a commercial relational optimizer to evaluate our translated queries in different input cardinality. Such exploration further validates the performance benefits of Andes.     

Markov Chain Analysis of Self-organizing Mobile Nodes

Self-organization of autonomous mobile nodes using bio-inspired algorithms in mobile ad hoc networks (manets) has been presented in earlier work of the authors. In this paper, the convergence speed of our force-based genetic algorithm (called fga) is provided through analysis using homogeneous Markov chains. The fga is run by each mobile node as a topology control mechanism to decide a corresponding node??s next speed and movement direction so that it guides an autonomous mobile node over an unknown geographical area to obtain a uniform node distribution while only using local information. The stochastic behavior of fga, like all ga-based approaches, makes it difficult to analyze the effects that various manet characteristics have on its convergence speed. Metrically transitive homogeneous Markov chains have been used to analyze the convergence of our fga with respect to various communication ranges of mobile nodes and also the number of nodes in various scenarios. The Dobrushin contraction coefficient of ergodicity is used for measuring convergence speed for Markov chain model of our fga. Two different testbed platforms are presented to illustrate effectiveness of our bio-inspired algorithm in terms of area coverage.     

Parameterized Domination in Circle Graphs

A circle graph is the intersection graph of a set of chords in a circle. Keil [Discrete Appl. Math., 42(1):51–63, 1993] proved that Dominating Set, Connected Dominating Set, and Total Dominating Set are NP-complete in circle graphs. To the best of our knowledge, nothing was known about the parameterized complexity of these problems in circle graphs. In this paper we prove the following results, which contribute in this direction:

• Dominating Set, Independent Dominating Set, Connected Dominating Set, Total Dominating Set, and Acyclic Dominating Set are W[1]-hard in circle graphs, parameterized by the size of the solution.
• Whereas both Connected Dominating Set and Acyclic Dominating Set are W[1]-hard in circle graphs, it turns out that Connected Acyclic Dominating Set is polynomial-time solvable in circle graphs.
• If T is a given tree, deciding whether a circle graph G has a dominating set inducing a graph isomorphic to T is NP-complete when T is in the input, and FPT when parameterized by t=|V(T)|. We prove that the FPT algorithm runs in subexponential time, namely $2^{\mathcal{O}(t \cdot\frac{\log\log t}{\log t})} \cdot n^{\mathcal{O}(1)}$ , where n=|V(G)|.

     

Scalability and robustness of parallel hyperheuristics applied to a multiobjectivised frequency assignment problem

The Frequency Assignment Problem (fap) is one of the key issues in the design of Global System for Mobile Communications (gsm) networks. The formulation of the fap used here focuses on aspects that are relevant to real gsm networks. In this paper, we adapt a parallel model to tackle a multiobjectivised version of the fap. It is a hybrid model which combines an island-based model and a hyperheuristic. The main aim of this paper is to design a strategy that facilitates the application of the current best-behaved algorithm. Specifically, our goal is to decrease the user effort required to set its parameters. At the same time, the usage of such an algorithm in parallel environments was enabled. As a result, the time required to attain high-quality solutions was decreased. We also conduct a robustness analysis of this parallel model. In this analysis we study the relationship between the migration stage of the parallel model and the quality of the resulting solutions. In addition, we also carry out a scalability study of the parallel model. In this case, we analyse the impact that the migration stage has on the scalability of the entire parallel model. Computational results with several real network instances have validated our proposed approach. The best-known frequency plans for two real-world network instances are improved with this strategy.     

Verification and validation meet planning and scheduling

A planning and scheduling (P&S) system takes as input a domain model and a goal, and produces a plan of actions to be executed, which will achieve the goal. A P&S system typically also offers plan execution and monitoring engines. Due to the non-deterministic nature of planning problems, it is a challenge to construct correct and reliable P&S systems, including, for example, declarative domain models. Verification and validation (V&V) techniques have been applied to address these issues. Furthermore, V&V systems have been applied to actually perform planning, and conversely, P&S systems have been applied to perform V&V of more traditional software. This article overviews some of the literature on the fruitful interaction between V&V and P&S.     

Evolutionary Algorithms for Quantum Computers

In this article, we formulate and study quantum analogues of randomized search heuristics, which make use of Grover search (in Proceedings of the 28th Annual ACM Symposium on Theory of Computing, pp. 212–219. ACM, New York, 1996) to accelerate the search for improved offsprings. We then specialize the above formulation to two specific search heuristics: Random Local Search and the (1+1) Evolutionary Algorithm. We call the resulting quantum versions of these search heuristics Quantum Local Search and the (1+1) Quantum Evolutionary Algorithm. We conduct a rigorous runtime analysis of these quantum search heuristics in the computation model of quantum algorithms, which, besides classical computation steps, also permits those unique to quantum computing devices. To this end, we study the six elementary pseudo-Boolean optimization problems OneMax, LeadingOnes, Discrepancy, Needle, Jump, and TinyTrap. It turns out that the advantage of the respective quantum search heuristic over its classical counterpart varies with the problem structure and ranges from no speedup at all for the problem Discrepancy to exponential speedup for the problem TinyTrap. We show that these runtime behaviors are closely linked to the probabilities of performing successful mutations in the classical algorithms.     

Thoughtful brute-force attack of the RERS 2012 and 2013 Challenges

The Rigorous Examination of Reactive Systems’ (rers) Challenges provide a forum for experimental evaluation based on specifically synthesized benchmark suites. In this paper, we report on our ‘brute-force attack’ of the rers 2012 and 2013 Challenges. We connected the rers problems to two state-of-the-art explicit state model checkers: LTSmin and Spin. Apart from an effective compression of the state vector, we did not analyze the source code of the problems. Our brute-force approach was successful: it won both editions of the rers Challenge.     

The Meteor metric for automatic evaluation of machine translation

The Meteor Automatic Metric for Machine Translation evaluation, originally developed and released in 2004, was designed with the explicit goal of producing sentence-level scores which correlate well with human judgments of translation quality. Several key design decisions were incorporated into Meteor in support of this goal. In contrast with IBM’s Bleu, which uses only precision-based features, Meteor uses and emphasizes recall in addition to precision, a property that has been confirmed by several metrics as being critical for high correlation with human judgments. Meteor also addresses the problem of reference translation variability by utilizing flexible word matching, allowing for morphological variants and synonyms to be taken into account as legitimate correspondences. Furthermore, the feature ingredients within Meteor are parameterized, allowing for the tuning of the metric’s free parameters in search of values that result in optimal correlation with human judgments. Optimal parameters can be separately tuned for different types of human judgments and for different languages. We discuss the initial design of the Meteor metric, subsequent improvements, and performance in several independent evaluations in recent years.     

The Mizar Mathematical Library in OMDoc: Translation and Applications

The Mizar Mathematical Library is one of the largest libraries of formalized and mechanically verified mathematics. Its language is highly optimized for authoring by humans. As in natural languages, the meaning of an expression is influenced by its (mathematical) context in a way that is natural to humans, but harder to specify for machine manipulation. Thus its custom file format can make the access to the library difficult. Indeed, the Mizar system itself is currently the only system that can fully operate on the Mizar library. This paper presents a translation of the Mizar library into the OMDoc format (Open Mathematical Documents), an XML-based representation format for mathematical knowledge. OMDoc is geared towards machine support and interoperability by making formula structure and context dependencies explicit. Thus, the Mizar library becomes accessible for a wide range of OMDoc-based tools for formal mathematics and knowledge management. We exemplify interoperability by indexing the translated library in the MathWebSearch engine, which provides an “applicable theorem search” service (almost) out of the box.