OpenRaiser/Intern-Atlas huggingface dataset:
Potential Maximal Clique Algorithms for Perfect Phylogeny Problems
Venue: arXiv cs.DM 2013
Year: 2013

Kloks, Kratsch, and Spinrad showed how treewidth and minimum-fill, NP-hard combinatorial optimization problems related to minimal triangulations, are broken into subproblems by block subgraphs defined by minimal separators. These ideas were expanded on by Bouchitté and Todinca, who used potential maximal cliques to solve these problems using a dynamic programming approach in time polynomial in the number of minimal separators of a graph. It is known that solutions to the perfect phylogeny problem, maximum compatibility problem, and unique perfect phylogeny problem are characterized by minimal triangulations of the partition intersection graph. In this paper, we show that techniques similar to those proposed by Bouchitté and Todinca can be used to solve the perfect phylogeny problem with missing data, the two- state maximum compatibility problem with missing data, and the unique perfect phylogeny problem with missing data in time polynomial in the number of minimal separators of the partition intersection graph.
Towards Dynamic Real-Time Geo-location Databases for TV White Spaces
Venue: arXiv cs.NI 2013
Year: 2013

Recent FCC regulations on TV white spaces allow geo-location databases to be the sole source of spectrum information for White Space Devices (WSDs). Geo-location databases protect TV band incumbents by keeping track of TV transmitters and their protected service areas based on their location, transmission parameters and sophisticated propagation models. In this article, we argue that keeping track of both TV transmitters and TV receivers (i.e. TV sets) can achieve significant improvement in the availability of white spaces. We first identify wasted spectrum opportunities, both temporal and spatial, due to the current approach of white spaces detection. We then propose DynaWhite, a cloud-based architecture that orchestrates the detection and dissemination of highly-dynamic, real-time, and fine-grained TV white space information. DynaWhite introduces the next generation of geo-location databases by combining traditional sensing techniques with a novel unconventional sensing approach based on the detection of the passive TV receivers using standard cell phones. We present a quantitative evaluation of the potential gains in white space availability for large scale deployments of DynaWhite. We finally identify challenges that need to be addressed in the research community in order to exploit this potential for leveraging dynamic real-time fine-grained TV white spaces.
$l_{2,p}$ Matrix Norm and Its Application in Feature Selection
Venue: arXiv cs.LG 2013
Year: 2013

Recently, $l_{2,1}$ matrix norm has been widely applied to many areas such as computer vision, pattern recognition, biological study and etc. As an extension of $l_1$ vector norm, the mixed $l_{2,1}$ matrix norm is often used to find jointly sparse solutions. Moreover, an efficient iterative algorithm has been designed to solve $l_{2,1}$-norm involved minimizations. Actually, computational studies have showed that $l_p$-regularization ($0<p<1$) is sparser than $l_1$-regularization, but the extension to matrix norm has been seldom considered. This paper presents a definition of mixed $l_{2,p}$ $(p\in (0, 1])$ matrix pseudo norm which is thought as both generalizations of $l_p$ vector norm to matrix and $l_{2,1}$-norm to nonconvex cases $(0<p<1)$. Fortunately, an efficient unified algorithm is proposed to solve the induced $l_{2,p}$-norm $(p\in (0, 1])$ optimization problems. The convergence can also be uniformly demonstrated for all $p\in (0, 1]$. Typical $p\in (0,1]$ are applied to select features in computational biology and the experimental results show that some choices of $0<p<1$ do improve the sparse pattern of using $p=1$.
Separating Topology and Geometry in Space Planning
Venue: arXiv cs.AI 2013
Year: 2013

We are dealing with the problem of space layout planning here. We present an architectural conceptual CAD approach. Starting with design specifications in terms of constraints over spaces, a specific enumeration heuristics leads to a complete set of consistent conceptual design solutions named topological solutions. These topological solutions which do not presume any precise definitive dimension correspond to the sketching step that an architect carries out from the Design specifications on a preliminary design phase in architecture.
Performance Analysis of OFDM-based System for Various Channels
Venue: arXiv cs.IT 2013
Year: 2013

The demand for high-speed mobile wireless communications is rapidly growing. Orthogonal Frequency Division Multiplexing (OFDM) technology promises to be a key technique for achieving the high data capacity and spectral efficiency requirements for wireless communication systems in the near future. This paper investigates the performance of OFDM-based system over static and non-static or fading channels. In order to investigate this, a simulation model has been created and implemented using MATLAB. A comparison has also been made between the performances of coherent and differential modulation scheme over static and fading channels. In the fading channels, it has been found that OFDM-based system's performance depends severely on Doppler shift which in turn depends on the velocity of user. It has been found that performance degrades as Doppler shift increases, as expected. This paper also performs a comparative study of OFDM-based system's performance on different fading channels and it has been found that it performs better over Rician channel, as expected and system performance improves as the value of Rician factor increases, as expected. As a last task, a coding technique, Gray Coding, has been used to improve system performace and it is found that it improves system performance by reducing BER about 25-32 percent.
A weaving process to define requirements for Cooperative Information System
Venue: arXiv cs.SE 2013
Year: 2013

