OpenRaiser/Intern-Atlas huggingface dataset:
On distributed monitoring of asynchronous systems
Venue: arXiv cs.FL 2012
Year: 2012

Distributed systems are notoriously difficult to understand and analyze in order to assert their correction w.r.t. given properties. They often exhibit a huge number of different behaviors, as soon as the active entities (peers, agents, processes, etc) behave in an asynchronous manner. Already the modelization of such systems is a non-trivial task, let alone their formal verification. The purpose of this paper is to discuss the problem of distributed monitoring on a simple model of finite-state distributed automata based on shared actions, called asynchronous automata. Monitoring is a question related to runtime verification: assume that we have to check a property $L$ against an unknown or very complex system $A$, so that classical static analysis is not possible. Therefore instead of model-checking a monitor is used, that checks the property on the underlying system at runtime. We are interested here in monitoring distributed systems modeled as asynchronous automata. It is natural to require that monitors should be of the same kind as the underlying system, so we consider here distributed monitoring. A distributed monitor does not have a global view of the system, therefore we propose the notion of locally monitorable trace language. Our main result shows that if the distributed alphabet of actions is connected and if $L$ is a set of infinite traces such that both $L$ and its complement $L^c$ are countable unions of locally safety languages, then $L$ is locally monitorable. We also show that over infinite traces, recognizable countable unions of locally safety languages are precisely the complements of deterministic languages.
Blind Channel Equalization
Venue: arXiv cs.IT 2012
Year: 2012

Future services demand high data rate and quality. Thus, it is necessary to define new and robust algorithms to equalize channels and reduce noise in communications. Nowadays, new equalization algorithms are being developed to optimize the channel bandwidth and reduce noise, namely, Blind Channel Equalization. Conventional equalizations minimizing mean-square error generally require a training sequence accompanying the data sequence. In this study, the result of Least Mean Square (LMS) algorithm applied on two given communication channels is analyzed. Considering the fact that blind equalizers do not require pilot signals to recover the transmitted data, implementation of four types of Constant Modulus Algorithm (CMA) for blind equalization of the channels are shown. Finally, a comparison of the simulation results of LMS and CMA for the test channels is provided.
Stochastic Kronecker Graph on Vertex-Centric BSP
Venue: arXiv cs.SI 2012
Year: 2012

Recently Stochastic Kronecker Graph (SKG), a network generation model, and vertex-centric BSP, a graph processing framework like Pregel, have attracted much attention in the network analysis community. Unfortunately the two are not very well-suited for each other and thus an implementation of SKG on vertex-centric BSP must either be done serially or in an unnatural manner. In this paper, we present a new network generation model, which we call Poisson Stochastic Kronecker Graph (PSKG), that generate edges according to the Poisson distribution. The advantage of PSKG is that it is easily parallelizable on vertex-centric BSP, requires no communication between computational nodes, and yet retains all the desired properties of SKG.
A New Direction for Counting Perfect Matchings
Venue: arXiv cs.DS 2012
Year: 2012

In this paper, we present a new exact algorithm for counting perfect matchings, which relies on neither inclusion-exclusion principle nor tree-decompositions. For any bipartite graph of $2n$ nodes and $Δn$ edges such that $Δ\geq 3$, our algorithm runs with $O^{\ast}(2^{(1 - 1/O(Δ\log Δ))n})$ time and exponential space. Compared to the previous algorithms, it achieves a better time bound in the sense that the performance degradation to the increase of $Δ$ is quite slower. The main idea of our algorithm is a new reduction to the problem of computing the cut-weight distribution of the input graph. The primary ingredient of this reduction is MacWilliams Identity derived from elementary coding theory. The whole of our algorithm is designed by combining that reduction with a non-trivial fast algorithm computing the cut-weight distribution. To the best of our knowledge, the approach posed in this paper is new and may be of independent interest.
Instantly Decodable versus Random Linear Network Coding: A Comparative Framework for Throughput and Decoding Delay Performance
Venue: arXiv cs.IT 2012
Year: 2012

