OpenRaiser/Intern-Atlas huggingface dataset:
Development of a Cargo Screening Process Simulator: A First Approach
Venue: arXiv cs.AI 2010
Year: 2010

The efficiency of current cargo screening processes at sea and air ports is largely unknown as few benchmarks exists against which they could be measured. Some manufacturers provide benchmarks for individual sensors but we found no benchmarks that take a holistic view of the overall screening procedures and no benchmarks that take operator variability into account. Just adding up resources and manpower used is not an effective way for assessing systems where human decision-making and operator compliance to rules play a vital role. Our aim is to develop a decision support tool (cargo-screening system simulator) that will map the right technology and manpower to the right commodity-threat combination in order to maximise detection rates. In this paper we present our ideas for developing such a system and highlight the research challenges we have identified. Then we introduce our first case study and report on the progress we have made so far.
Wireless Network Coding with Imperfect Overhearing
Venue: arXiv cs.IT 2010
Year: 2010

Not only is network coding essential to achieve the capacity of a single-session multicast network, it can also help to improve the throughput of wireless networks with multiple unicast sessions when overheard information is available. Most previous research aimed at realizing such improvement by using perfectly overheard information, while in practice, especially for wireless networks, overheard information is often imperfect. To date, it is unclear whether network coding should still be used in such situations with imperfect overhearing. In this paper, a simple but ubiquitous wireless network model with two unicast sessions is used to investigate this problem. From the diversity and multiplexing tradeoff perspective, it is proved that even when overheard information is imperfect, network coding can still help to improve the overall system performance. This result implies that network coding should be used actively regardless of the reception quality of overheard information.
Evaluation of Query Generators for Entity Search Engines
Venue: arXiv cs.DB 2010
Year: 2010

Dynamic web applications such as mashups need efficient access to web data that is only accessible via entity search engines (e.g. product or publication search engines). However, most current mashup systems and applications only support simple keyword searches for retrieving data from search engines. We propose the use of more powerful search strategies building on so-called query generators. For a given set of entities query generators are able to automatically determine a set of search queries to retrieve these entities from an entity search engine. We demonstrate the usefulness of query generators for on-demand web data integration and evaluate the effectiveness and efficiency of query generators for a challenging real-world integration scenario.
An Implementation of Nested Pattern Matching in Interaction Nets
Venue: arXiv cs.LO 2010
Year: 2010

Reduction rules in interaction nets are constrained to pattern match exactly one argument at a time. Consequently, a programmer has to introduce auxiliary rules to perform more sophisticated matches. In this paper, we describe the design and implementation of a system for interaction nets which allows nested pattern matching on interaction rules. We achieve a system that provides convenient ways to express interaction net programs without defining auxiliary rules.
A Type System for Tom
Venue: arXiv cs.LO 2010
Year: 2010

Extending a given language with new dedicated features is a general and quite used approach to make the programming language more adapted to problems. Being closer to the application, this leads to less programming flaws and easier maintenance. But of course one would still like to perform program analysis on these kinds of extended languages, in particular type checking and inference. In this case one has to make the typing of the extended features compatible with the ones in the starting language. The Tom programming language is a typical example of such a situation as it consists of an extension of Java that adds pattern matching, more particularly associative pattern matching, and reduction strategies. This paper presents a type system with subtyping for Tom, that is compatible with Java's type system, and that performs both type checking and type inference. We propose an algorithm that checks if all patterns of a Tom program are well-typed. In addition, we propose an algorithm based on equality and subtyping constraints that infers types of variables occurring in a pattern. Both algorithms are exemplified and the proposed type system is showed to be sound and complete.
Automating Fine Concurrency Control in Object-Oriented Databases
Venue: arXiv cs.DB 2010
Year: 2010

Several propositions were done to provide adapted concurrency control to object-oriented databases. However, most of these proposals miss the fact that considering solely read and write access modes on instances may lead to less parallelism than in relational databases! This paper cope with that issue, and advantages are numerous: (1) commutativity of methods is determined a priori and automatically by the compiler, without measurable overhead, (2) run-time checking of commutativity is as efficient as for compatibility, (3) inverse operations need not be specified for recovery, (4) this scheme does not preclude more sophisticated approaches, and, last but not least, (5) relational and object-oriented concurrency control schemes with read and write access modes are subsumed under this proposition.
Approximate Dynamic Programming using Halfspace Queries and Multiscale Monge decomposition
Venue: arXiv cs.DS 2010
Year: 2010