The development of a Cooperative Information System (CIS) becomes more and more complex, new challenges arise for managing this complexity. So, the aspect paradigm is regarded as a promising software development technique which can reduce the complexity and cost of developing large software systems. This opportunity can be used to develop a CIS able to support the interconnection of organizations information systems in order to ensure a common global service and to support the tempo of change in the business world that is increasing at an exponential level. We previously proposed an approach named AspeCiS (An Aspect-oriented Approach to Develop a Cooperative Information System) to develop a Cooperative Information System from existing Information Systems by using their artifacts such as existing requirements, and design. In this approach we have studied how to elicit CIS Requirements called Cooperative Requirements in AspeCiS. In this paper we propose a weaving process to define these requirements by reusing existing requirements and new aspectual requirements that we define to modify these requirements in order to be reused.
Using Smartphones as a Proxy for Forensic Evidence contained in Cloud Storage Services
Venue: arXiv cs.CR 2013
Year: 2013

Cloud storage services such as Dropbox, Box and SugarSync have been embraced by both individuals and organizations. This creates an environment that is potentially conducive to security breaches and malicious activities. The investigation of these cloud environments presents new challenges for the digital forensics community. It is anticipated that smartphone devices will retain data from these storage services. Hence, this research presents a preliminary investigation into the residual artifacts created on an iOS and Android device that has accessed a cloud storage service. The contribution of this paper is twofold. First, it provides an initial assessment on the extent to which cloud storage data is stored on these client-side devices. This view acts as a proxy for data stored in the cloud. Secondly, it provides documentation on the artifacts that could be useful in a digital forensics investigation of cloud services.
Sparse Phase Retrieval: Convex Algorithms and Limitations
Venue: arXiv cs.IT 2013
Year: 2013

We consider the problem of recovering signals from their power spectral density. This is a classical problem referred to in literature as the phase retrieval problem, and is of paramount importance in many fields of applied sciences. In general, additional prior information about the signal is required to guarantee unique recovery as the mapping from signals to power spectral density is not one-to-one. In this paper, we assume that the underlying signals are sparse. Recently, semidefinite programming (SDP) based approaches were explored by various researchers. Simulations of these algorithms strongly suggest that signals upto $o(\sqrt{n})$ sparsity can be recovered by this technique. In this work, we develop a tractable algorithm based on reweighted $l_1$-minimization that recovers a sparse signal from its power spectral density for significantly higher sparsities, which is unprecedented. We discuss the square-root bottleneck of the existing convex algorithms and show that a $k$-sparse signal can be efficiently recovered using $O(k^2logn)$ phaseless Fourier measurements. We also show that a $k$-sparse signal can be recovered using only $O(k log n)$ phaseless measurements if we are allowed to design the measurement matrices.
Improved Foreground Detection via Block-based Classifier Cascade with Probabilistic Decision Integration
Venue: arXiv cs.CV 2013
Year: 2013

Background subtraction is a fundamental low-level processing task in numerous computer vision applications. The vast majority of algorithms process images on a pixel-by-pixel basis, where an independent decision is made for each pixel. A general limitation of such processing is that rich contextual information is not taken into account. We propose a block-based method capable of dealing with noise, illumination variations and dynamic backgrounds, while still obtaining smooth contours of foreground objects. Specifically, image sequences are analysed on an overlapping block-by-block basis. A low-dimensional texture descriptor obtained from each block is passed through an adaptive classifier cascade, where each stage handles a distinct problem. A probabilistic foreground mask generation approach then exploits block overlaps to integrate interim block-level decisions into final pixel-level foreground segmentation. Unlike many pixel-based methods, ad-hoc post-processing of foreground masks is not required. Experiments on the difficult Wallflower and I2R datasets show that the proposed approach obtains on average better results (both qualitatively and quantitatively) than several prominent methods. We furthermore propose the use of tracking performance as an unbiased approach for assessing the practical usefulness of foreground segmentation methods, and show that the proposed approach leads to considerable improvements in tracking accuracy on the CAVIAR dataset.
Generating extrema approximation of analytically incomputable functions through usage of parallel computer aided genetic algorithms
Venue: arXiv cs.AI 2013
Year: 2013