This paper studies the tension between throughput and decoding delay performance of two widely-used network coding schemes: random linear network coding (RLNC) and instantly decodable network coding (IDNC). A single-hop broadcasting system model is considered that aims to deliver a block of packets to all receivers in the presence of packet erasures. For a fair and analytically tractable comparison between the two coding schemes, the transmission comprises two phases: a systematic transmission phase and a network coded transmission phase which is further divided into rounds. After the systematic transmission phase and given the same packet reception state, three quantitative metrics are proposed and derived in each scheme: 1) the absolute minimum number of transmissions in the first coded transmission round (assuming no erasures), 2) probability distribution of extra coded transmissions in a subsequent round (due to erasures), and 3) average packet decoding delay. This comparative study enables application-aware adaptive selection between IDNC and RLNC after systematic transmission phase. One contribution of this paper is to provide a deep and systematic understanding of the IDNC scheme, to propose the notion of packet diversity and an optimal IDNC encoding scheme for minimizing metric 1. This is generally NP-hard, but nevertheless required for characterizing and deriving all the three metrics. Analytical and numerical results show that there is no clear winner between RLNC and IDNC if one is concerned with both throughput and decoding delay performance. IDNC is more preferable than RLNC when the number of receivers is smaller than packet block size, and the case reverses when the number of receivers is much greater than the packet block size. In the middle regime, the choice can depend on the application and a specific instance of the problem.
Linear model predictive control based on polyhedral control Lyapunov functions: theory and applications
Venue: arXiv cs.SY 2012
Year: 2012

Polyhedral control Lyapunov functions (PCLFs) are exploited in finite-horizon linear model predictive control formulations in order to guarantee the maximal domain of attraction (DoA), in contrast to traditional formulations based on quadratic control Lyapunov functions. In particular, the terminal region is chosen as the largest DoA, namely the entire controllable set, which is parametrized by a level set of a suitable PCLF. Closed-loop stability of the origin is guaranteed either by using an "inflated" PCLF as terminal cost or by adding a contraction constraint for the PCLF evaluated at the current state. Two variants of the formulation based on the inflated PCLF terminal cost are also presented. In all proposed formulations, the guaranteed DoA is always the entire controllable set, independently of the chosen finite horizon. Closed-loop inherent robustness with respect to arbitrary, sufficiently small perturbations is also established. Moreover, all proposed schemes can be formulated as Quadratic Programming problems. Numerical examples show the main benefits and achievements of the proposed formulations.
Path Integral Control by Reproducing Kernel Hilbert Space Embedding
Venue: arXiv cs.LG 2012
Year: 2012

We present an embedding of stochastic optimal control problems, of the so called path integral form, into reproducing kernel Hilbert spaces. Using consistent, sample based estimates of the embedding leads to a model free, non-parametric approach for calculation of an approximate solution to the control problem. This formulation admits a decomposition of the problem into an invariant and task dependent component. Consequently, we make much more efficient use of the sample data compared to previous sample based approaches in this domain, e.g., by allowing sample re-use across tasks. Numerical examples on test problems, which illustrate the sample efficiency, are provided.
Social Event Detection with Interaction Graph Modeling
Venue: arXiv cs.SI 2012
Year: 2012

This paper focuses on detecting social, physical-world events from photos posted on social media sites. The problem is important: cheap media capture devices have significantly increased the number of photos shared on these sites. The main contribution of this paper is to incorporate online social interaction features in the detection of physical events. We believe that online social interaction reflect important signals among the participants on the "social affinity" of two photos, thereby helping event detection. We compute social affinity via a random-walk on a social interaction graph to determine similarity between two photos on the graph. We train a support vector machine classifier to combine the social affinity between photos and photo-centric metadata including time, location, tags and description. Incremental clustering is then used to group photos to event clusters. We have very good results on two large scale real-world datasets: Upcoming and MediaEval. We show an improvement between 0.06-0.10 in F1 on these datasets.
The Relative Exponential Time Complexity of Approximate Counting Satisfying Assignments
Venue: arXiv cs.CC 2012
Year: 2012

We study the exponential time complexity of approximate counting satisfying assignments of CNFs. We reduce the problem to deciding satisfiability of a CNF. Our reduction preserves the number of variables of the input formula and thus also preserves the exponential complexity of approximate counting. Our algorithm is also similar to an algorithm which works particular well in practice for which however no approximation guarantee was known. Towards an analysis of our reduction we provide a new inequality similar to the Bonami-Beckner hypercontractive inequality.
Characteristic formulas over intermediate logics
Venue: arXiv cs.LO 2012
Year: 2012

We expand the notion of characteristic formula to infinite finitely presentable subdirectly irreducible algebras. We prove that there is a continuum of varieties of Heyting algebras containing infinite finitely presentable subdirectly irreducible algebras. Moreover, we prove that there is a continuum of intermediate logics that can be axiomatized by characteristic formulas of infinite algebras while they are not axiomatizable by standard Jankov formulas. We give the examples of intermediate logics that are not axiomatizable by characteristic formulas of infinite algebras. Also, using the Goedel-McKinsey-Tarski translation we extend these results to the varieties of interior algebras and normal extensions of S4
Exploring scientists' working timetable: Do scientists often work overtime?
Venue: arXiv cs.DL 2012
Year: 2012