Let $P=(P_1, P_2, \ldots, P_n)$, $P_i \in \field{R}$ for all $i$, be a signal and let $C$ be a constant. In this work our goal is to find a function $F:[n]\rightarrow \field{R}$ which optimizes the following objective function: $$ \min_{F} \sum_{i=1}^n (P_i-F_i)^2 + C\times |\{i:F_i \neq F_{i+1} \} | $$ The above optimization problem reduces to solving the following recurrence, which can be done efficiently using dynamic programming in $O(n^2)$ time: $$ OPT_i = \min_{0 \leq j \leq i-1} [ OPT_j + \sum_{k=j+1}^i (P_k - (\sum_{m=j+1}^i P_m)/(i-j) )^2 ]+ C $$ The above recurrence arises naturally in applications where we wish to approximate the original signal $P$ with another signal $F$ which consists ideally of few piecewise constant segments. Such applications include database (e.g., histogram construction), speech recognition, biology (e.g., denoising aCGH data) applications and many more. In this work we present two new techniques for optimizing dynamic programming that can handle cost functions not treated by other standard methods. The basis of our first algorithm is the definition of a constant-shifted variant of the objective function that can be efficiently approximated using state of the art methods for range searching. Our technique approximates the optimal value of our objective function within additive $ε$ error and runs in $\tilde{O}(n^{1.5} \log{(\frac{U}ε))}$ time, where $U = \max_i f_i$. The second algorithm we provide solves a similar recurrence within a factor of $ε$ and runs in $O(n \log^2n / ε)$. The new technique introduced by our algorithm is the decomposition of the initial problem into a small (logarithmic) number of Monge optimization subproblems which we can speed up using existing techniques.
An efficient algorithm for the parallel solution of high-dimensional differential equations
Venue: arXiv cs.DC 2010
Year: 2010

The study of high-dimensional differential equations is challenging and difficult due to the analytical and computational intractability. Here, we improve the speed of waveform relaxation (WR), a method to simulate high-dimensional differential-algebraic equations. This new method termed adaptive waveform relaxation (AWR) is tested on a communication network example. Further we propose different heuristics for computing graph partitions tailored to adaptive waveform relaxation. We find that AWR coupled with appropriate graph partitioning methods provides a speedup by a factor between 3 and 16.
Cross-Layer Designs in Coded Wireless Fading Networks with Multicast
Venue: arXiv cs.NI 2010
Year: 2010

A cross-layer design along with an optimal resource allocation framework is formulated for wireless fading networks, where the nodes are allowed to perform network coding. The aim is to jointly optimize end-to-end transport layer rates, network code design variables, broadcast link flows, link capacities, average power consumption, and short-term power allocation policies. As in the routing paradigm where nodes simply forward packets, the cross-layer optimization problem with network coding is non-convex in general. It is proved however, that with network coding, dual decomposition for multicast is optimal so long as the fading at each wireless link is a continuous random variable. This lends itself to provably convergent subgradient algorithms, which not only admit a layered-architecture interpretation but also optimally integrate network coding in the protocol stack. The dual algorithm is also paired with a scheme that yields near-optimal network design variables, namely multicast end-to-end rates, network code design quantities, flows over the broadcast links, link capacities, and average power consumption. Finally, an asynchronous subgradient method is developed, whereby the dual updates at the physical layer can be affordably performed with a certain delay with respect to the resource allocation tasks in upper layers. This attractive feature is motivated by the complexity of the physical layer subproblem, and is an adaptation of the subgradient method suitable for network control.
The Video Genome
Venue: arXiv cs.CV 2010
Year: 2010

Fast evolution of Internet technologies has led to an explosive growth of video data available in the public domain and created unprecedented challenges in the analysis, organization, management, and control of such content. The problems encountered in video analysis such as identifying a video in a large database (e.g. detecting pirated content in YouTube), putting together video fragments, finding similarities and common ancestry between different versions of a video, have analogous counterpart problems in genetic research and analysis of DNA and protein sequences. In this paper, we exploit the analogy between genetic sequences and videos and propose an approach to video analysis motivated by genomic research. Representing video information as video DNA sequences and applying bioinformatic algorithms allows to search, match, and compare videos in large-scale databases. We show an application for content-based metadata mapping between versions of annotated video.
What's in a Session: Tracking Individual Behavior on the Web
Venue: arXiv cs.HC 2010
Year: 2010

