OpenRaiser/Intern-Atlas huggingface dataset:
A Domain-Specific Language for Incremental and Modular Design of Large-Scale Verifiably-Safe Flow Networks (Preliminary Report)
Venue: arXiv cs.PL 2011
Year: 2011

We define a domain-specific language (DSL) to inductively assemble flow networks from small networks or modules to produce arbitrarily large ones, with interchangeable functionally-equivalent parts. Our small networks or modules are "small" only as the building blocks in this inductive definition (there is no limit on their size). Associated with our DSL is a type theory, a system of formal annotations to express desirable properties of flow networks together with rules that enforce them as invariants across their interfaces, i.e, the rules guarantee the properties are preserved as we build larger networks from smaller ones. A prerequisite for a type theory is a formal semantics, i.e, a rigorous definition of the entities that qualify as feasible flows through the networks, possibly restricted to satisfy additional efficiency or safety requirements. This can be carried out in one of two ways, as a denotational semantics or as an operational (or reduction) semantics; we choose the first in preference to the second, partly to avoid exponential-growth rewriting in the operational approach. We set up a typing system and prove its soundness for our DSL.
Maximum Segment Sum, Monadically (distilled tutorial, with solutions)
Venue: arXiv cs.DS 2011
Year: 2011

The maximum segment sum problem is to compute, given a list of integers, the largest of the sums of the contiguous segments of that list. This problem specification maps directly onto a cubic-time algorithm; however, there is a very elegant linear-time solution too. The problem is a classic exercise in the mathematics of program construction, illustrating important principles such as calculational development, pointfree reasoning, algebraic structure, and datatype-genericity. Here, we take a sideways look at the datatype-generic version of the problem in terms of monadic functional programming, instead of the traditional relational approach; the presentation is tutorial in style, and leavened with exercises for the reader.
Specific "scientific" data structures, and their processing
Venue: arXiv cs.DS 2011
Year: 2011

Programming physicists use, as all programmers, arrays, lists, tuples, records, etc., and this requires some change in their thought patterns while converting their formulae into some code, since the "data structures" operated upon, while elaborating some theory and its consequences, are rather: power series and Padé approximants, differential forms and other instances of differential algebras, functionals (for the variational calculus), trajectories (solutions of differential equations), Young diagrams and Feynman graphs, etc. Such data is often used in a [semi-]numerical setting, not necessarily "symbolic", appropriate for the computer algebra packages. Modules adapted to such data may be "just libraries", but often they become specific, embedded sub-languages, typically mapped into object-oriented frameworks, with overloaded mathematical operations. Here we present a functional approach to this philosophy. We show how the usage of Haskell datatypes and - fundamental for our tutorial - the application of lazy evaluation makes it possible to operate upon such data (in particular: the "infinite" sequences) in a natural and comfortable manner.
Implementing Explicit and Finding Implicit Sharing in Embedded DSLs
Venue: arXiv cs.PL 2011
Year: 2011

Aliasing, or sharing, is prominent in many domains, denoting that two differently-named objects are in fact identical: a change in one object (memory cell, circuit terminal, disk block) is instantly reflected in the other. Languages for modelling such domains should let the programmer explicitly define the sharing among objects or expressions. A DSL compiler may find other identical expressions and share them, implicitly. Such common subexpression elimination is crucial to the efficient implementation of DSLs. Sharing is tricky in embedded DSL, since host aliasing may correspond to copying of the underlying objects rather than their sharing. This tutorial summarizes discussions of implementing sharing in Haskell DSLs for automotive embedded systems and hardware description languages. The technique has since been used in a Haskell SAT solver and the DSL for music synthesis. We demonstrate the embedding in pure Haskell of a simple DSL with a language form for explicit sharing. The DSL also has implicit sharing, implemented via hash-consing. Explicit sharing greatly speeds up hash-consing. The seemingly imperative nature of hash-consing is hidden beneath a simple combinator language. The overall implementation remains pure functional and easy to reason about.
Resumption-based big-step and small-step interpreters for While with interactive I/O
Venue: arXiv cs.PL 2011
Year: 2011

In this tutorial, we program big-step and small-step total interpreters for the While language extended with input and output primitives. While is a simple imperative language consisting of skip, assignment, sequence, conditional and loop. We first develop trace-based interpreters for While. Traces are potentially infinite nonempty sequences of states. The interpreters assign traces to While programs: for us, traces are denotations of While programs. The trace is finite if the program is terminating and infinite if the program is non-terminating. However, we cannot decide (i.e., write a program to determine), for any given program, whether its trace is finite or infinite, which amounts to deciding the halting problem. We then extend While with interactive input/output primitives. Accordingly, we extend the interpreters by generalizing traces to resumptions. The tutorial is based on our previous work with T. Uustalu on reasoning about interactive programs in the setting of constructive type theory.
Nonlinear Channel Estimation for OFDM System by Complex LS-SVM under High Mobility Conditions
Venue: arXiv cs.LG 2011
Year: 2011

