OpenRaiser/Intern-Atlas huggingface dataset:
States in Process Calculi
Venue: arXiv cs.LO 2014
Year: 2014

Formal reasoning about distributed algorithms (like Consensus) typically requires to analyze global states in a traditional state-based style. This is in contrast to the traditional action-based reasoning of process calculi. Nevertheless, we use domain-specific variants of the latter, as they are convenient modeling languages in which the local code of processes can be programmed explicitly, with the local state information usually managed via parameter lists of process constants. However, domain-specific process calculi are often equipped with (unlabeled) reduction semantics, building upon a rich and convenient notion of structural congruence. Unfortunately, the price for this convenience is that the analysis is cumbersome: the set of reachable states is modulo structural congruence, and the processes' state information is very hard to identify. We extract from congruence classes of reachable states individual state-informative representatives that we supply with a proper formal semantics. As a result, we can now freely switch between the process calculus terms and their representatives, and we can use the stateful representatives to perform assertional reasoning on process calculus models.
Verification of Linear Optical Quantum Computing using Quantum Process Calculus
Venue: arXiv cs.LO 2014
Year: 2014

We explain the use of quantum process calculus to describe and analyse linear optical quantum computing (LOQC). The main idea is to define two processes, one modelling a linear optical system and the other expressing a specification, and prove that they are behaviourally equivalent. We extend the theory of behavioural equivalence in the process calculus Communicating Quantum Processes (CQP) to include multiple particles (namely photons) as information carriers, described by Fock states or number states. We summarise the theory in this paper, including the crucial result that equivalence is a congruence, meaning that it is preserved by embedding in any context. In previous work, we have used quantum process calculus to model LOQC but without verifying models against specifications. In this paper, for the first time, we are able to carry out verification. We illustrate this approach by describing and verifying two models of an LOQC CNOT gate.
Logarithmic-Time Updates and Queries in Probabilistic Networks
Venue: arXiv cs.AI 2014
Year: 2014

In this paper we propose a dynamic data structure that supports efficient algorithms for updating and querying singly connected Bayesian networks (causal trees and polytrees). In the conventional algorithms, new evidence in absorbed in time O(1) and queries are processed in time O(N), where N is the size of the network. We propose a practical algorithm which, after a preprocessing phase, allows us to answer queries in time O(log N) at the expense of O(logn N) time per evidence absorption. The usefulness of sub-linear processing time manifests itself in applications requiring (near) real-time response over large probabilistic databases.
Generalized Qualitative Probability: Savage Revisited
Venue: arXiv cs.AI 2014
Year: 2014

Preferences among acts are analyzed in the style of L. Savage, but as partially ordered. The rationality postulates considered are weaker than Savage's on three counts. The Sure Thing Principle is derived in this setting. The postulates are shown to lead to a characterization of generalized qualitative probability that includes and blends both traditional qualitative probability and the ranked structures used in logical approaches.
Complexity of Mechanism Design
Venue: arXiv cs.GT 2014
Year: 2014

The aggregation of conflicting preferences is a central problem in multiagent systems. The key difficulty is that the agents may report their preferences insincerely. Mechanism design is the art of designing the rules of the game so that the agents are motivated to report their preferences truthfully and a (socially) desirable outcome is chosen. We propose an approach where a mechanism is automatically created for the preference aggregation setting at hand. This has several advantages, but the downside is that the mechanism design optimization problem needs to be solved anew each time. Focusing on settings where side payments are not possible, we show that the mechanism design problem is NP-complete for deterministic mechanisms. This holds both for dominant-strategy implementation and for Bayes-Nash implementation. We then show that if we allow randomized mechanisms, the mechanism design problem becomes tractable. In other words, the coordinator can tackle the computational complexity introduced by its uncertainty about the agents preferences BY making the agents face additional uncertainty.This comes at no loss, AND IN SOME cases at a gain, IN the(social) objective.
Shifted inverse determinant sums and new bounds for the DMT of space-time lattice codes
Venue: arXiv cs.IT 2014
Year: 2014

This paper considers shifted inverse determinant sums arising from the union bound of the pairwise error probability for space-time codes in multiple-antenna fading channels. Previous work by Vehkalahti et al. focused on the approximation of these sums for low multiplexing gains, providing a complete classification of the inverse determinant sums as a function of constellation size for the most well-known algebraic space-time codes. This work aims at building a general framework for the study of the shifted sums for all multiplexing gains. New bounds obtained using dyadic summing techniques suggest that the behavior of the shifted sums does characterize many properties of a lattice code such as the diversity-multiplexing gain trade-off, both under maximum-likelihood decoding and infinite lattice naive decoding. Moreover, these bounds allow to characterize the signal-to-noise ratio thresholds corresponding to different diversity gains.
MacWilliams identities for poset level weight enumerators of linear codes
Venue: arXiv cs.IT 2014
Year: 2014

