OpenRaiser/Intern-Atlas huggingface dataset:
Model Checking for Modal Dependence Logic: An Approach Through Post's Lattice
Venue: arXiv cs.CC 2013
Year: 2013

In this paper we investigate an extended version of modal dependence logic by allowing arbitrary Boolean connectives. Modal dependence logic was recently introduced by Jouko Väänänen by extending modal logic by a the dependence atom dep(.). In this paper we study the computational complexity of the model checking problem. For a complete classification of arbitrary Boolean functions we are using a Lattice approach introduced by Emil Post. This classification is done for all fragments of the logical language allowing modalities $\Diamond$ and $\Box$, the dependence atom, and logical symbols for arbitrary Boolean functions.
Anatomy of the chase
Venue: arXiv cs.DB 2013
Year: 2013

A lot of research activity has recently taken place around the chase procedure, due to its usefulness in data integration, data exchange, query optimization, peer data exchange and data correspondence, to mention a few. As the chase has been investigated and further developed by a number of research groups and authors, many variants of the chase have emerged and associated results obtained. Due to the heterogeneous nature of the area it is frequently difficult to verify the scope of each result. In this paper we take closer look at recent developments, and provide additional results. Our analysis allows us create a taxonomy of the chase variations and the properties they satisfy. Two of the most central problems regarding the chase is termination, and discovery of restricted classes of sets of dependencies that guarantee termination of the chase. The search for the restricted classes has been motivated by a fairly recent result that shows that it is undecidable to determine whether the chase with a given dependency set will terminate on a given instance. There is a small dissonance here, since the quest has been for classes of sets of dependencies guaranteeing termination of the chase on all instances, even though the latter problem was not known to be undecidable. We resolve the dissonance in this paper by showing that determining whether the chase with a given set of dependencies terminates on all instances is coRE-complete. Our reduction also gives us the aforementioned instance-dependent RE-completeness result as a byproduct. For one of the restricted classes, the stratified sets dependencies, we provide new complexity results for the problem of testing whether a given set of dependencies belongs to it. These results rectify some previous claims that have occurred in the literature.
An intelligent approach towards automatic shape modeling and object extraction from satellite images using cellular automata based algorithm
Venue: arXiv cs.CV 2013
Year: 2013

Automatic feature extraction domain has witnessed the application of many intelligent methodologies over past decade; however detection accuracy of these approaches were limited as object geometry and contextual knowledge were not given enough consideration. In this paper, we propose a frame work for accurate detection of features along with automatic interpolation, and interpretation by modeling feature shape as well as contextual knowledge using advanced techniques such as SVRF, Cellular Neural Network, Core set, and MACA. Developed methodology has been compared with contemporary methods using different statistical measures. Investigations over various satellite images revealed that considerable success was achieved with the CNN approach. CNN has been effective in modeling different complex features effectively and complexity of the approach has been considerably reduced using corset optimization. The system has dynamically used spectral and spatial information for representing contextual knowledge using CNN-prolog approach. System has been also proved to be effective in providing intelligent interpolation and interpretation of random features.
Blind Identification of ARX Models with Piecewise Constant Inputs
Venue: arXiv cs.SY 2013
Year: 2013

Blind system identification is known to be a hard ill-posed problem and without further assumptions, no unique solution is at hand. In this contribution, we are concerned with the task of identifying an ARX model from only output measurements. Driven by the task of identifying systems that are turned on and off at unknown times, we seek a piecewise constant input and a corresponding ARX model which approximates the measured outputs. We phrase this as a rank minimization problem and present a relaxed convex formulation to approximate its solution. The proposed method was developed to model power consumption of electrical appliances and is now a part of a bigger energy disaggregation framework. Code will be made available online.
Improved Lower Bounds for Sum Coloring via Clique Decomposition
Venue: arXiv cs.DM 2013
Year: 2013

Given an undirected graph $G = (V,E)$ with a set $V$ of vertices and a set $E$ of edges, the minimum sum coloring problem (MSCP) is to find a legal vertex coloring of $G$, using colors represented by natural numbers $1, 2, . . .$ such that the total sum of the colors assigned to the vertices is minimized. This paper describes an approach based on the decomposition of the original graph into disjoint cliques for computing lower bounds for the MSCP. Basically, the proposed approach identifies and removes at each extraction iteration a maximum number of cliques of the same size (the largest possible) from the graph. Computational experiments show that this approach is able to improve on the current best lower bounds for 14 benchmark instances, and to prove optimality for the first time for 4 instances. We also report lower bounds for 24 more instances for which no such bounds are available in the literature. These new lower bounds are useful to estimate the quality of the upper bounds obtained with various heuristic approaches.
A Comparative Analysis on the Applicability of Entropy in remote sensing
Venue: arXiv cs.CV 2013
Year: 2013

