OpenRaiser/Intern-Atlas huggingface dataset:
Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
Venue: arXiv cs.SC 2014
Year: 2014

Cylindrical algebraic decompositions (CADs) are a key tool for solving problems in real algebraic geometry and beyond. We recently presented a new CAD algorithm combining two advances: truth-table invariance, making the CAD invariant with respect to the truth of logical formulae rather than the signs of polynomials; and CAD construction by regular chains technology, where first a complex decomposition is constructed by refining a tree incrementally by constraint. We here consider how best to formulate problems for input to this algorithm. We focus on a choice (not relevant for other CAD algorithms) about the order in which constraints are presented. We develop new heuristics to help make this choice and thus allow the best use of the algorithm in practice. We also consider other choices of problem formulation for CAD, as discussed in CICM 2013, revisiting these in the context of the new algorithm.
High-Content Digital Microscopy with Python
Venue: arXiv cs.CE 2014
Year: 2014

High-Content Digital Microscopy enhances user comfort, data storage and analysis throughput, paving the way to new researches and medical diagnostics. A digital microscopy platform aims at capturing an image of a cover slip, at storing information on a file server and a database, at visualising the image and analysing its content. We will discuss how the Python ecosystem can provide such software framework efficiently. Moreover this paper will give an illustration of the data chunking approach to manage the huge amount of data.
Belief merging within fragments of propositional logic
Venue: arXiv cs.AI 2014
Year: 2014

Recently, belief change within the framework of fragments of propositional logic has gained increasing attention. Previous works focused on belief contraction and belief revision on the Horn fragment. However, the problem of belief merging within fragments of propositional logic has been neglected so far. This paper presents a general approach to define new merging operators derived from existing ones such that the result of merging remains in the fragment under consideration. Our approach is not limited to the case of Horn fragment but applicable to any fragment of propositional logic characterized by a closure property on the sets of models of its formulae. We study the logical properties of the proposed operators in terms of satisfaction of merging postulates, considering in particular distance-based merging operators for Horn and Krom fragments.
LaTeXML 2012 - A Year of LaTeXML
Venue: arXiv cs.DL 2014
Year: 2014

LaTeXML, a $\TeX$ to XML converter, is being used in a wide range of MKM applications. In this paper, we present a progress report for the 2012 calendar year. Noteworthy enhancements include: increased coverage such as Wikipedia syntax; enhanced capabilities such as embeddable JavaScript and CSS resources and RDFa support; a web service for remote processing via web-sockets; along with general accuracy and reliability improvements.
SPEEDY: An Eclipse-based IDE for invariant inference
Venue: arXiv cs.LO 2014
Year: 2014

SPEEDY is an Eclipse-based IDE for exploring techniques that assist users in generating correct specifications, particularly including invariant inference algorithms and tools. It integrates with several back-end tools that propose invariants and will incorporate published algorithms for inferring object and loop invariants. Though the architecture is language-neutral, current SPEEDY targets C programs. Building and using SPEEDY has confirmed earlier experience demonstrating the importance of showing and editing specifications in the IDEs that developers customarily use, automating as much of the production and checking of specifications as possible, and showing counterexample information directly in the source code editing environment. As in previous work, automation of specification checking is provided by back-end SMT solvers. However, reducing the effort demanded of software developers using formal methods also requires a GUI design that guides users in writing, reviewing, and correcting specifications and automates specification inference.
FoCaLiZe: Inside an F-IDE
Venue: arXiv cs.PL 2014
Year: 2014

For years, Integrated Development Environments have demonstrated their usefulness in order to ease the development of software. High-level security or safety systems require proofs of compliance to standards, based on analyses such as code review and, increasingly nowadays, formal proofs of conformance to specifications. This implies mixing computational and logical aspects all along the development, which naturally raises the need for a notion of Formal IDE. This paper examines the FoCaLiZe environment and explores the implementation issues raised by the decision to provide a single language to express specification properties, source code and machine-checked proofs while allowing incremental development and code reusability. Such features create strong dependencies between functions, properties and proofs, and impose an particular compilation scheme, which is described here. The compilation results are runnable OCaml code and a checkable Coq term. All these points are illustrated through a running example.
Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB
Venue: arXiv cs.SE 2014
Year: 2014