We examine the properties of all HTTP requests generated by a thousand undergraduates over a span of two months. Preserving user identity in the data set allows us to discover novel properties of Web traffic that directly affect models of hypertext navigation. We find that the popularity of Web sites -- the number of users who contribute to their traffic -- lacks any intrinsic mean and may be unbounded. Further, many aspects of the browsing behavior of individual users can be approximated by log-normal distributions even though their aggregate behavior is scale-free. Finally, we show that users' click streams cannot be cleanly segmented into sessions using timeouts, affecting any attempt to model hypertext navigation using statistics of individual sessions. We propose a strictly logical definition of sessions based on browsing activity as revealed by referrer URLs; a user may have several active sessions in their click stream at any one time. We demonstrate that applying a timeout to these logical sessions affects their statistics to a lesser extent than a purely timeout-based mechanism.
Automatic analysis of distance bounding protocols
Venue: arXiv cs.CR 2010
Year: 2010

Distance bounding protocols are used by nodes in wireless networks to calculate upper bounds on their distances to other nodes. However, dishonest nodes in the network can turn the calculations both illegitimate and inaccurate when they participate in protocol executions. It is important to analyze protocols for the possibility of such violations. Past efforts to analyze distance bounding protocols have only been manual. However, automated approaches are important since they are quite likely to find flaws that manual approaches cannot, as witnessed in literature for analysis pertaining to key establishment protocols. In this paper, we use the constraint solver tool to automatically analyze distance bounding protocols. We first formulate a new trace property called Secure Distance Bounding (SDB) that protocol executions must satisfy. We then classify the scenarios in which these protocols can operate considering the (dis)honesty of nodes and location of the attacker in the network. Finally, we extend the constraint solver so that it can be used to test protocols for violations of SDB in these scenarios and illustrate our technique on some published protocols.
How to prevent type-flaw attacks on security protocols under algebraic properties
Venue: arXiv cs.CR 2010
Year: 2010

Type-flaw attacks upon security protocols wherein agents are led to misinterpret message types have been reported frequently in the literature. Preventing them is crucial for protocol security and verification. Heather et al. proved that tagging every message field with it's type prevents all type-flaw attacks under a free message algebra and perfect encryption system. In this paper, we prove that type-flaw attacks can be prevented with the same technique even under the ACUN algebraic properties of XOR which is commonly used in "real-world" protocols such as SSL 3.0. Our proof method is general and can be easily extended to other monoidal operators that possess properties such as Inverse and Idempotence as well. We also discuss how tagging could be used to prevent type-flaw attacks under other properties such as associativity of pairing, commutative encryption, prefix property and homomorphic encryption.
Spatial logics with connectedness predicates
Venue: arXiv cs.LO 2010
Year: 2010

We consider quantifier-free spatial logics, designed for qualitative spatial representation and reasoning in AI, and extend them with the means to represent topological connectedness of regions and restrict the number of their connected components. We investigate the computational complexity of these logics and show that the connectedness constraints can increase complexity from NP to PSpace, ExpTime and, if component counting is allowed, to NExpTime.
Uniqueness Typing for Resource Management in Message-Passing Concurrency
Venue: arXiv cs.LO 2010
Year: 2010

We view channels as the main form of resources in a message-passing programming paradigm. These channels need to be carefully managed in settings where resources are scarce. To study this problem, we extend the pi-calculus with primitives for channel allocation and deallocation and allow channels to be reused to communicate values of different types. Inevitably, the added expressiveness increases the possibilities for runtime errors. We define a substructural type system which combines uniqueness typing and affine typing to reject these ill-behaved programs.
Labelled Lambda-calculi with Explicit Copy and Erase
Venue: arXiv cs.LO 2010
Year: 2010

We present two rewriting systems that define labelled explicit substitution lambda-calculi. Our work is motivated by the close correspondence between Levy's labelled lambda-calculus and paths in proof-nets, which played an important role in the understanding of the Geometry of Interaction. The structure of the labels in Levy's labelled lambda-calculus relates to the multiplicative information of paths; the novelty of our work is that we design labelled explicit substitution calculi that also keep track of exponential information present in call-by-value and call-by-name translations of the lambda-calculus into linear logic proof-nets.
Searching publications on operating systems
Venue: arXiv cs.OS 2010
Year: 2010

This note concerns a search for publications in which one can find statements that explain the concept of an operating system, reasons for introducing operating systems, a formalization of the concept of an operating system or theory about operating systems based on such a formalization. It reports on the way in which the search has been carried out and the outcome of the search. The outcome includes not only what the search was meant for, but also some added bonuses.
Predicting the Future with Social Media
Venue: arXiv cs.CY 2010
Year: 2010

In recent years, social media has become ubiquitous and important for social networking and content sharing. And yet, the content that is generated from these websites remains largely untapped. In this paper, we demonstrate how social media content can be used to predict real-world outcomes. In particular, we use the chatter from Twitter.com to forecast box-office revenues for movies. We show that a simple model built from the rate at which tweets are created about particular topics can outperform market-based predictors. We further demonstrate how sentiments extracted from Twitter can be further utilized to improve the forecasting power of social media.
Specifying Reusable Components
Venue: arXiv cs.SE 2010
Year: 2010