This paper presents capabilities of using genetic algorithms to find approximations of function extrema, which cannot be found using analytic ways. To enhance effectiveness of calculations, algorithm has been parallelized using OpenMP library. We gained much increase in speed on platforms using multithreaded processors with shared memory free access. During analysis we used different modifications of genetic operator, using them we obtained varied evolution process of potential solutions. Results allow to choose best methods among many applied in genetic algorithms and observation of acceleration on Yorkfield, Bloomfield, Westmere-EX and most recent Sandy Bridge cores.
The ForMaRE Project - Formal Mathematical Reasoning in Economics
Venue: arXiv cs.CE 2013
Year: 2013

The ForMaRE project applies formal mathematical reasoning to economics. We seek to increase confidence in economics' theoretical results, to aid in discovering new results, and to foster interest in formal methods, i.e. computer-aided reasoning, within economics. To formal methods, we seek to contribute user experience feedback from new audiences, as well as new challenge problems. In the first project year, we continued earlier game theory studies but then focused on auctions, where we are building a toolbox of formalisations, and have started to study matching and financial risk. In parallel to conducting research that connects economics and formal methods, we organise events and provide infrastructure to connect both communities, from fostering mutual awareness to targeted matchmaking. These efforts extend beyond economics, towards generally enabling domain experts to use mechanised reasoning.
CERES for First-Order Schemata
Venue: arXiv cs.LO 2013
Year: 2013

The cut-elimination method CERES (for first- and higher-order classical logic) is based on the notion of a characteristic clause set, which is extracted from an LK-proof and is always unsatisfiable. A resolution refutation of this clause set can be used as a skeleton for a proof with atomic cuts only (atomic cut normal form). This is achieved by replacing clauses from the resolution refutation by the corresponding projections of the original proof. We present a generalization of CERES (called CERESs) to first-order proof schemata and define a schematic version of the sequent calculus called LKS, and a notion of proof schema based on primitive recursive definitions. A method is developed to extract schematic characteristic clause sets and schematic projections from these proof schemata. We also define a schematic resolution calculus for refutation of schemata of clause sets, which can be applied to refute the schematic characteristic clause sets. Finally the projection schemata and resolution schemata are plugged together and a schematic representation of the atomic cut normal forms is obtained. A major benefit of CERESs is the extension of cut-elimination to inductively defined proofs: we compare CERESs with standard calculi using induction rules and demonstrate that CERESs is capable of performing cut-elimination where traditional methods fail. The algorithmic handling of CERESs is supported by a recent extension of the CERES system.
StegTorrent: a Steganographic Method for the P2P File Sharing Service
Venue: arXiv cs.MM 2013
Year: 2013

The paper proposes StegTorrent a new network steganographic method for the popular P2P file transfer service-BitTorrent. It is based on modifying the order of data packets in the peer-peer data exchange protocol. Unlike other existing steganographic methods that modify the packets' order it does not require any synchronization. Experimental results acquired from prototype implementation proved that it provides high steganographic bandwidth of up to 270 b/s while introducing little transmission distortion and providing difficult detectability.
Simple Schemas for Unordered XML
Venue: arXiv cs.DB 2013
Year: 2013

We consider unordered XML, where the relative order among siblings is ignored, and propose two simple yet practical schema formalisms: disjunctive multiplicity schemas (DMS), and its restriction, disjunction-free multiplicity schemas (MS). We investigate their computational properties and characterize the complexity of the following static analysis problems: schema satisfiability, membership of a tree to the language of a schema, schema containment, twig query satisfiability, implication, and containment in the presence of schema. Our research indicates that the proposed formalisms retain much of the expressiveness of DTDs without an increase in computational complexity.
Maximizing the Lifetime of Multi-chain PEGASIS using Sink Mobility
Venue: arXiv cs.NI 2013
Year: 2013

In this paper, we propose the mobility of a sink in improved energy efficient PEGASIS-based protocol (IEEPB) to advance the network lifetime of Wireless Sensor Networks (WSNs). The multi-head chain, multi-chain concept and the sink mobility affects largely in enhancing the network lifetime of wireless sensors. Thus, we recommend Mobile sink improved energy-efficient PEGASIS-based routing protocol (MIEEPB); a multi-chain model having a sink mobility, to achieve proficient energy utilization of wireless sensors. As the motorized movement of mobile sink is steered by petrol or current, there is a need to confine this movement within boundaries and the trajectory of mobile sink should be fixed. In our technique, the mobile sink moves along its trajectory and stays for a sojourn time at sojourn location to guarantee complete data collection. We develop an algorithm for trajectory of mobile sink. We ultimately perform wide-ranging experiments to assess the performance of the proposed method. The results reveal that the proposed way out is nearly optimal and also better than IEEPB in terms of network lifetime.
The Public Safety Broadband Network: A Novel Architecture with Mobile Base Stations
Venue: arXiv cs.NI 2013
Year: 2013