A nonlinear channel estimator using complex Least Square Support Vector Machines (LS-SVM) is proposed for pilot-aided OFDM system and applied to Long Term Evolution (LTE) downlink under high mobility conditions. The estimation algorithm makes use of the reference signals to estimate the total frequency response of the highly selective multipath channel in the presence of non-Gaussian impulse noise interfering with pilot signals. Thus, the algorithm maps trained data into a high dimensional feature space and uses the structural risk minimization (SRM) principle to carry out the regression estimation for the frequency response function of the highly selective channel. The simulations show the effectiveness of the proposed method which has good performance and high precision to track the variations of the fading channels compared to the conventional LS method and it is robust at high speed mobility.
An Empirical Study on variants of TCP over AODV routing protocol in MANET
Venue: arXiv cs.NI 2011
Year: 2011

The cardinal concept of TCP development was to carry data within the network where network congestion plays a vital role to cause packet loss. On the other hand, there are several other reasons to lose packets in Mobile Ad Hoc Networks due to fading, interfaces, multi-path routing, malicious node, and black hole. Along with throughput, fairness of TCP protocols is important to establish a good communication. In this paper, an empirical study has been done by simulation and analysis of TCP variations under AODV routing protocol. In our simulation, we studied multiple variations of TCP, such as Reno, New-Reno, Vegas, and Tahoe. The simulation work has been done in NS2 environment. Based on the analysis simulation result of we carried out our observations with respect to the behavior of AODV routing protocol for different TCP packets under several QoS metrics such as drop, throughput, delay, and jitter.
Tech Report A Variational HEM Algorithm for Clustering Hidden Markov Models
Venue: arXiv cs.AI 2011
Year: 2011

The hidden Markov model (HMM) is a generative model that treats sequential data under the assumption that each observation is conditioned on the state of a discrete hidden variable that evolves in time as a Markov chain. In this paper, we derive a novel algorithm to cluster HMMs through their probability distributions. We propose a hierarchical EM algorithm that i) clusters a given collection of HMMs into groups of HMMs that are similar, in terms of the distributions they represent, and ii) characterizes each group by a "cluster center", i.e., a novel HMM that is representative for the group. We present several empirical studies that illustrate the benefits of the proposed algorithm.
An approximately truthful-in-expectation mechanism for combinatorial auctions using value queries
Venue: arXiv cs.GT 2011
Year: 2011

This manuscript presents an alternative implementation of the truthful-in-expectation mechanism of Dughmi, Roughgarden and Yan for combinatorial auctions with weighted-matroid-rank-sum valuations. The new implementation uses only value queries and is approximately truthful-in-expectation, in the sense that by reporting truthfully each agent maximizes his utility within a multiplicative 1-o(1) factor. It still provides an optimal (1-1/e-o(1))-approximation in social welfare. We achieve this by first presenting an approximately maximal-in-distributional-range allocation rule and then showing a black-box transformation to an approximately truthful-in-expectation mechanism.
Limitations of randomized mechanisms for combinatorial auctions
Venue: arXiv cs.GT 2011
Year: 2011