Codes over various metrics such as Rosenbloom-Tsfasman (RT), Lee, etc. have been considered. Recently, codes over poset metrics have been studied. Poset metric is a great generalization of many metrics especially the well-known ones such as the RT and the Hamming metrics. Poset metric can be realized on the channels with localized error occurrences. It has been shown that MacWilliams identities are not admissible for codes over poset metrics in general [Kim and Oh, 2005]. Lately, to overcome this problem some further studies on MacWilliams identities over poset metrics has been presented. In this paper, we introduce new poset level weight enumerators of linear codes over Frobenius commutative rings. We derive MacWilliams-type identities for each of the given enumerators which generalize in great deal the previous results discussed in the literature. Most of the weight enumerators in the literature such as Hamming, Rosenbloom-Tsfasman and complete m-spotty weight enumerators follow as corollaries to these identities especially.
An Abstract Formal Basis for Digital Crowds
Venue: arXiv cs.LO 2014
Year: 2014

Crowdsourcing, together with its related approaches, has become very popular in recent years. All crowdsourcing processes involve the participation of a digital crowd, a large number of people that access a single Internet platform or shared service. In this paper we explore the possibility of applying formal methods, typically used for the verification of software and hardware systems, in analysing the behaviour of a digital crowd. More precisely, we provide a formal description language for specifying digital crowds. We represent digital crowds in which the agents do not directly communicate with each other. We further show how this specification can provide the basis for sophisticated formal methods, in particular formal verification.
Parallel Distributed Breadth First Search on the Kepler Architecture
Venue: arXiv cs.DC 2014
Year: 2014

We present the results obtained by using an evolution of our CUDA-based solution for the exploration, via a Breadth First Search, of large graphs. This latest version exploits at its best the features of the Kepler architecture and relies on a combination of techniques to reduce both the number of communications among the GPUs and the amount of exchanged data. The final result is a code that can visit more than 800 billion edges in a second by using a cluster equipped with 4096 Tesla K20X GPUs.
Computing consensus: A logic for reasoning about deliberative processes based on argumentation
Venue: arXiv cs.LO 2014
Year: 2014

We consider multi-agent argumentation, where each agent's view of the arguments is encoded as an argumentation framework (AF). Then we study deliberative processes than can occur on this basis. We think of a deliberative process as taking the shape of a stepwise aggregation of a single joint AF, and we are interested in reasoning about the space of possible outcomes. The only restriction we place on deliberative processes is that they should satisfy faithfulness, a postulate amounting to requiring that whenever deliberation leads to a new relationship being introduced between two arguments, this relationship is endorsed by at least one participating agent. We use modal logic to reason about the resulting deliberative structures, and we provide some technical results on model checking. We also give an example and suggest some directions for future work.
Computing the log-determinant of symmetric, diagonally dominant matrices in near-linear time
Venue: arXiv cs.NA 2014
Year: 2014

We present new algorithms for computing the log-determinant of symmetric, diagonally dominant matrices. Existing algorithms run with cubic complexity with respect to the size of the matrix in the worst case. Our algorithm computes an approximation of the log-determinant in time near-linear with respect to the number of non-zero entries and with high probability. This algorithm builds upon the utra-sparsifiers introduced by Spielman and Teng for Laplacian matrices and ultimately uses their refined versions introduced by Koutis, Miller and Peng in the context of solving linear systems. We also present simpler algorithms that compute upper and lower bounds and that may be of more immediate practical interest.
Context-awareness of the IoT through the on-the-fly preference modeling
Venue: arXiv cs.SE 2014
Year: 2014

The context-awareness of things that belong to IoT networks have to be considered in a distributed computation paradigm. In the paper we suggest the use of graph transformations and temporal logic as a formal framework for a knowledge representation of user/inhabitant behaviors in multi-agent systems. IoT networks are considered as graph structures. Dynamic preference models, understood as a priority in the selecting, is also introduced. Preference models as a result of observed behaviors base on formal logic, and they are built on-the-fly by software agents. Software agents gather knowledge about user preferences expressed in terms of logical specifications as well as suggest on-the-fly future behavior basing on the logical inference process using the semantic tableaux method. The predictive processes are result of some new and important events in the context of IoT systems that should meet a response. Due to the ubiquitous availability of cyber systems that interact with physical environments, there is a great need to develop technologies that target the whole IoT system as a context-awareness system. Formal approach increases the trustworthy of a system. A simple yet illustrative example is provided.
Limits on the performance of Infotaxis under inaccurate modelling of the environment
Venue: arXiv cs.ET 2014
Year: 2014