Entropy is the measure of uncertainty in any data and is adopted for maximisation of mutual information in many remote sensing operations. The availability of wide entropy variations motivated us for an investigation over the suitability preference of these versions to specific operations. Methodologies were implemented in Matlab and were enhanced with entropy variations. Evaluation of various implementations was based on different statistical parameters with reference to the study area The popular available versions like Tsalli's, Shanon's, and Renyi's entropies were analysed in context of various remote sensing operations namely thresholding, clustering and registration.
Parameterized Complexity of Discrete Morse Theory
Venue: arXiv cs.CG 2013
Year: 2013

Optimal Morse matchings reveal essential structures of cell complexes which lead to powerful tools to study discrete geometrical objects, in particular discrete 3-manifolds. However, such matchings are known to be NP-hard to compute on 3-manifolds, through a reduction to the erasability problem. Here, we refine the study of the complexity of problems related to discrete Morse theory in terms of parameterized complexity. On the one hand we prove that the erasability problem is W[P]-complete on the natural parameter. On the other hand we propose an algorithm for computing optimal Morse matchings on triangulations of 3-manifolds which is fixed-parameter tractable in the treewidth of the bipartite graph representing the adjacency of the 1- and 2-simplexes. This algorithm also shows fixed parameter tractability for problems such as erasability and maximum alternating cycle-free matching. We further show that these results are also true when the treewidth of the dual graph of the triangulated 3-manifold is bounded. Finally, we investigate the respective treewidths of simplicial and generalized triangulations of 3-manifolds.
On the speed of constraint propagation and the time complexity of arc consistency testing
Venue: arXiv cs.LO 2013
Year: 2013

Establishing arc consistency on two relational structures is one of the most popular heuristics for the constraint satisfaction problem. We aim at determining the time complexity of arc consistency testing. The input structures $G$ and $H$ can be supposed to be connected colored graphs, as the general problem reduces to this particular case. We first observe the upper bound $O(e(G)v(H)+v(G)e(H))$, which implies the bound $O(e(G)e(H))$ in terms of the number of edges and the bound $O((v(G)+v(H))^3)$ in terms of the number of vertices. We then show that both bounds are tight up to a constant factor as long as an arc consistency algorithm is based on constraint propagation (like any algorithm currently known). Our argument for the lower bounds is based on examples of slow constraint propagation. We measure the speed of constraint propagation observed on a pair $G,H$ by the size of a proof, in a natural combinatorial proof system, that Spoiler wins the existential 2-pebble game on $G,H$. The proof size is bounded from below by the game length $D(G,H)$, and a crucial ingredient of our analysis is the existence of $G,H$ with $D(G,H)=Ω(v(G)v(H))$. We find one such example among old benchmark instances for the arc consistency problem and also suggest a new, different construction.
Semantic Matching of Security Policies to Support Security Experts
Venue: arXiv cs.CR 2013
Year: 2013

Management of security policies has become increasingly difficult given the number of domains to manage, taken into consideration their extent and their complexity. Security experts has to deal with a variety of frameworks and specification languages used in different domains that may belong to any Cloud Computing or Distributed Systems. This wealth of frameworks and languages make the management task and the interpretation of the security policies so difficult. Each approach provides its own conflict management method or tool, the security expert will be forced to manage all these tools, which makes the field maintenance and time consuming expensive. In order to hide this complexity and to facilitate some security experts tasks and automate the others, we propose a security policies aligning based on ontologies process; this process enables to detect and resolve security policies conflicts and to support security experts in managing tasks.
Decentralized Eigenvalue Algorithms for Distributed Signal Detection in Cognitive Networks
Venue: arXiv cs.DC 2013
Year: 2013

In this paper we derive and analyze two algorithms -- referred to as decentralized power method (DPM) and decentralized Lanczos algorithm (DLA) -- for distributed computation of one (the largest) or multiple eigenvalues of a sample covariance matrix over a wireless network. The proposed algorithms, based on sequential average consensus steps for computations of matrix-vector products and inner vector products, are first shown to be equivalent to their centralized counterparts in the case of exact distributed consensus. Then, closed-form expressions of the error introduced by non-ideal consensus are derived for both algorithms. The error of the DPM is shown to vanish asymptotically under given conditions on the sequence of consensus errors. Finally, we consider applications to spectrum sensing in cognitive radio networks, and we show that virtually all eigenvalue-based tests proposed in the literature can be implemented in a distributed setting using either the DPM or the DLA. Simulation results are presented that validate the effectiveness of the proposed algorithms in conditions of practical interest (large-scale networks, small number of samples, and limited number of iterations).
On the Complexity of the Decisive Problem in Simple, Regular and Weighted Games
Venue: arXiv cs.GT 2013
Year: 2013

