OpenRaiser/Intern-Atlas huggingface dataset:
Disjunctive form and the modal $μ$ alternation hierarchy
Venue: arXiv cs.LO 2015
Year: 2015

This paper studies the relationship between disjunctive form, a syntactic normal form for the modal mu calculus, and the alternation hierarchy. First it shows that all disjunctive formulas which have equivalent tableau have the same syntactic alternation depth. However, tableau equivalence only preserves alternation depth for the disjunctive fragment: there are disjunctive formulas with arbitrarily high alternation depth that are tableau equivalent to alternation-free non-disjunctive formulas. Conversely, there are non-disjunctive formulas of arbitrarily high alternation depth that are tableau equivalent to disjunctive formulas without alternations. This answers negatively the so far open question of whether disjunctive form preserves alternation depth. The classes of formulas studied here illustrate a previously undocumented type of avoidable syntactic complexity which may contribute to our understanding of why deciding the alternation hierarchy is still an open problem.
Recurrent Reinforcement Learning: A Hybrid Approach
Venue: arXiv cs.LG 2015
Year: 2015

Successful applications of reinforcement learning in real-world problems often require dealing with partially observable states. It is in general very challenging to construct and infer hidden states as they often depend on the agent's entire interaction history and may require substantial domain knowledge. In this work, we investigate a deep-learning approach to learning the representation of states in partially observable tasks, with minimal prior knowledge of the domain. In particular, we propose a new family of hybrid models that combines the strength of both supervised learning (SL) and reinforcement learning (RL), trained in a joint fashion: The SL component can be a recurrent neural networks (RNN) or its long short-term memory (LSTM) version, which is equipped with the desired property of being able to capture long-term dependency on history, thus providing an effective way of learning the representation of hidden states. The RL component is a deep Q-network (DQN) that learns to optimize the control for maximizing long-term rewards. Extensive experiments in a direct mailing campaign problem demonstrate the effectiveness and advantages of the proposed approach, which performs the best among a set of previous state-of-the-art methods.
uIP Support for the Network Simulation Cradle
Venue: arXiv cs.NI 2015
Year: 2015

This paper introduces the ongoing integration of Contiki's uIP stack into the OMNeT++ port of the Network Simulation Cradle (NSC). The NSC utilizes code from real world stack implementations and allows for an accurate simulation and comparison of different TCP/IP stacks. uIP(v6) provides resource-constrained devices with an RFC-compliant TCP/IP stack and promotes the use of IPv6 in the vastly growing field of Internet of Things scenarios. This work-in-progress report discusses our motivation to integrate uIP into the NSC, our chosen approach and possible use cases for the simulation of uIP in OMNeT++.
Domain-Specific Modeling and Code Generation for Cross-Platform Multi-Device Mobile Apps
Venue: arXiv cs.SE 2015
Year: 2015

Nowadays, mobile devices constitute the most common computing device. This new computing model has brought intense competition among hardware and software providers who are continuously introducing increasingly powerful mobile devices and innovative OSs into the market. In consequence, cross-platform and multi-device development has become a priority for software companies that want to reach the widest possible audience. However, developing an application for several platforms implies high costs and technical complexity. Currently, there are several frameworks that allow cross-platform application development. However, these approaches still require manual programming. My research proposes to face the challenge of the mobile revolution by exploiting abstraction, modeling and code generation, in the spirit of the modern paradigm of Model Driven Engineering.
Fast Exact Shortest Path and Distance Queries on Road Networks with Parametrized Costs
Venue: arXiv cs.DS 2015
Year: 2015

We study a scenario for route planning in road networks, where the objective to be optimized may change between every shortest path query. Since this invalidates many of the known speedup techniques for road networks that are based on preprocessing of shortest path structures, we investigate optimizations exploiting solely the topological structure of networks. We experimentally evaluate our technique on a large set of real-world road networks of various data sources. With lightweight preprocessing our technique answers long-distance queries across continental networks significantly faster than previous approaches towards the same problem formulation.
High Frequency Radio Network Simulation Using OMNeT++
Venue: arXiv cs.NI 2015
Year: 2015