A nationwide interoperable public safety broadband network is being planned by the United States government. The network will be based on long term evolution (LTE) standards and use recently designated spectrum in the 700 MHz band. The public safety network has different objectives and traffic patterns than commercial wireless networks. In particular, the public safety network puts more emphasis on coverage, reliability and latency in the worst case scenario. Moreover, the routine public safety traffic is relatively light, whereas when a major incident occurs, the traffic demand at the incident scene can be significantly heavier than that in a commercial network. Hence it is prohibitively costly to build the public safety network using conventional cellular network architecture consisting of an infrastructure of stationary base transceiver stations. A novel architecture is proposed in this paper for the public safety broadband network. The architecture deploys stationary base stations sparsely to serve light routine traffic and dispatches mobile base stations to incident scenes along with public safety personnel to support heavy traffic. The analysis shows that the proposed architecture can potentially offer more than 75% reduction in terms of the total number of base stations needed.
Subgraphs Satisfying MSO Properties on z-Topologically Orderable Digraphs
Venue: arXiv cs.CC 2013
Year: 2013

We introduce the notion of z-topological orderings for digraphs. We prove that given a digraph G on n vertices admitting a z-topological order- ing, together with such an ordering, one may count the number of subgraphs of G that at the same time satisfy a monadic second order formula ϕ and are the union of k directed paths, in time f (ϕ, k, z) * n^O(k*z) . Our result implies the polynomial time solvability of many natural counting problems on digraphs admitting z-topological orderings for constant values of z and k. Concerning the relationship between z-topological orderability and other digraph width measures, we observe that any digraph of directed path-width d has a z- topological ordering for z <= 2d + 1. On the other hand, there are digraphs on n vertices admitting a z-topological order for z = 2, but whose directed path-width is Θ(log n). Since graphs of bounded directed path-width can have both arbitrarily large undirected tree-width and arbitrarily large clique width, our result provides for the first time a suitable way of partially trans- posing metatheorems developed in the context of the monadic second order logic of graphs of constant undirected tree-width and constant clique width to the realm of digraph width measures that are closed under taking subgraphs and whose constant levels incorporate families of graphs of arbitrarily large undirected tree-width and arbitrarily large clique width.
Limited Attention and Centrality in Social Networks
Venue: arXiv cs.SI 2013
Year: 2013

How does one find important or influential people in an online social network? Researchers have proposed a variety of centrality measures to identify individuals that are, for example, often visited by a random walk, infected in an epidemic, or receive many messages from friends. Recent research suggests that a social media users' capacity to respond to an incoming message is constrained by their finite attention, which they divide over all incoming information, i.e., information sent by users they follow. We propose a new measure of centrality --- limited-attention version of Bonacich's Alpha-centrality --- that models the effect of limited attention on epidemic diffusion. The new measure describes a process in which nodes broadcast messages to their out-neighbors, but the neighbors' ability to receive the message depends on the number of in-neighbors they have. We evaluate the proposed measure on real-world online social networks and show that it can better reproduce an empirical influence ranking of users than other popular centrality measures.
Medical Process Modeling: an Artifact-Centric Approach
Venue: arXiv cs.OH 2013
Year: 2013

In this position paper we argue that just as traditional business process modeling has been adopted to deal with clinical pathways, also the artifact-centric process modeling technique may be successfully used to model various kinds of medical processes: physiological processes, disease behavior and treatment processes. We also discuss how a proposed approach may be used to deal with an interplay of all the processes a patient is subject to and what are the queries that might be imposed over an overall patient model.
Two Variable vs. Linear Temporal Logic in Model Checking and Games
Venue: arXiv cs.LO 2013
Year: 2013

Model checking linear-time properties expressed in first-order logic has non-elementary complexity, and thus various restricted logical languages are employed. In this paper we consider two such restricted specification logics, linear temporal logic (LTL) and two-variable first-order logic (FO2). LTL is more expressive but FO2 can be more succinct, and hence it is not clear which should be easier to verify. We take a comprehensive look at the issue, giving a comparison of verification problems for FO2, LTL, and various sublogics thereof across a wide range of models. In particular, we look at unary temporal logic (UTL), a subset of LTL that is expressively equivalent to FO2; we also consider the stutter-free fragment of FO2, obtained by omitting the successor relation, and the expressively equivalent fragment of UTL, obtained by omitting the next and previous connectives. We give three logic-to-automata translations which can be used to give upper bounds for FO2 and UTL and various sublogics. We apply these to get new bounds for both non-deterministic systems (hierarchical and recursive state machines, games) and for probabilistic systems (Markov chains, recursive Markov chains, and Markov decision processes). We couple these with matching lower-bound arguments. Next, we look at combining FO2 verification techniques with those for LTL. We present here a language that subsumes both FO2 and LTL, and inherits the model checking properties of both languages. Our results give both a unified approach to understanding the behaviour of FO2 and LTL, along with a nearly comprehensive picture of the complexity of verification for these logics and their sublogics.