A novel method is proposed to monitor and record scientists' working timetable. We record the downloads information of scientific papers real-timely from Springer round the clock, and try to explore scientists' working habits. As our observation demonstrates, many scientists are still engaged in their research after working hours every day. Many of them work far into the night, even till next morning. In addition, research work also intrudes into their weekends. Different working time patterns are revealed. In the US, overnight work is more prevalent among scientists, while Chinese scientists mostly have busy weekends with their scientific research.
Expressiveness and Completeness in Abstraction
Venue: arXiv cs.LO 2012
Year: 2012

We study two notions of expressiveness, which have appeared in abstraction theory for model checking, and find them incomparable in general. In particular, we show that according to the most widely used notion, the class of Kripke Modal Transition Systems is strictly less expressive than the class of Generalised Kripke Modal Transition Systems (a generalised variant of Kripke Modal Transition Systems equipped with hypertransitions). Furthermore, we investigate the ability of an abstraction framework to prove a formula with a finite abstract model, a property known as completeness. We address the issue of completeness from a general perspective: the way it depends on certain abstraction parameters, as well as its relationship with expressiveness.
Tree rules in probabilistic transition system specifications with negative and quantitative premises
Venue: arXiv cs.PL 2012
Year: 2012

Probabilistic transition system specifications (PTSSs) in the ntmufnu/ntmuxnu format provide structural operational semantics for Segala-type systems that exhibit both probabilistic and nondeterministic behavior and guarantee that isimilarity is a congruence.Similar to the nondeterministic case of rule format tyft/tyxt, we show that the well-foundedness requirement is unnecessary in the probabilistic setting. To achieve this, we first define an extended version of the ntmufnu/ntmuxnu format in which quantitative premises and conclusions include nested convex combinations of distributions. This format also guarantees that bisimilarity is a congruence. Then, for a given (possibly non-well-founded) PTSS in the new format, we construct an equivalent well-founded transition system consisting of only rules of the simpler (well-founded) probabilistic ntree format. Furthermore, we develop a proof-theoretic notion for these PTSSs that coincides with the existing stratification-based meaning in case the PTSS is stratifiable. This continues the line of research lifting structural operational semantic results from the nondeterministic setting to systems with both probabilistic and nondeterministic behavior.
Operational semantics for signal handling
Venue: arXiv cs.PL 2012
Year: 2012

Signals are a lightweight form of interprocess communication in Unix. When a process receives a signal, the control flow is interrupted and a previously installed signal handler is run. Signal handling is reminiscent both of exception handling and concurrent interleaving of processes. In this paper, we investigate different approaches to formalizing signal handling in operational semantics, and compare them in a series of examples. We find the big-step style of operational semantics to be well suited to modelling signal handling. We integrate exception handling with our big-step semantics of signal handling, by adopting the exception convention as defined in the Definition of Standard ML. The semantics needs to capture the complex interactions between signal handling and exception handling.
On Derivatives and Subpattern Orders of Countable Subshifts
Venue: arXiv cs.CC 2012
Year: 2012

We study the computational and structural aspects of countable two-dimensional SFTs and other subshifts. Our main focus is on the topological derivatives and subpattern posets of these objects, and our main results are constructions of two-dimensional countable subshifts with interesting properties. We present an SFT whose iterated derivatives are maximally complex from the computational point of view, a sofic shift whose subpattern poset contains an infinite descending chain, a family of SFTs whose finite subpattern posets contain arbitrary finite posets, and a natural example of an SFT with infinite Cantor-Bendixon rank.
Computing by Temporal Order: Asynchronous Cellular Automata
Venue: arXiv cs.FL 2012
Year: 2012

Our concern is the behaviour of the elementary cellular automata with state set 0,1 over the cell set Z/nZ (one-dimensional finite wrap-around case), under all possible update rules (asynchronicity). Over the torus Z/nZ (n<= 11),we will see that the ECA with Wolfram rule 57 maps any v in F_2^n to any w in F_2^n, varying the update rule. We furthermore show that all even (element of the alternating group) bijective functions on the set F_2^n = 0,...,2^n-1, can be computed by ECA57, by iterating it a sufficient number of times with varying update rules, at least for n <= 10. We characterize the non-bijective functions computable by asynchronous rules.
Linear functional classes over cellular automata
Venue: arXiv cs.FL 2012
Year: 2012

Cellular automata are a discrete dynamical system which models massively parallel computation. Much attention is devoted to computations with small time complexity for which the parallelism may provide further possibilities. In this paper, we investigate the ability of cellular automata related to functional computation. We introduce several functional classes of low time complexity which contain "natural" problems. We examine their inclusion relationships and emphasize that several questions arising from this functional framework are related to current ones coming from the recognition context. We also provide a negative result which explicits limits on the information transmission whose consequences go beyond the functional point of view.
Multidimensional Web Page Evaluation Model Using Segmentation And Annotations
Venue: arXiv cs.IR 2012
Year: 2012

