OpenRaiser/Intern-Atlas huggingface dataset:
A Logical Foundation for Environment Classifiers
Venue: arXiv cs.PL 2010
Year: 2010

Taha and Nielsen have developed a multi-stage calculus λα with a sound type system using the notion of environment classifiers. They are special identifiers, with which code fragments and variable declarations are annotated, and their scoping mechanism is used to ensure statically that certain code fragments are closed and safely runnable. In this paper, we investigate the Curry-Howard isomorphism for environment classifiers by developing a typed λ-calculus λ|>. It corresponds to multi-modal logic that allows quantification by transition variables---a counterpart of classifiers---which range over (possibly empty) sequences of labeled transitions between possible worlds. This interpretation will reduce the "run" construct---which has a special typing rule in λα---and embedding of closed code into other code fragments of different stages---which would be only realized by the cross-stage persistence operator in λα---to merely a special case of classifier application. λ|> enjoys not only basic properties including subject reduction, confluence, and strong normalization but also an important property as a multi-stage calculus: time-ordered normalization of full reduction. Then, we develop a big-step evaluation semantics for an ML-like language based on λ|> with its type system and prove that the evaluation of a well-typed λ|> program is properly staged. We also identify a fragment of the language, where erasure evaluation is possible. Finally, we show that the proof system augmented with a classical axiom is sound and complete with respect to a Kripke semantics of the logic.
Haar Wavelet Based Approach for Image Compression and Quality Assessment of Compressed Image
Venue: arXiv cs.MM 2010
Year: 2010

With the increasing growth of technology and the entrance into the digital age, we have to handle a vast amount of information every time which often presents difficulties. So, the digital information must be stored and retrieved in an efficient and effective manner, in order for it to be put to practical use. Wavelets provide a mathematical way of encoding information in such a way that it is layered according to level of detail. This layering facilitates approximations at various intermediate stages. These approximations can be stored using a lot less space than the original data. Here a low complex 2D image compression method using wavelets as the basis functions and the approach to measure the quality of the compressed image are presented. The particular wavelet chosen and used here is the simplest wavelet form namely the Haar Wavelet. The 2D discret wavelet transform (DWT) has been applied and the detail matrices from the information matrix of the image have been estimated. The reconstructed image is synthesized using the estimated detail matrices and information matrix provided by the Wavelet transform. The quality of the compressed images has been evaluated using some factors like Compression Ratio (CR), Peak Signal to Noise Ratio (PSNR), Mean Opinion Score (MOS), Picture Quality Scale (PQS) etc.
Rational Convex Programs, Their Feasibility, and the Arrow-Debreu Nash Bargaining Game
Venue: arXiv cs.GT 2010
Year: 2010

Over the last decade, combinatorial algorithms have been obtained for exactly solving several nonlinear convex programs. We first provide a formal context to this activity by introducing the notion of {\em rational convex programs} -- this also enables us to identify a number of questions for further study. So far, such algorithms were obtained for total problems only. Our main contribution is developing the methodology for handling non-total problems, i.e., their associated convex programs may be infeasible for certain settings of the parameters. The specific problem we study pertains to a Nash bargaining game, called ADNB, which is derived from the linear case of the Arrow-Debreu market model. We reduce this game to computing an equilibrium in a new market model called {\em flexible budget market}, and we obtain primal-dual algorithms for determining feasibility, as well as giving a proof of infeasibility and finding an equilibrium. We give an application of our combinatorial algorithm for ADNB to an important "fair" throughput allocation problem on a wireless channel.
Towards A Shape Analysis for Graph Transformation Systems
Venue: arXiv cs.PL 2010
Year: 2010