We study the computational complexity of an important property of simple, regular and weighted games, which is decisiveness. We show that this concept can naturally be represented in the context of hypergraph theory, and that decisiveness can be decided for simple games in quasi-polynomial time, and for regular and weighted games in polynomial time. The strongness condition poses the main difficulties, while properness reduces the complexity of the problem, especially if it is amplified by regularity. On the other hand, regularity also allows to specify the problem instances much more economically, implying a reconsideration of the corresponding complexity measure that, as we prove, has important structural as well as algorithmic consequences.
A rigorous geometry-probability equivalence in characterization of $\ell_1$-optimization
Venue: arXiv cs.IT 2013
Year: 2013

In this paper we consider under-determined systems of linear equations that have sparse solutions. This subject attracted enormous amount of interest in recent years primarily due to influential works \cite{CRT,DonohoPol}. In a statistical context it was rigorously established for the first time in \cite{CRT,DonohoPol} that if the number of equations is smaller than but still linearly proportional to the number of unknowns then a sparse vector of sparsity also linearly proportional to the number of unknowns can be recovered through a polynomial $\ell_1$-optimization algorithm (of course, this assuming that such a sparse solution vector exists). Moreover, the geometric approach of \cite{DonohoPol} produced the exact values for the proportionalities in question. In our recent work \cite{StojnicCSetam09} we introduced an alternative statistical approach that produced attainable values of the proportionalities. Those happened to be in an excellent numerical agreement with the ones of \cite{DonohoPol}. In this paper we give a rigorous analytical confirmation that the results of \cite{StojnicCSetam09} indeed match those from \cite{DonohoPol}.
Exploring the Role of Logically Related Non-Question Phrases for Answering Why-Questions
Venue: arXiv cs.CL 2013
Year: 2013

In this paper, we show that certain phrases although not present in a given question/query, play a very important role in answering the question. Exploring the role of such phrases in answering questions not only reduces the dependency on matching question phrases for extracting answers, but also improves the quality of the extracted answers. Here matching question phrases means phrases which co-occur in given question and candidate answers. To achieve the above discussed goal, we introduce a bigram-based word graph model populated with semantic and topical relatedness of terms in the given document. Next, we apply an improved version of ranking with a prior-based approach, which ranks all words in the candidate document with respect to a set of root words (i.e. non-stopwords present in the question and in the candidate document). As a result, terms logically related to the root words are scored higher than terms that are not related to the root words. Experimental results show that our devised system performs better than state-of-the-art for the task of answering Why-questions.
The untyped stack calculus and Bohm's theorem
Venue: arXiv cs.LO 2013
Year: 2013

The stack calculus is a functional language in which is in a Curry-Howard correspondence with classical logic. It enjoys confluence but, as well as Parigot's lambda-mu, does not admit the Bohm Theorem, typical of the lambda-calculus. We present a simple extension of stack calculus which is for the stack calculus what Saurin's Lambda-mu is for lambda-mu.
The stack calculus
Venue: arXiv cs.LO 2013
Year: 2013

We introduce a functional calculus with simple syntax and operational semantics in which the calculi introduced so far in the Curry-Howard correspondence for Classical Logic can be faithfully encoded. Our calculus enjoys confluence without any restriction. Its type system enforces strong normalization of expressions and it is a sound and complete system for full implicational Classical Logic. We give a very simple denotational semantics which allows easy calculations of the interpretation of expressions.
Control Explicit---Data Symbolic Model Checking: An Introduction
Venue: arXiv cs.SE 2013
Year: 2013

A comprehensive verification of parallel software imposes three crucial requirements on the procedure that implements it. Apart from accepting real code as program input and temporal formulae as specification input, the verification should be exhaustive, with respect to both control and data flows. This paper is concerned with the third requirement, proposing to combine explicit model checking to handle the control with symbolic set representations to handle the data. The combination of explicit and symbolic approaches is first investigated theoretically and we report the requirements on the symbolic representation and the changes to the model checking process the combination entails. The feasibility and efficiency of the combination is demonstrated on a case study using the DVE modelling language and we report a marked improvement in scalability compared to previous solutions. The results described in this paper show the potential to meet all three requirements for automatic verification in a single procedure combining explicit model checking with symbolic set representations.
Geometric tree kernels: Classification of COPD from airway tree geometry
Venue: arXiv cs.CV 2013
Year: 2013