Harris Corporation has an interest in making HF radios a suitable medium for wireless information networks using standard Internet protocols. Although HF radio links have many unique characteristics, HF wireless subnets can be subject to many of the same traffic flow characteristics and topologies as existing line-of-sight (LOS) radio networks, giving rise to similar issues (media access, connectivity, routing) which lend themselves to investigation through simulation. Accordingly, we have undertaken to develop efficient, high-fidelity simulations of various aspects of HF radio communications and networking using the OMNeT++ framework. Essential aspects of these simulations include HF channel models simulating relevant channel attributes such as Signal to Noise Ratio, multipath, and Doppler spread; a calibrated physical layer model reproducing the error statistics (including burst error distributions) of the MIL-STD-188-110B/C HF modem waveforms, both narrowband (3 kHz) and wideband (up to 24 kHz) on the simulated HF channels; a model of the NATO STANAG 5066 data link protocol; and integration of these models with the OMNeT++ network simulation framework and its INET library of Internet protocol models. This simulation is used to evaluate the impacts of different STANAG 5066 configuration settings on TCP network performance, and to evaluate strategies for optimizing throughput over HF links using TCP Performance Enhancing Proxy (PEP) techniques.
Use it or Lose it: Selective Memory and Forgetting in a Perpetual Learning Machine
Venue: arXiv cs.LG 2015
Year: 2015

In a recent article we described a new type of deep neural network - a Perpetual Learning Machine (PLM) - which is capable of learning 'on the fly' like a brain by existing in a state of Perpetual Stochastic Gradient Descent (PSGD). Here, by simulating the process of practice, we demonstrate both selective memory and selective forgetting when we introduce statistical recall biases during PSGD. Frequently recalled memories are remembered, whilst memories recalled rarely are forgotten. This results in a 'use it or lose it' stimulus driven memory process that is similar to human memory.
Towards Understanding Egyptian Arabic Dialogues
Venue: arXiv cs.CL 2015
Year: 2015

Labelling of user's utterances to understanding his attends which called Dialogue Act (DA) classification, it is considered the key player for dialogue language understanding layer in automatic dialogue systems. In this paper, we proposed a novel approach to user's utterances labeling for Egyptian spontaneous dialogues and Instant Messages using Machine Learning (ML) approach without relying on any special lexicons, cues, or rules. Due to the lack of Egyptian dialect dialogue corpus, the system evaluated by multi-genre corpus includes 4725 utterances for three domains, which are collected and annotated manually from Egyptian call-centers. The system achieves F1 scores of 70. 36% overall domains.
A Formal C Memory Model for Separation Logic
Venue: arXiv cs.LO 2015
Year: 2015

The core of a formal semantics of an imperative programming language is a memory model that describes the behavior of operations on the memory. Defining a memory model that matches the description of C in the C11 standard is challenging because C allows both high-level (by means of typed expressions) and low-level (by means of bit manipulation) memory accesses. The C11 standard has restricted the interaction between these two levels to make more effective compiler optimizations possible, on the expense of making the memory model complicated. We describe a formal memory model of the (non-concurrent part of the) C11 standard that incorporates these restrictions, and at the same time describes low-level memory operations. This formal memory model includes a rich permission model to make it usable in separation logic and supports reasoning about program transformations. The memory model and essential properties of it have been fully formalized using the Coq proof assistant.
A sub-optimal solution for optimal control of linear systems with unmeasurable switching delays
Venue: arXiv cs.SY 2015
Year: 2015