Recently, a randomized mechanism has been discovered [Dughmi, Roughgarden and Yan; STOC'11] for combinatorial auctions that is truthful in expectation and guarantees a (1-1/e)-approximation to the optimal social welfare when players have coverage valuations. This approximation ratio is the best possible even for non-truthful algorithms, assuming $P \neq NP$. Given the recent sequence of negative results for combinatorial auctions under more restrictive notions of incentive compatibility, this development raises a natural question: Are truthful-in-expectation mechanisms compatible with polynomial-time approximation in a way that deterministic or universally truthful mechanisms are not? In particular, can polynomial-time truthful-in-expectation mechanisms guarantee a near-optimal approximation ratio for more general variants of combinatorial auctions? We prove that this is not the case. Specifically, the result of Dughmi, Roughgarden and Yan cannot be extended to combinatorial auctions with submodular valuations in the value oracle model. (Absent strategic considerations, a (1-1/e)-approximation is still achievable in this setting.) More precisely, we prove that there is a constant γ>0 such that there is no randomized mechanism that is truthful-in-expectation--- or even approximately truthful-in-expectation --- and guarantees an m^{-γ}-approximation to the optimal social welfare for combinatorial auctions with submodular valuations in the value oracle model. We also prove an analogous result for the flexible combinatorial public projects (CPP) problem. Both our results present an unexpected separation between coverage functions and submodular functions, which does not occur for these problems without strategic considerations.
Toward Designing Intelligent PDEs for Computer Vision: An Optimal Control Approach
Venue: arXiv cs.CV 2011
Year: 2011

Many computer vision and image processing problems can be posed as solving partial differential equations (PDEs). However, designing PDE system usually requires high mathematical skills and good insight into the problems. In this paper, we consider designing PDEs for various problems arising in computer vision and image processing in a lazy manner: \emph{learning PDEs from real data via data-based optimal control}. We first propose a general intelligent PDE system which holds the basic translational and rotational invariance rule for most vision problems. By introducing a PDE-constrained optimal control framework, it is possible to use the training data resulting from multiple ways (ground truth, results from other methods, and manual results from humans) to learn PDEs for different computer vision tasks. The proposed optimal control based training framework aims at learning a PDE-based regressor to approximate the unknown (and usually nonlinear) mapping of different vision tasks. The experimental results show that the learnt PDEs can solve different vision problems reasonably well. In particular, we can obtain PDEs not only for problems that traditional PDEs work well but also for problems that PDE-based methods have never been tried before, due to the difficulty in describing those problems in a mathematical way.
Data Mining Techniques: A Source for Consumer Behavior Analysis
Venue: arXiv cs.DB 2011
Year: 2011

Various studies on consumer purchasing behaviors have been presented and used in real problems. Data mining techniques are expected to be a more effective tool for analyzing consumer behaviors. However, the data mining method has disadvantages as well as advantages. Therefore, it is important to select appropriate techniques to mine databases. The objective of this paper is to know consumer behavior, his psychological condition at the time of purchase and how suitable data mining method apply to improve conventional method. Moreover, in an experiment, association rule is employed to mine rules for trusted customers using sales data in a super market industry
Interference Mitigation in Large Random Wireless Networks
Venue: arXiv cs.IT 2011
Year: 2011

A central problem in the operation of large wireless networks is how to deal with interference -- the unwanted signals being sent by transmitters that a receiver is not interested in. This thesis looks at ways of combating such interference. In Chapters 1 and 2, we outline the necessary information and communication theory background, including the concept of capacity. We also include an overview of a new set of schemes for dealing with interference known as interference alignment, paying special attention to a channel-state-based strategy called ergodic interference alignment. In Chapter 3, we consider the operation of large regular and random networks by treating interference as background noise. We consider the local performance of a single node, and the global performance of a very large network. In Chapter 4, we use ergodic interference alignment to derive the asymptotic sum-capacity of large random dense networks. These networks are derived from a physical model of node placement where signal strength decays over the distance between transmitters and receivers. (See also arXiv:1002.0235 and arXiv:0907.5165.) In Chapter 5, we look at methods of reducing the long time delays incurred by ergodic interference alignment. We analyse the tradeoff between reducing delay and lowering the communication rate. (See also arXiv:1004.0208.) In Chapter 6, we outline a problem that is equivalent to the problem of pooled group testing for defective items. We then present some new work that uses information theoretic techniques to attack group testing. We introduce for the first time the concept of the group testing channel, which allows for modelling of a wide range of statistical error models for testing. We derive new results on the number of tests required to accurately detect defective items, including when using sequential `adaptive' tests.
Measuring Intelligence through Games
Venue: arXiv cs.AI 2011
Year: 2011

Artificial general intelligence (AGI) refers to research aimed at tackling the full problem of artificial intelligence, that is, create truly intelligent agents. This sets it apart from most AI research which aims at solving relatively narrow domains, such as character recognition, motion planning, or increasing player satisfaction in games. But how do we know when an agent is truly intelligent? A common point of reference in the AGI community is Legg and Hutter's formal definition of universal intelligence, which has the appeal of simplicity and generality but is unfortunately incomputable. Games of various kinds are commonly used as benchmarks for "narrow" AI research, as they are considered to have many important properties. We argue that many of these properties carry over to the testing of general intelligence as well. We then sketch how such testing could practically be carried out. The central part of this sketch is an extension of universal intelligence to deal with finite time, and the use of sampling of the space of games expressed in a suitably biased game description language.
Lifted Unit Propagation for Effective Grounding
Venue: arXiv cs.LO 2011
Year: 2011

A grounding of a formula $ϕ$ over a given finite domain is a ground formula which is equivalent to $ϕ$ on that domain. Very effective propositional solvers have made grounding-based methods for problem solving increasingly important, however for realistic problem domains and instances, the size of groundings is often problematic. A key technique in ground (e.g., SAT) solvers is unit propagation, which often significantly reduces ground formula size even before search begins. We define a "lifted" version of unit propagation which may be carried out prior to grounding, and describe integration of the resulting technique into grounding algorithms. We describe an implementation of the method in a bottom-up grounder, and an experimental study of its performance.
A Study of the PDGF Signaling Pathway with PRISM
Venue: arXiv cs.CE 2011
Year: 2011

In this paper, we apply the probabilistic model checker PRISM to the analysis of a biological system -- the Platelet-Derived Growth Factor (PDGF) signaling pathway, demonstrating in detail how this pathway can be analyzed in PRISM. We show that quantitative verification can yield a better understanding of the PDGF signaling pathway.
Estimating the overlap between dependent computations for automatic parallelization
Venue: arXiv cs.PL 2011
Year: 2011

Researchers working on the automatic parallelization of programs have long known that too much parallelism can be even worse for performance than too little, because spawning a task to be run on another CPU incurs overheads. Autoparallelizing compilers have therefore long tried to use granularity analysis to ensure that they only spawn off computations whose cost will probably exceed the spawn-off cost by a comfortable margin. However, this is not enough to yield good results, because data dependencies may \emph{also} limit the usefulness of running computations in parallel. If one computation blocks almost immediately and can resume only after another has completed its work, then the cost of parallelization again exceeds the benefit. We present a set of algorithms for recognizing places in a program where it is worthwhile to execute two or more computations in parallel that pay attention to the second of these issues as well as the first. Our system uses profiling information to compute the times at which a procedure call consumes the values of its input arguments and the times at which it produces the values of its output arguments. Given two calls that may be executed in parallel, our system uses the times of production and consumption of the variables they share to determine how much their executions would overlap if they were run in parallel, and therefore whether executing them in parallel is a good idea or not. We have implemented this technique for Mercury in the form of a tool that uses profiling data to generate recommendations about what to parallelize, for the Mercury compiler to apply on the next compilation of the program. We present preliminary results that show that this technique can yield useful parallelization speedups, while requiring nothing more from the programmer than representative input data for the profiling run.
A Study of Computer-Based Simulations for Nano-Systems and their types
Venue: arXiv cs.ET 2011
Year: 2011

In most of the cases, the experimental study of Nanotechnology involves high cost for Laboratory set-up and the experimentation processes were also slow. So, one cannot rely on experimental nanotechnology alone. As such, the Computer-Based molecular simulations and modeling are one of the foundations of computational nanotechnology. The computer based modeling and simulations were also referred as computational experimentations. In real experiments, the investigator doesn't have full control over the experiment. But, in Computational experimentation the investigator have full control over the experiment. The accuracy of such Computational nano-technology based experiment generally depends on the accuracy of the following things: Intermolecular interaction, Numerical models and Simulation schemes used. Once the accuracy of the Computational Scheme is guaranteed one can use that to investigate various nonlinear interactions whose results are completely unexpected and unforeseen. Apart from it, numerical modeling and computer based simulations also help to understand the theoretical part of the nano-science involved in the nano-system. They allow us to develop useful analytic and predictive models. In this paper, a brief study of Computer-Based- Simulation techniques as well as some Experimental result obtained using it were given.
Net-Centric World: Lifestyle of the 21st Century
Venue: arXiv cs.CY 2011
Year: 2011

In this paper, we research the potential of information communication technologies (ICTs) for changing our society from a commute-centric to a network-centric environment. We propose to formalize the key attributes of ICT-based telecommuting experiences from both economic and human interactivity perspective. We introduce the notion of network-eligible transactions and disclose the link between degree of network centricity and worker settlement radius, postulating that media-rich network services have a strong potential to increase the physical distance between work and home locations. We also highlight notable technology challenges and opportunities of migration from location-based to mobile living, signifying the needs for new services and standards development.
Integrating Learning from Examples into the Search for Diagnostic Policies
Venue: arXiv cs.AI 2011
Year: 2011

This paper studies the problem of learning diagnostic policies from training examples. A diagnostic policy is a complete description of the decision-making actions of a diagnostician (i.e., tests followed by a diagnostic decision) for all possible combinations of test results. An optimal diagnostic policy is one that minimizes the expected total cost, which is the sum of measurement costs and misdiagnosis costs. In most diagnostic settings, there is a tradeoff between these two kinds of costs. This paper formalizes diagnostic decision making as a Markov Decision Process (MDP). The paper introduces a new family of systematic search algorithms based on the AO* algorithm to solve this MDP. To make AO* efficient, the paper describes an admissible heuristic that enables AO* to prune large parts of the search space. The paper also introduces several greedy algorithms including some improvements over previously-published methods. The paper then addresses the question of learning diagnostic policies from examples. When the probabilities of diseases and test results are computed from training data, there is a great danger of overfitting. To reduce overfitting, regularizers are integrated into the search algorithms. Finally, the paper compares the proposed methods on five benchmark diagnostic data sets. The studies show that in most cases the systematic search methods produce better diagnostic policies than the greedy methods. In addition, the studies show that for training sets of realistic size, the systematic search algorithms are practical on todays desktop computers.