We study the performance of infotaxis search strategy measured by the rate of success and mean search time, under changes in the environment parameters such as diffusivity, rate of emission or wind velocity. We also investigate the drop of performance caused by an innacurate modelling of the environment. Our findings show that infotaxis remains robust as long as the estimated parameters fall within a certain range around their true values, but the success rate quickly drops making infotaxis no longer feasible if the searcher agent severely underestimates or overestimates the real environment parameters. This study places some limits on the performance of infotaxis, and thus it has practical consequences for the design of infotaxis based machines to track and detect an emitting source of chemicals or volatile substances.
Applying Spiking Neural Nets to Noise Shaping
Venue: arXiv cs.ET 2014
Year: 2014

-In recent years, there has been an increased focus on the mechanics of information transmission in spiking neural networks. Especially the Noise Shaping properties of these networks and their similarity to Delta-Sigma Modulators has received a lot of attention. However, very little of the research done in this area has focused on the effect the weights in these networks have on the Noise Shaping properties and on post- processing of the network output signal. This paper concerns itself with the various modes of network operation and beneficial as well as detrimental effects which the systematic generation of network weights can effect. Also, a method for post-processing of the spiking output signal is introduced, bringing the output signal more in line with conventional Delta-Sigma Modulators. Relevancy of this research to industrial application of neural nets as building blocks of oversampled A/D converters is shown. Also, further points of contention are listed, which must be thoroughly researched to add to the above mentioned applicability of spiking neural nets.
Neighborhood Rank Order Coding for Robust Texture Analysis and Feature Extraction
Venue: arXiv cs.CV 2014
Year: 2014

Research into the visual cortex and general neural information processing has led to various attempts to integrate pulse computation schemes in image analysis systems. Of interest is especially the robustness of representing an analogue signal in the phase or duration of a pulsed, quasi-digital signal, as well as the possibility of direct digital interaction, i.e. computation, among these signals. Such a computation can also achieve information compaction for subsequent processing stages. By using a pulse order encoding scheme motivated by dendritic pulse interaction, we will show that a powerful low-level feature and texture extraction operator, called Pulsed Local Orientation Coding (PLOC), can be implemented. Feature extraction results are being presented, and a possible VLSI implementation is detailed.
Capacity and Error Rate Analysis of MIMO Satellite Communication Systems in Fading Scenarios
Venue: arXiv cs.IT 2014
Year: 2014

In this paper, we investigated the capacity and bit error rate (BER) performance of Multiple Input Multiple Output (MIMO) satellite systems with single and multiple dual polarized satellites in geostationary orbit and a mobile ground receiving station with multiple antennas. We evaluated the effects of both system parameters such as number of satellites, number of receive antennas, and SNR and environmental factors including atmospheric signal attenuations and signal phase disturbances on the overall system performance using both analytical and spatial models for MIMO satellite systems.
A Heuristic Search Algorithm for Solving First-Order MDPs
Venue: arXiv cs.AI 2014
Year: 2014