Graphs and graph transformation systems are a frequently used modelling technique for a wide range of different domains, cover- ing areas as diverse as refactorings, network topologies or reconfigurable software. Being a formal method, graph transformation systems lend themselves to a formal analysis. This has inspired the development of various verification methods, in particular also model checking tools. In this paper, we present a verification technique for infinite-state graph transformation systems. The technique employs the abstraction principle used in shape analysis of programs, summarising possibly infinitely many nodes thus giving shape graphs. The technique has been implemented using the 3-valued logical foundations of standard shape analysis. We exemplify the approach on an example from the railway domain.
Sparse coding and dictionary learning based on the MDL principle
Venue: arXiv cs.IT 2010
Year: 2010

The power of sparse signal coding with learned dictionaries has been demonstrated in a variety of applications and fields, from signal processing to statistical inference and machine learning. However, the statistical properties of these models, such as underfitting or overfitting given sets of data, are still not well characterized in the literature. This work aims at filling this gap by means of the Minimum Description Length (MDL) principle -- a well established information-theoretic approach to statistical inference. The resulting framework derives a family of efficient sparse coding and modeling (dictionary learning) algorithms, which by virtue of the MDL principle, are completely parameter free. Furthermore, such framework allows to incorporate additional prior information in the model, such as Markovian dependencies, in a natural way. We demonstrate the performance of the proposed framework with results for image denoising and classification tasks.
Polynomial Bottleneck Congestion Games with Optimal Price of Anarchy
Venue: arXiv cs.GT 2010
Year: 2010

We study {\em bottleneck congestion games} where the social cost is determined by the worst congestion of any resource. These games directly relate to network routing problems and also job-shop scheduling problems. In typical bottleneck congestion games, the utility costs of the players are determined by the worst congested resources that they use. However, the resulting Nash equilibria are inefficient, since the price of anarchy is proportional on the number of resources which can be high. Here we show that we can get smaller price of anarchy with the bottleneck social cost metric. We introduce the {\em polynomial bottleneck games} where the utility costs of the players are polynomial functions of the congestion of the resources that they use. In particular, the delay function for any resource $r$ is $C_{r}^\M$, where $C_r$ is the congestion measured as the number of players that use $r$, and $\M \geq 1$ is an integer constant that defines the degree of the polynomial. The utility cost of a player is the sum of the individual delays of the resources that it uses. The social cost of the game remains the same, namely, it is the worst bottleneck resource congestion: $\max_{r} C_r$. We show that polynomial bottleneck games are very efficient and give price of anarchy $O(|R|^{1/(\M+1)})$, where $R$ is the set of resources. This price of anarchy is tight, since we demonstrate a game with price of anarchy $Ω(|R|^{1/(\M+1)})$, for any $\M \geq 1$. We obtain our tight bounds by using two proof techniques: {\em transformation}, which we use to convert arbitrary games to simpler games, and {\em expansion}, which we use to bound the price of anarchy in a simpler game.
Emergency Response Communications and Associated Security Challenges
Venue: arXiv cs.NI 2010
Year: 2010

The natural or man-made disaster demands an efficient communication and coordination among first responders to save life and other community resources. Normally, the traditional communication infrastructures such as land line or cellular networks are damaged and don't provide adequate communication services to first responders for exchanging emergency related information. Wireless ad hoc networks such as mobile ad hoc networks, wireless sensor networks and wireless mesh networks are the promising alternatives in such type of situations. The security requirements for emergency response communications include privacy, data integrity, authentication, key management, access control and availability. Various ad hoc communication frameworks have been proposed for emergency response situations. The majority of the proposed frameworks don't provide adequate security services for reliable and secure information exchange. This paper presents a survey of the proposed emergency response communication frameworks and the potential security services required by them to provide reliable and secure information exchange during emergency situations.
Equivalence Checking in Embedded Systems Design Verification using PRES+ model
Venue: arXiv cs.LO 2010
Year: 2010