We present the implementation of pyB, a predicate - and expression - checker for the B language. The tool is to be used for a secondary tool chain for data validation and data generation, with ProB being used in the primary tool chain. Indeed, pyB is an independent cleanroom-implementation which is used to double-check solutions generated by ProB, an animator and model-checker for B specifications. One of the major goals is to use ProB together with pyB to generate reliable outputs for high-integrity safety critical applications. Although pyB is still work in progress, the ProB/pyB toolchain has already been successfully tested on various industrial B machines and data validation tasks.
Network Control without CSI using Rateless Codes for Downlink Cellular Systems
Venue: arXiv cs.IT 2014
Year: 2014

Wireless network scheduling and control techniques (e.g., opportunistic scheduling) rely heavily on access to Channel State Information (CSI). However, obtaining this information is costly in terms of bandwidth, time, and power, and could result in large overhead. Therefore, a critical question is how to optimally manage network resources in the absence of such information. To that end, we develop a cross-layer solution for downlink cellular systems with imperfect (and possibly no) CSI at the transmitter. We use rateless codes to resolve channel uncertainty. To keep the decoding complexity low, we explicitly incorporate time-average block-size constraints, and aim to maximize the system utility. The block-size of a rateless code is determined by both the network control decisions and the unknown CSI of many time slots. Therefore, unlike standard utility maximization problems, this problem can be viewed as a constrained partial observed Markov decision problem (CPOMDP), which is known to be hard due to the "curse of dimensionality." However, by using a modified Lyapunov drift method, we develop a dynamic network control scheme, which yields a total network utility within O(1/Lav) of utility-optimal point achieved by infinite block-size channel codes, where Lav is the enforced value of the time-average block-size of rateless codes. This opens the door of being able to trade complexity/delay for performance gains in the absence of accurate CSI. Our simulation results show that the proposed scheme improves the network throughput by up to 68% over schemes that use fixed-rate codes.
A Family of Descriptive Approaches To Preferred Answer Sets
Venue: arXiv cs.LO 2014
Year: 2014

In logic programming under the answer set semantics, preferences on rules are used to choose which of the conflicting rules are applied. Many interesting semantics have been proposed. Brewka and Eiter's Principle I expresses the basic intuition behind the preferences. All the approaches that satisfy Principle I introduce a rather imperative feature into otherwise declarative language. They understand preferences as the order, in which the rules of a program have to be applied. In this paper we present two purely declarative approaches for preference handling that satisfy Principle I, and work for general conflicts, including direct and indirect conflicts between rules. The first approach is based on the idea that a rule cannot be defeated by a less preferred conflicting rule. This approach is able to ignore preferences between non-conflicting rules, and, for instance, is equivalent with the answer set semantics for the subclass of stratified programs. It is suitable for the scenarios, when developers do not have full control over preferences. The second approach relaxes the requirement for ignoring conflicting rules, which ensures that it stays in the NP complexity class. It is based on the idea that a rule cannot be defeated by a rule that is less preferred or depends on a less preferred rule. The second approach can be also characterized by a transformation to logic programs without preferences. It turns out that the approaches form a hierarchy, a branch in the hierarchy of the approaches by Delgrande et. al., Wang et. al., and Brewka and Eiter. Finally, we show an application for which the existing approaches are not usable, and the approaches of this paper produce expected results.
Reallocation Mechanisms
Venue: arXiv cs.GT 2014
Year: 2014