Methodological contributions: This paper introduces a family of kernels for analyzing (anatomical) trees endowed with vector valued measurements made along the tree. While state-of-the-art graph and tree kernels use combinatorial tree/graph structure with discrete node and edge labels, the kernels presented in this paper can include geometric information such as branch shape, branch radius or other vector valued properties. In addition to being flexible in their ability to model different types of attributes, the presented kernels are computationally efficient and some of them can easily be computed for large datasets (N of the order 10.000) of trees with 30-600 branches. Combining the kernels with standard machine learning tools enables us to analyze the relation between disease and anatomical tree structure and geometry. Experimental results: The kernels are used to compare airway trees segmented from low-dose CT, endowed with branch shape descriptors and airway wall area percentage measurements made along the tree. Using kernelized hypothesis testing we show that the geometric airway trees are significantly differently distributed in patients with Chronic Obstructive Pulmonary Disease (COPD) than in healthy individuals. The geometric tree kernels also give a significant increase in the classification accuracy of COPD from geometric tree structure endowed with airway wall thickness measurements in comparison with state-of-the-art methods, giving further insight into the relationship between airway wall thickness and COPD. Software: Software for computing kernels and statistical tests is available at http://image.diku.dk/aasa/software.php.
Agent-based modeling of a price information trading business
Venue: arXiv cs.AI 2013
Year: 2013

We describe an agent-based simulation of a fictional (but feasible) information trading business. The Gas Price Information Trader (GPIT) buys information about real-time gas prices in a metropolitan area from drivers and resells the information to drivers who need to refuel their vehicles. Our simulation uses real world geographic data, lifestyle-dependent driving patterns and vehicle models to create an agent-based model of the drivers. We use real world statistics of gas price fluctuation to create scenarios of temporal and spatial distribution of gas prices. The price of the information is determined on a case-by-case basis through a simple negotiation model. The trader and the customers are adapting their negotiation strategies based on their historical profits. We are interested in the general properties of the emerging information market: the amount of realizable profit and its distribution between the trader and customers, the business strategies necessary to keep the market operational (such as promotional deals), the price elasticity of demand and the impact of pricing strategies on the profit.
Independent Vector Analysis: Identification Conditions and Performance Bounds
Venue: arXiv cs.LG 2013
Year: 2013

Recently, an extension of independent component analysis (ICA) from one to multiple datasets, termed independent vector analysis (IVA), has been the subject of significant research interest. IVA has also been shown to be a generalization of Hotelling's canonical correlation analysis. In this paper, we provide the identification conditions for a general IVA formulation, which accounts for linear, nonlinear, and sample-to-sample dependencies. The identification conditions are a generalization of previous results for ICA and for IVA when samples are independently and identically distributed. Furthermore, a principal aim of IVA is the identification of dependent sources between datasets. Thus, we provide the additional conditions for when the arbitrary ordering of the sources within each dataset is common. Performance bounds in terms of the Cramer-Rao lower bound are also provided for the demixing matrices and interference to source ratio. The performance of two IVA algorithms are compared to the theoretical bounds.
Statistical inference framework for source detection of contagion processes on arbitrary network structures
Venue: arXiv cs.SI 2013
Year: 2013

In this paper we introduce a statistical inference framework for estimating the contagion source from a partially observed contagion spreading process on an arbitrary network structure. The framework is based on a maximum likelihood estimation of a partial epidemic realization and involves large scale simulation of contagion spreading processes from the set of potential source locations. We present a number of different likelihood estimators that are used to determine the conditional probabilities associated to observing partial epidemic realization with particular source location candidates. This statistical inference framework is also applicable for arbitrary compartment contagion spreading processes on networks. We compare estimation accuracy of these approaches in a number of computational experiments performed with the SIR (susceptible-infected-recovered), SI (susceptible-infected) and ISS (ignorant-spreading-stifler) contagion spreading models on synthetic and real-world complex networks.
A Neuromorphic VLSI Design for Spike Timing and Rate Based Synaptic Plasticity
Venue: arXiv cs.NE 2013
Year: 2013

Triplet-based Spike Timing Dependent Plasticity (TSTDP) is a powerful synaptic plasticity rule that acts beyond conventional pair-based STDP (PSTDP). Here, the TSTDP is capable of reproducing the outcomes from a variety of biological experiments, while the PSTDP rule fails to reproduce them. Additionally, it has been shown that the behaviour inherent to the spike rate-based Bienenstock-Cooper-Munro (BCM) synaptic plasticity rule can also emerge from the TSTDP rule. This paper proposes an analog implementation of the TSTDP rule. The proposed VLSI circuit has been designed using the AMS 0.35 um CMOS process and has been simulated using design kits for Synopsys and Cadence tools. Simulation results demonstrate how well the proposed circuit can alter synaptic weights according to the timing difference amongst a set of different patterns of spikes. Furthermore, the circuit is shown to give rise to a BCM-like learning rule, which is a rate-based rule. To mimic implementation environment, a 1000 run Monte Carlo (MC) analysis was conducted on the proposed circuit. The presented MC simulation analysis and the simulation result from fine-tuned circuits show that, it is possible to mitigate the effect of process variations in the proof of concept circuit, however, a practical variation aware design technique is required to promise a high circuit performance in a large scale neural network. We believe that the proposed design can play a significant role in future VLSI implementations of both spike timing and rate based neuromorphic learning systems.