In this paper we focus on some aspects related to modeling and formal verification of embedded systems. Many models have been proposed to represent embedded systems. These models encompass a broad range of styles, characteristics, and application domains and include the extensions of finite state machines, data flow graphs, communication processes and Petri nets. In this report, we have used a PRES+ model (Petri net based Representation for Embedded Systems) as an extension of classical Petri net model that captures concurrency, timing behaviour of embedded systems; it allows systems to be representative in different levels of abstraction and improves expressiveness by allowing the token to carry information. Modeling using PRES+, as discussed above, may be convenient for specifying the input behaviour because it supports concurrency. However, there is no equivalence checking method reported in the literature for PRES+ models to the best of our knowledge. In contrast, equivalence checking of FSMD models exist. As a first step, therefore, we seek to devise an algorithm to translate PRES+ models to FSMD models and we seek to hand execute our algorithm on a real life example and we have to translate two versions of PRES+ models to FSMD models. Then using existing equivalence checker we have checked the equivalence between two FSMD models.
Authentication from matrix conjugation
Venue: arXiv cs.CR 2010
Year: 2010

We propose an authentication scheme where forgery (a.k.a. impersonation) seems infeasible without finding the prover's long-term private key. The latter would follow from solving the conjugacy search problem in the platform (noncommutative) semigroup, i.e., to recovering X from X^{-1}AX and A. The platform semigroup that we suggest here is the semigroup of nxn matrices over truncated multivariable polynomials over a ring.
Dynamic Multi Layer Signature based Intrusion Detection system Using Mobile Agents
Venue: arXiv cs.CR 2010
Year: 2010

Intrusion detection systems have become a key component in ensuring the safety of systems and networks. As networks grow in size and speed continues to increase, it is crucial that efficient scalable techniques should be developed for IDS systems. Signature based detection is the most extensively used threat detection technique for Intrusion Detection Systems (IDS). One of the foremost challenges for signaturebased IDS systems is how to keep up with large volume of incoming traffic when each packet needs to be compared with every signature in the database. When an IDS cannot keep up with the traffic flood, all it can do is to drop packets, therefore, may miss potential attacks. This paper proposes a new model called Dynamic Multi-Layer Signature based IDS using Mobile Agents, which can detect imminent threats with very high success rate by dynamically and automatically creating and using small and efficient multiple databases, and at the same time, provide mechanism to update these small signature databases at regular intervals using Mobile Agents
TCP over low-power and lossy networks: tuning the segment size to minimize energy consumption
Venue: arXiv cs.NI 2010
Year: 2010

Low-power and Lossy Networks (LLNs), like wireless networks based upon the IEEE 802.15.4 standard, have strong energy constraints, and are moreover subject to frequent transmission errors, not only due to congestion but also to collisions and to radio channel conditions. This paper introduces an analytical model to compute the total energy consumption in an LLN due to the TCP protocol. The model allows us to highlight some tradeoffs as regards the choice of the TCP maximum segment size, of the Forward Error Correction (FEC) redundancy ratio, and of the number of link-layer retransmissions, in order to minimize the total energy consumption.
A Distributed Trust Management Framework for Detecting Malicious Packet Dropping Nodes in a Mobile Ad Hoc Network
Venue: arXiv cs.CR 2010
Year: 2010

In a multi-hop mobile ad hoc network (MANET) mobile nodes communicate with each other forming a cooperative radio network. Security remains a major challenge for these networks due to their features of open medium, dynamically changing topologies, reliance on cooperative algorithms, absence of centralized monitoring points, and lack of any clear lines of defense. Most of the currently existing security algorithms designed for these networks are insecure, in efficient, and have low detection accuracy for nodes' misbehaviour. In this paper, a new approach has been proposed to bring out the complementary relationship between key distribution and misbehaviour detection for developing an integrated security solution for MANETs. The redundancy of routing information in ad hoc networks is utilized to develop a highly reliable protocol that works even in presence of transient network partitioning and Byzantine failure of nodes. The proposed mechanism is fully co-operative, and thus it is more robust as the vulnerabilities of the election algorithms used for choosing the subset of nodes for cooperation are absent. Simulation results show the effectiveness of the proposed protocol.
On the Mesh Array for Matrix Multiplication
Venue: arXiv cs.DC 2010
Year: 2010