We consider reallocation problems in settings where the initial endowment of each agent consists of a subset of the resources. The private information of the players is their value for every possible subset of the resources. The goal is to redistribute resources among agents to maximize efficiency. Monetary transfers are allowed, but participation is voluntary. We develop incentive-compatible, individually-rational and budget balanced mechanisms for several classic settings, including bilateral trade, partnership dissolving, Arrow-Debreu markets, and combinatorial exchanges. All our mechanisms (except one) provide a constant approximation to the optimal efficiency in these settings, even in ones where the preferences of the agents are complex multi-parameter functions.
Going higher in the First-order Quantifier Alternation Hierarchy on Words
Venue: arXiv cs.FL 2014
Year: 2014

We investigate the quantifier alternation hierarchy in first-order logic on finite words. Levels in this hierarchy are defined by counting the number of quantifier alternations in formulas. We prove that one can decide membership of a regular language to the levels $\mathcal{B}Σ_2$ (boolean combination of formulas having only 1 alternation) and $Σ_3$ (formulas having only 2 alternations beginning with an existential block). Our proof works by considering a deeper problem, called separation, which, once solved for lower levels, allows us to solve membership for higher levels.
Unit verification procedure as a test of real time messaging-based processes
Venue: arXiv cs.SE 2014
Year: 2014

The article presents the first results of a PhD study connected to testing of safety critical medical devices: a systematically executed case study at a Hungarian manufacturer of medical devices. The article shortly describes the process of testing currently being used. Elements of the testing approach less commonly applied in software industry are emphasized . The ending point of the actual testing process in the case study is the starting point for further research: the automated analysis of the testing results. The author started to develop a new approach, using a combination of tools, and modeling a model-based test generating tool - something that is both novel and intensive as an area of research.
Weight enumerator of some irreducible cyclic codes
Venue: arXiv cs.IT 2014
Year: 2014

In this article, we show explicitly all possible weight enumerators for every irreducible cyclic code of length $n$ over a finite field $\mathbb F_q$, in the case which each prime divisor of $n$ is also a divisor of $q-1$.
Mining online social networks with Python to study urban mobility
Venue: arXiv cs.SI 2014
Year: 2014

On-line social networks have grown quickly over the last few years and nowadays many people use them frequently. Furthermore the emergence of smartphones allows to access these networks any time from any physical location. Among the social networks, Twitter offers a particularly large set of data publicly available. Here we discuss the procedure to mine this data and store it in distributed databases using Python scripts. We also illustrate how geolocated tweets can be used to study the mobility of people in urban areas.
Scaling Laws for Infrastructure Single and Multihop Wireless Networks in Wideband Regimes
Venue: arXiv cs.IT 2014
Year: 2014

With millimeter wave bands emerging as a strong candidate for 5G cellular networks, next-generation systems may be in a unique position where spectrum is plentiful. To assess the potential value of this spectrum, this paper derives scaling laws on the per mobile downlink feasible rate with large bandwidth and number of nodes, for both Infrastructure Single Hop (ISH) and Infrastructure Multi-Hop (IMH) architectures. It is shown that, for both cases, there exist \emph{critical bandwidth scalings} above which increasing the bandwidth no longer increases the feasible rate per node. These critical thresholds coincide exactly with the bandwidths where, for each architecture, the network transitions from being degrees-of-freedom-limited to power-limited. For ISH, this critical bandwidth threshold is lower than IMH when the number of users per base station grows with network size. This result suggests that multi-hop transmissions may be necessary to fully exploit large bandwidth degrees of freedom in deployments with growing number of users per cell.
Channel Selection for Network-assisted D2D Communication via No-Regret Bandit Learning with Calibrated Forecasting
Venue: arXiv cs.GT 2014
Year: 2014