We consider the optimal control design problem for discrete-time LTI systems with state feedback, when the actuation signal is subject to unmeasurable switching propagation delays, due to e.g. the routing in a multi-hop communication network and/or jitter. In particular, we set up a constrained optimization problem where the cost function is the worst-case $\mathcal{L}_2$ norm for all admissible switching delays. We first show how to model these systems as pure switching linear systems, and as main contribution of the paper we provide an algorithm to compute a sub-optimal solution.
Receiver Algorithm based on Differential Signaling for SIMO Phase Noise Channels with Common and Separate Oscillator Configurations
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, a receiver algorithm consisting of differential transmission and a two-stage detection for a single-input multiple-output (SIMO) phase-noise channels is studied. Specifically, the phases of the QAM modulated data symbols are manipulated before transmission in order to make them more immune to the random rotational effects of phase noise. At the receiver, a two-stage detector is implemented, which first detects the amplitude of the transmitted symbols from a nonlinear combination of the received signal amplitudes. Then in the second stage, the detector performs phase detection. The studied signaling method does not require transmission of any known symbols that act as pilots. Furthermore, no phase noise estimator (or a tracker) is needed at the receiver to compensate the effect of phase noise. This considerably reduces the complexity of the receiver structure. Moreover, it is observed that the studied algorithm can be used for the setups where a common local oscillator or separate independent oscillators drive the radio-frequency circuitries connected to each antenna. Due to the differential encoding/decoding of the phase, weighted averaging can be employed at a multi-antenna receiver, allowing for phase noise suppression to leverage the large number of antennas. Hence, we observe that the performance improves by increasing the number of antennas, especially in the separate oscillator case. Further increasing the number of receive antennas results in a performance error floor, which is a function of the quality of the oscillator at the transmitter.
Program Analysis with Local Policy Iteration
Venue: arXiv cs.LO 2015
Year: 2015

We present a new algorithm for deriving numerical invariants that combines the precision of max-policy iteration with the flexibility and scalability of conventional Kleene iterations. It is defined in the Configurable Program Analysis (CPA) framework, thus allowing inter-analysis communication. It uses adjustable-block encoding in order to traverse loop-free program sections, possibly containing branching, without introducing extra abstraction. Our technique operates over any template linear constraint domain, including the interval and octagon domains; templates can also be derived from the program source. The implementation is evaluated on a set of benchmarks from the Software Verification Competition (SV-Comp). It competes favorably with state-of-the-art analyzers.
On 4-Map Graphs and 1-Planar Graphs and their Recognition Problem
Venue: arXiv cs.CG 2015
Year: 2015

We establish a one-to-one correspondence between 1-planar graphs and general and hole-free 4-map graphs and show that 1-planar graphs can be recognized in polynomial time if they are crossing-augmented, fully triangulated, and maximal 1-planar, respectively, with a polynomial of degree 120, 3, and 5, respectively.
Relational reasoning via probabilistic coupling
Venue: arXiv cs.LO 2015
Year: 2015

Probabilistic coupling is a powerful tool for analyzing pairs of probabilistic processes. Roughly, coupling two processes requires finding an appropriate witness process that models both processes in the same probability space. Couplings are powerful tools proving properties about the relation between two processes, include reasoning about convergence of distributions and stochastic dominance---a probabilistic version of a monotonicity property. While the mathematical definition of coupling looks rather complex and cumbersome to manipulate, we show that the relational program logic pRHL---the logic underlying the EasyCrypt cryptographic proof assistant---already internalizes a generalization of probabilistic coupling. With this insight, constructing couplings is no harder than constructing logical proofs. We demonstrate how to express and verify classic examples of couplings in pRHL, and we mechanically verify several couplings in EasyCrypt.
Fingerprint Recognition Using Translation Invariant Scattering Network
Venue: arXiv cs.CV 2015
Year: 2015

Fingerprint recognition has drawn a lot of attention during last decades. Different features and algorithms have been used for fingerprint recognition in the past. In this paper, a powerful image representation called scattering transform/network, is used for recognition. Scattering network is a convolutional network where its architecture and filters are predefined wavelet transforms. The first layer of scattering representation is similar to sift descriptors and the higher layers capture higher frequency content of the signal. After extraction of scattering features, their dimensionality is reduced by applying principal component analysis (PCA). At the end, multi-class SVM is used to perform template matching for the recognition task. The proposed scheme is tested on a well-known fingerprint database and has shown promising results with the best accuracy rate of 98\%.
Implementation of a Wake-up Radio Cross-Layer Protocol in OMNeT++ / MiXiM
Venue: arXiv cs.NI 2015
Year: 2015