The evaluation of web pages against a query is the pivot around which the Information Retrieval domain revolves around. The context sensitive, semantic evaluation of web pages is a non-trivial problem which needs to be addressed immediately. This research work proposes a model to evaluate the web pages by cumulating the segment scores which are computed by multidimensional evaluation methodology. The model proposed is hybrid since it utilizes both the structural semantics and content semantics in the evaluation process. The score of the web page is computed in a bottom-up process by evaluating individual segment's score through a multi-dimensional approach. The model incorporates an approach for segment level annotation. The proposed model is prototyped for evaluation; experiments conducted on the prototype confirm the model's efficiency in semantic evaluation of pages.
Small Strong Epsilon Nets
Venue: arXiv cs.CG 2012
Year: 2012

Let P be a set of n points in $\mathbb{R}^d$. A point x is said to be a centerpoint of P if x is contained in every convex object that contains more than $dn\over d+1$ points of P. We call a point x a strong centerpoint for a family of objects $\mathcal{C}$ if $x \in P$ is contained in every object $C \in \mathcal{C}$ that contains more than a constant fraction of points of P. A strong centerpoint does not exist even for halfspaces in $\mathbb{R}^2$. We prove that a strong centerpoint exists for axis-parallel boxes in $\mathbb{R}^d$ and give exact bounds. We then extend this to small strong $ε$-nets in the plane and prove upper and lower bounds for $ε_i^\mathcal{S}$ where $\mathcal{S}$ is the family of axis-parallel rectangles, halfspaces and disks. Here $ε_i^\mathcal{S}$ represents the smallest real number in $[0,1]$ such that there exists an $ε_i^\mathcal{S}$-net of size i with respect to $\mathcal{S}$.
Adapt or Die: Polynomial Lower Bounds for Non-Adaptive Dynamic Data Structures
Venue: arXiv cs.DS 2012
Year: 2012

In this paper, we study the role non-adaptivity plays in maintaining dynamic data structures. Roughly speaking, a data structure is non-adaptive if the memory locations it reads and/or writes when processing a query or update depend only on the query or update and not on the contents of previously read cells. We study such non-adaptive data structures in the cell probe model. This model is one of the least restrictive lower bound models and in particular, cell probe lower bounds apply to data structures developed in the popular word-RAM model. Unfortunately, this generality comes at a high cost: the highest lower bound proved for any data structure problem is only polylogarithmic. Our main result is to demonstrate that one can in fact obtain polynomial cell probe lower bounds for non-adaptive data structures. To shed more light on the seemingly inherent polylogarithmic lower bound barrier, we study several different notions of non-adaptivity and identify key properties that must be dealt with if we are to prove polynomial lower bounds without restrictions on the data structures. Finally, our results also unveil an interesting connection between data structures and depth-2 circuits. This allows us to translate conjectured hard data structure problems into good candidates for high circuit lower bounds; in particular, in the area of linear circuits for linear operators. Building on lower bound proofs for data structures in slightly more restrictive models, we also present a number of properties of linear operators which we believe are worth investigating in the realm of circuit lower bounds.
Efficient Quasigroup Block Cipher for Sensor Networks
Venue: arXiv cs.CR 2012
Year: 2012

We present a new quasigroup based block encryption system with and without cipher-block-chaining. We compare its performance against Advanced Encryption Standard-256 (AES256) bit algorithm using the NIST statistical test suite (NIST-STS) that tests for randomness of a sequence. Since it is well known that a good encryption algorithm must destroy any statistical properties of the input sequence and produce an output close to a true random sequence, the NIST-STS suite results provide a good test bench. In almost all tests from the suite the proposed algorithm performs better than AES256.
Low Complexity Space-Frequency MIMO OFDM System for Double-Selective Fading Channels
Venue: arXiv cs.IT 2012
Year: 2012

This paper presents a highly robust space-frequency block coded (SFBC) multiple-input multiple-output (MIMO) orthogonal frequency division multiplexing (OFDM) system. The proposed system is based on applying a short block length Walsh Hadamard transform (WHT) after the SFBC encoder. The main advantage of the proposed system is that the channel frequency responses over every two adjacent subcarriers become equal. Such interesting result provides an exceptional operating conditions for SFBC-OFDM systems transmitting over time and frequencyselective fading channels. Monte Carlo simulation is used to evaluate the bit error rate (BER) performance of the proposed system using various wireless channels with different degrees of frequency selectivity and Doppler spreads. The simulation results demonstrated that the proposed scheme substantially outperforms the standard SFBC-OFDM and the space-time block coded (STBC) OFDM systems in severe time-varying frequency-selective fading channels. Moreover, the proposed system has very low complexity because it is based on short block length WHT.