We consider the distributed channel selection problem in the context of device-to-device (D2D) communication as an underlay to a cellular network. Underlaid D2D users communicate directly by utilizing the cellular spectrum but their decisions are not governed by any centralized controller. Selfish D2D users that compete for access to the resources construct a distributed system, where the transmission performance depends on channel availability and quality. This information, however, is difficult to acquire. Moreover, the adverse effects of D2D users on cellular transmissions should be minimized. In order to overcome these limitations, we propose a network-assisted distributed channel selection approach in which D2D users are only allowed to use vacant cellular channels. This scenario is modeled as a multi-player multi-armed bandit game with side information, for which a distributed algorithmic solution is proposed. The solution is a combination of no-regret learning and calibrated forecasting, and can be applied to a broad class of multi-player stochastic learning problems, in addition to the formulated channel selection problem. Analytically, it is established that this approach not only yields vanishing regret (in comparison to the global optimal solution), but also guarantees that the empirical joint frequencies of the game converge to the set of correlated equilibria.
Query shredding: Efficient relational evaluation of queries over nested multisets (extended version)
Venue: arXiv cs.DB 2014
Year: 2014

Nested relational query languages have been explored extensively, and underlie industrial language-integrated query systems such as Microsoft's LINQ. However, relational databases do not natively support nested collections in query results. This can lead to major performance problems: if programmers write queries that yield nested results, then such systems typically either fail or generate a large number of queries. We present a new approach to query shredding, which converts a query returning nested data to a fixed number of SQL queries. Our approach, in contrast to prior work, handles multiset semantics, and generates an idiomatic SQL:1999 query directly from a normal form for nested queries. We provide a detailed description of our translation and present experiments showing that it offers comparable or better performance than a recent alternative approach on a range of examples.
Robustness against Power is PSPACE-complete
Venue: arXiv cs.LO 2014
Year: 2014

Power is a RISC architecture developed by IBM, Freescale, and several other companies and implemented in a series of POWER processors. The architecture features a relaxed memory model providing very weak guarantees with respect to the ordering and atomicity of memory accesses. Due to these weaknesses, some programs that are correct under sequential consistency (SC) show undesirable effects when run under Power. We call these programs not robust against the Power memory model. Formally, a program is robust if every computation under Power has the same data and control dependencies as some SC computation. Our contribution is a decision procedure for robustness of concurrent programs against the Power memory model. It is based on three ideas. First, we reformulate robustness in terms of the acyclicity of a happens-before relation. Second, we prove that among the computations with cyclic happens-before relation there is one in a certain normal form. Finally, we reduce the existence of such a normal-form computation to a language emptiness problem. Altogether, this yields a PSPACE algorithm for checking robustness against Power. We complement it by a matching lower bound to show PSPACE-completeness.
Inventions on Menu and Toolbar Coordination
Venue: arXiv cs.HC 2014
Year: 2014

Both toolbar and dropdown menu are used popularly in a graphical user interface with a similar objective of providing easy access to the internal functions. Often the same functions are provided through both menu and toolbar. Both toolbar and dropdown menu have their own advantages and disadvantages. A menu can provide more options occupying less real estate, while toolbar can provide a single click access without navigating through trees and branches. As a menu and toolbar system shares many common objectives, it is often useful maintain some relationship to coordinate between both the elements of a GUI system. The relationships can be easy as both of them often share the same internal function. For example, the print option in a menu will (most likely) call the same function as the print button on the toolbar. This article discusses the similarities and differences between a dropdown menu and toolbar. Five inventions trying to focus on both menu and toolbar are illustrated in the article.
Simplified Variable-Scaled Min Sum LDPC decoder for irregular LDPC Codes
Venue: arXiv cs.IT 2014
Year: 2014

Min-Sum decoding is widely used for decoding LDPC codes in many modern digital video broadcasting decoding due to its relative low complexity and robustness against quantization error. However, the suboptimal performance of the Min-Sum affects the integrated performance of wireless receivers. In this paper, we present the idea of adapting the scaling factor of the Min-Sum decoder with iterations through a simple approximation. For the ease of implementation the scaling factor can be changed in a staircase fashion. The stair step is designed to optimize the decoder performance and the required storage for its different values. The variable scaling factor proposed algorithm produces a non-trivial improvement of the performance of the Min-Sum decoding as verified by simulation results.
Theta-3 is connected
Venue: arXiv cs.CG 2014
Year: 2014