This paper presents the DoRa protocol, which is a new cross-layer protocol for handling the double radio of nodes in wake-up radio scenario. The implementation details in OMNET++/MiXiM are also given, with a focus on the implemented MAC layers. The main goal of the DoRa protocol is to reduce energy consumption in wireless sensor network, by taking full advantage of the passive wake-up scheme. The performance of the DoRa protocol is then evaluated and results are compared with B-MAC and IEEE 802.15.4 protocols.
Regain Control of Growing Dependencies in OMNeT++ Simulations
Venue: arXiv cs.SE 2015
Year: 2015

When designing simulation models, it is favourable to reuse existing models as far as possible to reduce the effort from the first idea to simulation results. Thanks to the OMNeT++ community, there are several toolboxes available covering a wide range of network communication protocols. However, it can be quite a daunting task to handle the build process when multiple existing simulation models need to be combined with custom sources. Project references provided by the OMNeT++ Integrated Development Environment (IDE) are just partly up to the task because it can be barely automated. For this reason, a new approach is presented to build complex simulation models with the help of CMake, which is a wide-spread build tool for C and C++ projects. The resulting toolchain allows to handle dependencies conveniently without need for any changes in upstream projects and also takes special care of OMNeT++-specific aspects.
Lazy Factored Inference for Functional Probabilistic Programming
Venue: arXiv cs.AI 2015
Year: 2015

Probabilistic programming provides the means to represent and reason about complex probabilistic models using programming language constructs. Even simple probabilistic programs can produce models with infinitely many variables. Factored inference algorithms are widely used for probabilistic graphical models, but cannot be applied to these programs because all the variables and factors have to be enumerated. In this paper, we present a new inference framework, lazy factored inference (LFI), that enables factored algorithms to be used for models with infinitely many variables. LFI expands the model to a bounded depth and uses the structure of the program to precisely quantify the effect of the unexpanded part of the model, producing lower and upper bounds to the probability of the query.
A Tutorial of the Mobile Multimedia Wireless Sensor Network OMNeT++ Framework
Venue: arXiv cs.NI 2015
Year: 2015

In this work, we will give a detailed tutorial instruction about how to use the Mobile Multi-Media Wireless Sensor Networks (M3WSN) simulation framework. The M3WSN framework has been published as a scientific paper in the 6th International Workshop on OMNeT++ (2013). M3WSN framework enables the multimedia transmission of real video sequence. Therefore, a set of multimedia algorithms, protocols, and services can be evaluated by using QoE metrics. Moreover, key video-related information, such as frame types, GoP length and intra-frame dependency can be used for creating new assessment and optimization solutions. To support mobility, M3WSN utilizes different mobility traces to enable the understanding of how the network behaves under mobile situations. This tutorial will cover how to install and configure the M3WSN framework, setting and running the experiments, creating mobility and video traces, and how to evaluate the performance of different protocols. The tutorial will be given in an environment of Ubuntu 12.04 LTS and OMNeT++ 4.2.
Invited Abstract: Issues with State-based Energy Consumption Modelling
Venue: arXiv cs.NI 2015
Year: 2015

Energy consumption modelling by state based approaches often assume constant energy consumption values in each state. However, it happens in certain situations that during state transitions or even during a state the energy consumption is not constant and does fluctuate. This paper discusses those issues by presenting some examples from wireless sensor and wireless local area networks for such cases and possible solutions.
On extremal trees with respect to the $F$-index
Venue: arXiv cs.DM 2015
Year: 2015