This article presents new properties of the mesh array for matrix multiplication. In contrast to the standard array that requires 3n-2 steps to complete its computation, the mesh array requires only 2n-1 steps. Symmetries of the mesh array computed values are presented which enhance the efficiency of the array for specific applications. In multiplying symmetric matrices, the results are obtained in 3n/2+1 steps. The mesh array is examined for its application as a scrambling system.
Belief Propagation based MIMO Detection Operating on Quantized Channel Output
Venue: arXiv cs.IT 2010
Year: 2010

In multiple-antenna communications, as bandwidth and modulation order increase, system components must work with demanding tolerances. In particular, high resolution and high sampling rate analog-to-digital converters (ADCs) are often prohibitively challenging to design. Therefore ADCs for such applications should be low-resolution. This paper provides new insights into the problem of optimal signal detection based on quantized received signals for multiple-input multiple-output (MIMO) channels. It capitalizes on previous works which extensively analyzed the unquantized linear vector channel using graphical inference methods. In particular, a "loopy" belief propagation-like (BP) MIMO detection algorithm, operating on quantized data with low complexity, is proposed. In addition, we study the impact of finite receiver resolution in fading channels in the large-system limit by means of a state evolution analysis of the BP algorithm, which refers to the limit where the number of transmit and receive antennas go to infinity with a fixed ratio. Simulations show that the theoretical findings might give accurate results even with moderate number of antennas.
Fast Continuous Haar and Fourier Transforms of Rectilinear Polygons from VLSI Layouts
Venue: arXiv cs.CE 2010
Year: 2010

We develop the pruned continuous Haar transform and the fast continuous Fourier series, two fast and efficient algorithms for rectilinear polygons. Rectilinear polygons are used in VLSI processes to describe design and mask layouts of integrated circuits. The Fourier representation is at the heart of many of these processes and the Haar transform is expected to play a major role in techniques envisioned to speed up VLSI design. To ensure correct printing of the constantly shrinking transistors and simultaneously handle their increasingly large number, ever more computationally intensive techniques are needed. Therefore, efficient algorithms for the Haar and Fourier transforms are vital. We derive the complexity of both algorithms and compare it to that of discrete transforms traditionally used in VLSI. We find a significant reduction in complexity when the number of vertices of the polygons is small, as is the case in VLSI layouts. This analysis is completed by an implementation and a benchmark of the continuous algorithms and their discrete counterpart. We show that on tested VLSI layouts the pruned continuous Haar transform is 5 to 25 times faster, while the fast continuous Fourier series is 1.5 to 3 times faster.
An Introduction to Time-Constrained Automata
Venue: arXiv cs.LO 2010
Year: 2010

We present time-constrained automata (TCA), a model for hard real-time computation in which agents behaviors are modeled by automata and constrained by time intervals. TCA actions can have multiple start time and deadlines, can be aperiodic, and are selected dynamically following a graph, the time-constrained automaton. This allows expressing much more precise time constraints than classical periodic or sporadic model, while preserving the ease of scheduling and analysis. We provide some properties of this model as well as their scheduling semantics. We show that TCA can be automatically derived from source-code, and optimally scheduled on single processors using a variant of EDF. We explain how time constraints can be used to guarantee communication determinism by construction, and to study when possible agent interactions happen.
Selective Image Super-Resolution
Venue: arXiv cs.CV 2010
Year: 2010