Reusable software components need expressive specifications. This paper outlines a rigorous foundation to model-based contracts, a method to equip classes with strong contracts that support accurate design, implementation, and formal verification of reusable components. Model-based contracts conservatively extend the classic Design by Contract with a notion of model, which underpins the precise definitions of such concepts as abstract equivalence and specification completeness. Experiments applying model-based contracts to libraries of data structures suggest that the method enables accurate specification of practical software.
Why the Internet is so 'small'?
Venue: arXiv cs.NI 2010
Year: 2010

During the last three decades the Internet has experienced fascinating evolution, both exponential growth in traffic and rapid expansion in topology. The size of the Internet becomes enormous, yet the network is very `small' in the sense that it is extremely efficient to route data packets across the global Internet. This paper provides a brief review on three fundamental properties of the Internet topology at the autonomous systems (AS) level. Firstly the Internet has a power-law degree distribution, which means the majority of nodes on the Internet AS graph have small numbers of links, whereas a few nodes have very large numbers of links. Secondly the Internet exhibits a property called disassortative mixing, which means poorly-connected nodes tend to link with well-connected nodes, and vice versa. Thirdly the best-connected nodes, or the rich nodes, are tightly interconnected with each other forming a rich-club. We explain that it is these structural properties that make the global Internet so 'small'.
Development of a multi-user handwriting recognition system using Tesseract open source OCR engine
Venue: arXiv cs.CV 2010
Year: 2010

The objective of the paper is to recognize handwritten samples of lower case Roman script using Tesseract open source Optical Character Recognition (OCR) engine under Apache License 2.0. Handwritten data samples containing isolated and free-flow text were collected from different users. Tesseract is trained with user-specific data samples of both the categories of document pages to generate separate user-models representing a unique language-set. Each such language-set recognizes isolated and free-flow handwritten test samples collected from the designated user. On a three user model, the system is trained with 1844, 1535 and 1113 isolated handwritten character samples collected from three different users and the performance is tested on 1133, 1186 and 1204 character samples, collected form the test sets of the three users respectively. The user specific character level accuracies were obtained as 87.92%, 81.53% and 65.71% respectively. The overall character-level accuracy of the system is observed as 78.39%. The system fails to segment 10.96% characters and erroneously classifies 10.65% characters on the overall dataset.
Geometric Algebra Model of Distributed Representations
Venue: arXiv cs.AI 2010
Year: 2010

Formalism based on GA is an alternative to distributed representation models developed so far --- Smolensky's tensor product, Holographic Reduced Representations (HRR) and Binary Spatter Code (BSC). Convolutions are replaced by geometric products, interpretable in terms of geometry which seems to be the most natural language for visualization of higher concepts. This paper recalls the main ideas behind the GA model and investigates recognition test results using both inner product and a clipped version of matrix representation. The influence of accidental blade equality on recognition is also studied. Finally, the efficiency of the GA model is compared to that of previously developed models.
Multi-Stage Programs are Generalized Arrows
Venue: arXiv cs.PL 2010
Year: 2010

The lambda calculus, subject to typing restrictions, provides a syntax for the internal language of cartesian closed categories. This paper establishes a parallel result: staging annotations, subject to named level restrictions, provide a syntax for the internal language of Freyd categories, which are known to be in bijective correspondence with Arrows. The connection is made by interpreting multi-stage type systems as indexed functors from polynomial categories to their reindexings. This result applies only to multi-stage languages which are (1) homogeneous, (2) allow cross-stage persistence and (3) place no restrictions on the use of structural rules in typing derivations. Removing these restrictions and repeating the construction yields generalized arrows, of which Arrows are a particular case. A translation from well-typed multi-stage programs to single-stage GArrow terms is provided. The translation is defined by induction on the structure of the proof that the multi-stage program is well-typed, relying on information encoded in the proof's use of structural rules. Metalanguage designers can now factor out the syntactic machinery of metaprogramming by providing a single translation from staging syntax into expressions of generalized arrow type. Object language providers need only implement the functions of the generalized arrow type class in point-free style. Object language users may write metaprograms over these object languages in a point-ful style, using the same binding, scoping, abstraction, and application mechanisms in both the object language and metalanguage. This paper's principal contributions are the GArrow definition of Figures 2 and 3, the translation in Figure 5 and the category-theoretic semantics of Definition 16. An accompanying Coq proof formalizes the type system, translation procedure, and key theorems.