In this paper, we show that the $θ$-graph with three cones is connected. We also provide an alternative proof of the connectivity of the Yao graph with three cones.
It's a Small World for Random Surfers
Venue: arXiv cs.DM 2014
Year: 2014

We prove logarithmic upper bounds for the diameters of the random-surfer Webgraph model and the PageRank-based selection Webgraph model, confirming the small world phenomenon holds for them. In the special case when the generated graph is a tree, we provide close lower and upper bounds for the diameters of both models.
Data Driven Energy Efficiency in Buildings
Venue: arXiv cs.OH 2014
Year: 2014

Buildings across the world contribute significantly to the overall energy consumption and are thus stakeholders in grid operations. Towards the development of a smart grid, utilities and governments across the world are encouraging smart meter deployments. High resolution (often at every 15 minutes) data from these smart meters can be used to understand and optimize energy consumptions in buildings. In addition to smart meters, buildings are also increasingly managed with Building Management Systems (BMS) which control different sub-systems such as lighting and heating, ventilation, and air conditioning (HVAC). With the advent of these smart meters, increased usage of BMS and easy availability and widespread installation of ambient sensors, there is a deluge of building energy data. This data has been leveraged for a variety of applications such as demand response, appliance fault detection and optimizing HVAC schedules. Beyond the traditional use of such data sets, they can be put to effective use towards making buildings smarter and hence driving every possible bit of energy efficiency. Effective use of this data entails several critical areas from sensing to decision making and participatory involvement of occupants. Picking from wide literature in building energy efficiency, we identify five crust areas (also referred to as 5 Is) for realizing data driven energy efficiency in buildings : i) instrument optimally; ii) interconnect sub-systems; iii) inferred decision making; iv) involve occupants and v) intelligent operations. We classify prior work as per these 5 Is and dis-cuss challenges, opportunities and applications across them. Building upon these 5 Is we discuss a well studied problem in building energy efficiency -non-intrusive load monitoring (NILM) and how research in this area spans across the 5 Is.
Weak MSO+U with Path Quantifiers over Infinite Trees
Venue: arXiv cs.LO 2014
Year: 2014

This paper shows that over infinite trees, satisfiability is decidable for weak monadic second-order logic extended by the unbounding quantifier U and quantification over infinite paths. The proof is by reduction to emptiness for a certain automaton model, while emptiness for the automaton model is decided using profinite trees.
Disjoint-Path Selection in Internet: What traceroutes tell us?
Venue: arXiv cs.NI 2014
Year: 2014

Routing policies used in the Internet can be restrictive, limiting communication between source-destination pairs to one path, when often better alternatives exist. To avoid route flapping, recovery mechanisms may be dampened, making adaptation slow. Unstructured overlays have been proposed to mitigate the issues of path and performance failures in the Internet by routing through an indirect-path via overlay peer(s). Choosing alternate-paths in overlay networks is a challenging issue. Ensuring both availability and performance guarantees on alternate paths requires aggressive monitoring of all overlay paths using active probing; this limits scalability. An alternate technique to select an overlay-path is to bias its selection based on physical disjointness criteria to bypass the failure on the primary-path. Recently, several techniques have emerged which can optimize the selection of a disjoint-path without incurring the high costs associated with probing paths. In this paper, we show that using only commodity approaches, i.e. running infrequent traceroutes between overlay hosts, a lot of information can be revealed about the underlying physical path diversity in the overlay network which can be used to make informed-guesses for alternate-path selection. We test our approach using datasets between real-world hosts in AMP and RIPE networks.