In this paper we propose a vision system that performs image Super Resolution (SR) with selectivity. Conventional SR techniques, either by multi-image fusion or example-based construction, have failed to capitalize on the intrinsic structural and semantic context in the image, and performed "blind" resolution recovery to the entire image area. By comparison, we advocate example-based selective SR whereby selectivity is exemplified in three aspects: region selectivity (SR only at object regions), source selectivity (object SR with trained object dictionaries), and refinement selectivity (object boundaries refinement using matting). The proposed system takes over-segmented low-resolution images as inputs, assimilates recent learning techniques of sparse coding (SC) and grouped multi-task lasso (GMTL), and leads eventually to a framework for joint figure-ground separation and interest object SR. The efficiency of our framework is manifested in our experiments with subsets of the VOC2009 and MSRC datasets. We also demonstrate several interesting vision applications that can build on our system.
Fast-Decodable Asymmetric Space-Time Codes from Division Algebras
Venue: arXiv cs.IT 2010
Year: 2010

Multiple-input double-output (MIDO) codes are important in the near-future wireless communications, where the portable end-user device is physically small and will typically contain at most two receive antennas. Especially tempting is the 4 x 2 channel due to its immediate applicability in the digital video broadcasting (DVB). Such channels optimally employ rate-two space-time (ST) codes consisting of (4 x 4) matrices. Unfortunately, such codes are in general very complex to decode, hence setting forth a call for constructions with reduced complexity. Recently, some reduced complexity constructions have been proposed, but they have mainly been based on different ad hoc methods and have resulted in isolated examples rather than in a more general class of codes. In this paper, it will be shown that a family of division algebra based MIDO codes will always result in at least 37.5% worst-case complexity reduction, while maintaining full diversity and, for the first time, the non-vanishing determinant (NVD) property. The reduction follows from the fact that, similarly to the Alamouti code, the codes will be subsets of matrix rings of the Hamiltonian quaternions, hence allowing simplified decoding. At the moment, such reductions are among the best known for rate-two MIDO codes. Several explicit constructions are presented and shown to have excellent performance through computer simulations.
E-Net Models of a Software System for E-Mail Security
Venue: arXiv cs.CR 2010
Year: 2010

This paper presents solutions for cryptography protection in MS Outlook. The solutions comprise the authors' experience in development and implementation of systems for information security in the Automated Information Systems of Bulgarian Armed Forces. The architecture, the models and the methods are being explained.
Python for education: the exact cover problem
Venue: arXiv cs.DS 2010
Year: 2010

Python implementation of Algorithm X by Knuth is presented. Algorithm X finds all solutions to the exact cover problem. The exemplary results for pentominoes, Latin squares and Sudoku are given.
Editing Knowledge in Large Mathematical Corpora. A case study with Semantic LaTeX (sTeX)
Venue: arXiv cs.DL 2010
Year: 2010

Before we can get the whole potential of employing computers in the process of managing mathematical `knowledge', we have to convert informal knowledge into machine-oriented representations. How exactly to support this process so that it becomes as effortless as possible is one of the main unsolved problems of Mathematical Knowledge Management. Two independent projects in formalization of mathematical content showed that many of the time consuming tasks could be significantly reduced if adequate tool support were available. It was also established that similar tasks are typical for object oriented languages and that they are to a large extent solved by Integrated Development Environments (IDE). This thesis starts by analyzing the opportunities where formalization process can benefit from software support. A list of research questions is compiled along with a set of software requirements which are then used for developing a new IDE for the semantic \TeX{} (\stex{}) format. The result of the current research is that, indeed, IDEs can be very useful in the process of formalization and presents a set of best practices for implementing such IDEs.
Symmetry in Shannon's Noiseless Coding Theorem
Venue: arXiv cs.IT 2010
Year: 2010

Statements of Shannon's Noiseless Coding Theorem by various authors, including the original, are reviewed and clarified. Traditional statements of the theorem are often unclear as to when it applies. A new notation is introduced and the domain of application is clarified. An examination of the bounds of the Theorem leads to a new symmetric restatement. It is shown that the extended upper bound is an acheivable upper bound, giving symmetry to the theorem.The relation of information entropy to the physical entropy of Gibbs and Boltmann is illustrated. Consequently, the study of Shannon Entropy is strongly related to physics and there is a physical theory of information. This paper is the beginning of of an attempt to clarify these relationships.