We present a heuristic search algorithm for solving first-order MDPs (FOMDPs). Our approach combines first-order state abstraction that avoids evaluating states individually, and heuristic search that avoids evaluating all states. Firstly, we apply state abstraction directly on the FOMDP avoiding propositionalization. Such kind of abstraction is referred to as firstorder state abstraction. Secondly, guided by an admissible heuristic, the search is restricted only to those states that are reachable from the initial state. We demonstrate the usefullness of the above techniques for solving FOMDPs on a system, referred to as FCPlanner, that entered the probabilistic track of the International Planning Competition (IPC'2004).
On the Conditional Independence Implication Problem: A Lattice-Theoretic Approach
Venue: arXiv cs.AI 2014
Year: 2014

A lattice-theoretic framework is introduced that permits the study of the conditional independence (CI) implication problem relative to the class of discrete probability measures. Semi-lattices are associated with CI statements and a finite, sound and complete inference system relative to semi-lattice inclusions is presented. This system is shown to be (1) sound and complete for saturated CI statements, (2) complete for general CI statements, and (3) sound and complete for stable CI statements. These results yield a criterion that can be used to falsify instances of the implication problem and several heuristics are derived that approximate this "lattice-exclusion" criterion in polynomial time. Finally, we provide experimental results that relate our work to results obtained from other existing inference algorithms.
Conditional Probability Tree Estimation Analysis and Algorithms
Venue: arXiv cs.LG 2014
Year: 2014

We consider the problem of estimating the conditional probability of a label in time O(log n), where n is the number of possible labels. We analyze a natural reduction of this problem to a set of binary regression problems organized in a tree structure, proving a regret bound that scales with the depth of the tree. Motivated by this analysis, we propose the first online algorithm which provably constructs a logarithmic depth tree on the set of labels to solve this problem. We test the algorithm empirically, showing that it works succesfully on a dataset with roughly 106 labels.
Approximate inference on planar graphs using Loop Calculus and Belief Propagation
Venue: arXiv cs.AI 2014
Year: 2014

We introduce novel results for approximate inference on planar graphical models using the loop calculus framework. The loop calculus (Chertkov and Chernyak, 2006b) allows to express the exact partition function Z of a graphical model as a finite sum of terms that can be evaluated once the belief propagation (BP) solution is known. In general, full summation over all correction terms is intractable. We develop an algorithm for the approach presented in Chertkov et al. (2008) which represents an efficient truncation scheme on planar graphs and a new representation of the series in terms of Pfaffians of matrices. We analyze in detail both the loop series and the Pfaffian series for models with binary variables and pairwise interactions, and show that the first term of the Pfaffian series can provide very accurate approximations. The algorithm outperforms previous truncation schemes of the loop series and is competitive with other state-of-the-art methods for approximate inference.
Quantum Annealing for Clustering
Venue: arXiv cs.AI 2014
Year: 2014

This paper studies quantum annealing (QA) for clustering, which can be seen as an extension of simulated annealing (SA). We derive a QA algorithm for clustering and propose an annealing schedule, which is crucial in practice. Experiments show the proposed QA algorithm finds better clustering assignments than SA. Furthermore, QA is as easy as SA to implement.
Gaussian Process Structural Equation Models with Latent Variables
Venue: arXiv cs.LG 2014
Year: 2014

In a variety of disciplines such as social sciences, psychology, medicine and economics, the recorded data are considered to be noisy measurements of latent variables connected by some causal structure. This corresponds to a family of graphical models known as the structural equation model with latent variables. While linear non-Gaussian variants have been well-studied, inference in nonparametric structural equation models is still underdeveloped. We introduce a sparse Gaussian process parameterization that defines a non-linear structure connecting latent variables, unlike common formulations of Gaussian process latent variable models. The sparse parameterization is given a full Bayesian treatment without compromising Markov chain Monte Carlo efficiency. We compare the stability of the sampling procedure and the predictive ability of the model against the current practice.
Markov Chains on Orbits of Permutation Groups
Venue: arXiv cs.AI 2014
Year: 2014

We present a novel approach to detecting and utilizing symmetries in probabilistic graphical models with two main contributions. First, we present a scalable approach to computing generating sets of permutation groups representing the symmetries of graphical models. Second, we introduce orbital Markov chains, a novel family of Markov chains leveraging model symmetries to reduce mixing times. We establish an insightful connection between model symmetries and rapid mixing of orbital Markov chains. Thus, we present the first lifted MCMC algorithm for probabilistic graphical models. Both analytical and empirical results demonstrate the effectiveness and efficiency of the approach.
Guess Who Rated This Movie: Identifying Users Through Subspace Clustering
Venue: arXiv cs.LG 2014
Year: 2014

It is often the case that, within an online recommender system, multiple users share a common account. Can such shared accounts be identified solely on the basis of the userprovided ratings? Once a shared account is identified, can the different users sharing it be identified as well? Whenever such user identification is feasible, it opens the way to possible improvements in personalized recommendations, but also raises privacy concerns. We develop a model for composite accounts based on unions of linear subspaces, and use subspace clustering for carrying out the identification task. We show that a significant fraction of such accounts is identifiable in a reliable manner, and illustrate potential uses for personalized recommendation.
Active Sensing as Bayes-Optimal Sequential Decision Making
Venue: arXiv cs.AI 2014
Year: 2014

Sensory inference under conditions of uncertainty is a major problem in both machine learning and computational neuroscience. An important but poorly understood aspect of sensory processing is the role of active sensing. Here, we present a Bayes-optimal inference and control framework for active sensing, C-DAC (Context-Dependent Active Controller). Unlike previously proposed algorithms that optimize abstract statistical objectives such as information maximization (Infomax) [Butko & Movellan, 2010] or one-step look-ahead accuracy [Najemnik & Geisler, 2005], our active sensing model directly minimizes a combination of behavioral costs, such as temporal delay, response error, and effort. We simulate these algorithms on a simple visual search task to illustrate scenarios in which context-sensitivity is particularly beneficial and optimization with respect to generic statistical objectives particularly inadequate. Motivated by the geometric properties of the C-DAC policy, we present both parametric and non-parametric approximations, which retain context-sensitivity while significantly reducing computational complexity. These approximations enable us to investigate the more complex problem involving peripheral vision, and we notice that the difference between C-DAC and statistical policies becomes even more evident in this scenario.