In a study on the structure--dependency of the total $π$-electron energy from 1972, Trinajstić and one of the present authors have shown that it depends on the sums $\sum_{v\in V}d(v)^2$ and $\sum_{v\in V}d(v)^3$, where $d(v)$ is the degree of a vertex $v$ of the underling molecular graph $G$. The first sum was later named {\it first Zagreb index} and over the years became one of the most investigated graph--based molecular structure descriptors. On the other hand, the second sum, except in very few works on the general first Zagreb index and the zeroth--order general Randić index, has been almost completely neglected. Recently, this second sum was named {\em forgotten index}, or shortly the $F$-{\em index}, and shown to have an exceptional applicative potential. In this paper we examine the trees extremal with respect to the $F$-index.
Good Colour Maps: How to Design Them
Venue: arXiv cs.GR 2015
Year: 2015

Many colour maps provided by vendors have highly uneven perceptual contrast over their range. It is not uncommon for colour maps to have perceptual flat spots that can hide a feature as large as one tenth of the total data range. Colour maps may also have perceptual discontinuities that induce the appearance of false features. Previous work in the design of perceptually uniform colour maps has mostly failed to recognise that CIELAB space is only designed to be perceptually uniform at very low spatial frequencies. The most important factor in designing a colour map is to ensure that the magnitude of the incremental change in perceptual lightness of the colours is uniform. The specific requirements for linear, diverging, rainbow and cyclic colour maps are developed in detail. To support this work two test images for evaluating colour maps are presented. The use of colour maps in combination with relief shading is considered and the conditions under which colour can enhance or disrupt relief shading are identified. Finally, a set of new basis colours for the construction of ternary images are presented. Unlike the RGB primaries these basis colours produce images whereby the salience of structures are consistent irrespective of the assignment of basis colours to data channels.
Silent Self-stabilizing BFS Tree Algorithms Revised
Venue: arXiv cs.DC 2015
Year: 2015

In this paper, we revisit two fundamental results of the self-stabilizing literature about silent BFS spanning tree constructions: the Dolev et al algorithm and the Huang and Chen's algorithm. More precisely, we propose in the composite atomicity model three straightforward adaptations inspired from those algorithms. We then present a deep study of these three algorithms. Our results are related to both correctness (convergence and closure, assuming a distributed unfair daemon) and complexity (analysis of the stabilization time in terms of rounds and steps).
Voronoi-Based Coverage Control of Heterogeneous Disk-Shaped Robots
Venue: arXiv cs.RO 2015
Year: 2015

In distributed mobile sensing applications, networks of agents that are heterogeneous respecting both actuation as well as body and sensory footprint are often modelled by recourse to power diagrams --- generalized Voronoi diagrams with additive weights. In this paper we adapt the body power diagram to introduce its "free subdiagram," generating a vector field planner that solves the combined sensory coverage and collision avoidance problem via continuous evaluation of an associated constrained optimization problem. We propose practical extensions (a heuristic congestion manager that speeds convergence and a lift of the point particle controller to the more practical differential drive kinematics) that maintain the convergence and collision guarantees.
Benchmarking for Bayesian Reinforcement Learning
Venue: arXiv cs.AI 2015
Year: 2015

In the Bayesian Reinforcement Learning (BRL) setting, agents try to maximise the collected rewards while interacting with their environment while using some prior knowledge that is accessed beforehand. Many BRL algorithms have already been proposed, but even though a few toy examples exist in the literature, there are still no extensive or rigorous benchmarks to compare them. The paper addresses this problem, and provides a new BRL comparison methodology along with the corresponding open source library. In this methodology, a comparison criterion that measures the performance of algorithms on large sets of Markov Decision Processes (MDPs) drawn from some probability distributions is defined. In order to enable the comparison of non-anytime algorithms, our methodology also includes a detailed analysis of the computation time requirement of each algorithm. Our library is released with all source code and documentation: it includes three test problems, each of which has two different prior distributions, and seven state-of-the-art RL algorithms. Finally, our library is illustrated by comparing all the available algorithms and the results are discussed.