OpenRaiser/Intern-Atlas huggingface dataset:
Revisiting the Complexity of Stability of Continuous and Hybrid Systems
Venue: arXiv cs.SY 2014
Year: 2014

We develop a framework to give upper bounds on the "practical" computational complexity of stability problems for a wide range of nonlinear continuous and hybrid systems. To do so, we describe stability properties of dynamical systems using first-order formulas over the real numbers, and reduce stability problems to the delta-decision problems of these formulas. The framework allows us to obtain a precise characterization of the complexity of different notions of stability for nonlinear continuous and hybrid systems. We prove that bounded versions of the stability problems are generally decidable, and give upper bounds on their complexity. The unbounded versions are generally undecidable, for which we give upper bounds on their degrees of unsolvability.
Nonmonotonic Reasoning as a Temporal Activity
Venue: arXiv cs.AI 2014
Year: 2014

A {\it dynamic reasoning system} (DRS) is an adaptation of a conventional formal logical system that explicitly portrays reasoning as a temporal activity, with each extralogical input to the system and each inference rule application being viewed as occurring at a distinct time step. Every DRS incorporates some well-defined logic together with a controller that serves to guide the reasoning process in response to user inputs. Logics are generic, whereas controllers are application-specific. Every controller does, nonetheless, provide an algorithm for nonmonotonic belief revision. The general notion of a DRS comprises a framework within which one can formulate the logic and algorithms for a given application and prove that the algorithms are correct, i.e., that they serve to (i) derive all salient information and (ii) preserve the consistency of the belief set. This paper illustrates the idea with ordinary first-order predicate calculus, suitably modified for the present purpose, and an example. The example revisits some classic nonmonotonic reasoning puzzles (Opus the Penguin, Nixon Diamond) and shows how these can be resolved in the context of a DRS, using an expanded version of first-order logic that incorporates typed predicate symbols. All concepts are rigorously defined and effectively computable, thereby providing the foundation for a future software implementation.
Randomized Sketches of Convex Programs with Sharp Guarantees
Venue: arXiv cs.IT 2014
Year: 2014

Random projection (RP) is a classical technique for reducing storage and computational costs. We analyze RP-based approximations of convex programs, in which the original optimization problem is approximated by the solution of a lower-dimensional problem. Such dimensionality reduction is essential in computation-limited settings, since the complexity of general convex programming can be quite high (e.g., cubic for quadratic programs, and substantially higher for semidefinite programs). In addition to computational savings, random projection is also useful for reducing memory usage, and has useful properties for privacy-sensitive optimization. We prove that the approximation ratio of this procedure can be bounded in terms of the geometry of constraint set. For a broad class of random projections, including those based on various sub-Gaussian distributions as well as randomized Hadamard and Fourier transforms, the data matrix defining the cost function can be projected down to the statistical dimension of the tangent cone of the constraints at the original solution, which is often substantially smaller than the original dimension. We illustrate consequences of our theory for various cases, including unconstrained and $\ell_1$-constrained least squares, support vector machines, low-rank matrix estimation, and discuss implications on privacy-sensitive optimization and some connections with de-noising and compressed sensing.
Generalizing Modular Logic Programs
Venue: arXiv cs.AI 2014
Year: 2014

Even though modularity has been studied extensively in conventional logic programming, there are few approaches on how to incorporate modularity into Answer Set Programming, a prominent rule-based declarative programming paradigm. A major approach is Oikarinnen and Janhunen's Gaifman-Shapiro-style architecture of program modules, which provides the composition of program modules. Their module theorem properly strengthens Lifschitz and Turner's splitting set theorem for normal logic programs. However, this approach is limited by module conditions that are imposed in order to ensure the compatibility of their module system with the stable model semantics, namely forcing output signatures of composing modules to be disjoint and disallowing positive cyclic dependencies between different modules. These conditions turn out to be too restrictive in practice and in this paper we discuss alternative ways of lift both restrictions independently, effectively solving the first, widening the applicability of this framework and the scope of the module theorem.
Human Factors of Formal Methods
Venue: arXiv cs.SE 2014
Year: 2014

This paper provides a brief introduction to the work that aims to apply the achievements within the area of engineering psychology to the area of formal methods, focusing on the specification phase of a system development process.
Refinement-Based Specification: Requirements and Architecture
Venue: arXiv cs.SE 2014
Year: 2014

This paper presents the methodology for the system requirements and architecture w.r.t. their decomposition and refinement. It also introduces ideas of refinement layers and of refinement-based verification.
Fast Dynamic Graph Algorithms for Parameterized Problems
Venue: arXiv cs.DS 2014
Year: 2014

Fully dynamic graph is a data structure that (1) supports edge insertions and deletions and (2) answers problem specific queries. The time complexity of (1) and (2) are referred to as the update time and the query time respectively. There are many researches on dynamic graphs whose update time and query time are $o(|G|)$, that is, sublinear in the graph size. However, almost all such researches are for problems in P. In this paper, we investigate dynamic graphs for NP-hard problems exploiting the notion of fixed parameter tractability (FPT). We give dynamic graphs for Vertex Cover and Cluster Vertex Deletion parameterized by the solution size $k$. These dynamic graphs achieve almost the best possible update time $O(\mathrm{poly}(k)\log n)$ and the query time $O(f(\mathrm{poly}(k),k))$, where $f(n,k)$ is the time complexity of any static graph algorithm for the problems. We obtain these results by dynamically maintaining an approximate solution which can be used to construct a small problem kernel. Exploiting the dynamic graph for Cluster Vertex Deletion, as a corollary, we obtain a quasilinear-time (polynomial) kernelization algorithm for Cluster Vertex Deletion. Until now, only quadratic time kernelization algorithms are known for this problem. We also give a dynamic graph for Chromatic Number parameterized by the solution size of Cluster Vertex Deletion, and a dynamic graph for bounded-degree Feedback Vertex Set parameterized by the solution size. Assuming the parameter is a constant, each dynamic graph can be updated in $O(\log n)$ time and can compute a solution in $O(1)$ time. These results are obtained by another approach.
Covert Optical Communication
Venue: arXiv cs.IT 2014
Year: 2014

Encryption prevents unauthorized decoding, but does not ensure stealth---a security demand that a mere presence of a message be undetectable. We characterize the ultimate limit of covert communication that is secure against the most powerful physically-permissible adversary. We show that, although it is impossible over a pure-loss channel, covert communication is attainable in the presence of any excess noise, such as a $300$K thermal blackbody. In this case, $\mathcal{O}(\sqrt{n})$ bits can be transmitted reliably and covertly in $n$ optical modes using standard optical communication equipment. The all-powerful adversary may intercept all transmitted photons not received by the intended receiver, and employ arbitrary quantum memory and measurements. Conversely, we show that this square root scaling cannot be outperformed. We corroborate our theory in a proof-of-concept experiment. We believe that our findings will enable practical realizations of covert communication and sensing, both for point-to-point and networked scenarios.
A LabVIEW based user-friendly X-ray phase-contrast imaging system software platform
Venue: arXiv cs.SE 2014
Year: 2014

X-ray phase-contrast imaging can provide greatly improved contrast over conventional absorption-based imaging for weakly absorbing samples, such as biological soft tissues and fibre composites. In this manuscript, we introduce an easy and fast way to develop a user-friendly software platform dedicated to the new grating-based X-ray phase-contrast imaging setup recently built at the National Synchrotron Radiation Laboratory of the University of Science and Technology of China. Unified management and control of 21 motorized positioning stages, of an ultra-precision piezoelectric translation stage and of the X-ray tube are achieved with this platform. The software package also covers the automatic image acquisition of the phase-stepping scanning with a flat panel detector. Moreover, a data post-processing module for signals retrieval and other custom features are in principle available. With a seamless integration of all necessary functions in a unique package, this software platform will greatly support the user activity during experimental runs.
I know what leaked in your pocket: uncovering privacy leaks on Android Apps with Static Taint Analysis
Venue: arXiv cs.SE 2014
Year: 2014

Android applications may leak privacy data carelessly or maliciously. In this work we perform inter-component data-flow analysis to detect privacy leaks between components of Android applications. Unlike all current approaches, our tool, called IccTA, propagates the context between the components, which improves the precision of the analysis. IccTA outperforms all other available tools by reaching a precision of 95.0% and a recall of 82.6% on DroidBench. Our approach detects 147 inter-component based privacy leaks in 14 applications in a set of 3000 real-world applications with a precision of 88.4%. With the help of ApkCombiner, our approach is able to detect inter-app based privacy leaks.
The Utility and Practicality of Quantifying Software Reliability
Venue: arXiv cs.SE 2014
Year: 2014

We argue that quantifying software reliability is important in demonstrating that system-level risks are As Low As Reasonably Practicable (ALARP). Furthermore, we demonstrate that such quantification is possible in at least one meaningful case. It is, however, unlikely to be practical in every case. This means it is unlikely to be included as an explicit objective in standards. Hence, for those cases where software reliability can be quantified, merely following a standard may lead to risk-reduction opportunities being missed.
An Approach to Forgetting in Disjunctive Logic Programs that Preserves Strong Equivalence
Venue: arXiv cs.AI 2014
Year: 2014

In this paper we investigate forgetting in disjunctive logic programs, where forgetting an atom from a program amounts to a reduction in the signature of that program. The goal is to provide an approach that is syntax-independent, in that if two programs are strongly equivalent, then the results of forgetting an atom in each program should also be strongly equivalent. Our central definition of forgetting is impractical but satisfies this goal: Forgetting an atom is characterised by the set of SE consequences of the program that do not mention the atom to be forgotten. We then provide an equivalent, practical definition, wherein forgetting an atom $p$ is given by those rules in the program that don't mention $p$, together with rules obtained by a single inference step from rules that do mention $p$. Forgetting is shown to have appropriate properties; as well, the finite characterisation results in a modest (at worst quadratic) blowup. Finally we have also obtained a prototype implementation of this approach to forgetting.
Performance Bounds for Vector Quantized Compressive Sensing
Venue: arXiv cs.IT 2014
Year: 2014

In this paper, we endeavor for predicting the performance of quantized compressive sensing under the use of sparse reconstruction estimators. We assume that a high rate vector quantizer is used to encode the noisy compressive sensing measurement vector. Exploiting a block sparse source model, we use Gaussian mixture density for modeling the distribution of the source. This allows us to formulate an optimal rate allocation problem for the vector quantizer. Considering noisy CS quantized measurements, we analyze upper- and lower-bounds on reconstruction error performance guarantee of two estimators - convex relaxation based basis pursuit de-noising estimator and an oracle-assisted least-squares estimator.
Aca 2.0: Questions and Answers
Venue: arXiv cs.DL 2014
Year: 2014

"Academia 2.0" is a proposal to organize scientific publishing around true peer-to-peer distributed dissemination channels and eliminate the traditional role of the academic publisher. This model will be first presented at the 2014 workshop on Reproducible Research Methodologies and New Publication Models in Computer Engineering (TRUST'14) in the form of a high-level overview, so as to stimulate discussion and gather feedback on its merits and feasibility. This report complements the 6-page introductory article presented at TRUST, by detailing the review processes, some use scenarios and answering the reviewer's comments in detail.
Games with recurring certainty
Venue: arXiv cs.LO 2014
Year: 2014

Infinite games where several players seek to coordinate under imperfect information are known to be intractable, unless the information flow is severely restricted. Examples of undecidable cases typically feature a situation where players become uncertain about the current state of the game, and this uncertainty lasts forever. Here we consider games where the players attain certainty about the current state over and over again along any play. For finite-state games, we note that this kind of recurring certainty implies a stronger condition of periodic certainty, that is, the events of state certainty ultimately occur at uniform, regular intervals. We show that it is decidable whether a given game presents recurring certainty, and that, if so, the problem of synthesising coordination strategies under w-regular winning conditions is solvable.
Pupil: An Open Source Platform for Pervasive Eye Tracking and Mobile Gaze-based Interaction
Venue: arXiv cs.CV 2014
Year: 2014

Commercial head-mounted eye trackers provide useful features to customers in industry and research but are expensive and rely on closed source hardware and software. This limits the application areas and use of mobile eye tracking to expert users and inhibits user-driven development, customisation, and extension. In this paper we present Pupil -- an accessible, affordable, and extensible open source platform for mobile eye tracking and gaze-based interaction. Pupil comprises 1) a light-weight headset with high-resolution cameras, 2) an open source software framework for mobile eye tracking, as well as 3) a graphical user interface (GUI) to playback and visualize video and gaze data. Pupil features high-resolution scene and eye cameras for monocular and binocular gaze estimation. The software and GUI are platform-independent and include state-of-the-art algorithms for real-time pupil detection and tracking, calibration, and accurate gaze estimation. Results of a performance evaluation show that Pupil can provide an average gaze estimation accuracy of 0.6 degree of visual angle (0.08 degree precision) with a latency of the processing pipeline of only 0.045 seconds.
Space-Time Physical-Layer Network Coding
Venue: arXiv cs.IT 2014
Year: 2014

A space-time physical-layer network coding (ST- PNC) method is presented for information exchange among multiple users over fully-connected multi-way relay networks. The method involves two steps: i) side-information learning and ii) space-time relay transmission. In the first step, different sets of users are scheduled to send signals over networks and the remaining users and relays overhear the transmitted signals, thereby learning the interference patterns. In the second step, multiple relays cooperatively send out linear combinations of signals received in the previous phase using space-time precoding so that all users efficiently exploit their side-information in the form of: 1) what they sent and 2) what they overheard in decoding. This coding concept is illustrated through two simple network examples. It is shown that ST-PNC improves the sum of degrees of freedom (sum-DoF) of the network compared to existing interference management methods. With ST-PNC, the sum-DoF of a general multi-way relay network without channel knowledge at the users is characterized in terms of relevant system parameters, chiefly the number of users, the number of relays, and the number of antennas at relays. A major implication of the derived results is that efficiently harnessing both transmit- ted and overheard signals as side-information brings significant performance improvements to fully-connected multi-way relay networks.
Exemplar Dynamics Models of the Stability of Phonological Categories
Venue: arXiv cs.CL 2014
Year: 2014

We develop a model for the stability and maintenance of phonological categories. Examples of phonological categories are vowel sounds such as "i" and "e". We model such categories as consisting of collections of labeled exemplars that language users store in their memory. Each exemplar is a detailed memory of an instance of the linguistic entity in question. Starting from an exemplar-level model we derive integro-differential equations for the long-term evolution of the density of exemplars in different portions of phonetic space. Using these latter equations we investigate under what conditions two phonological categories merge or not. Our main conclusion is that for the preservation of distinct phonological categories, it is necessary that anomalous speech tokens of a given category are discarded, and not merely stored in memory as an exemplar of another category.
Unified POF Programming for Diversified SDN Data Plane
Venue: arXiv cs.NI 2014
Year: 2014

In many real-world OpenFlow-based SDN deployments, the ability to program heterogeneous forwarding elements built with different forwarding architectures is a desirable capability. In this paper, we discuss a data plane programming framework suitable for a flexible and protocol-oblivious data plane and show how OpenFlow can evolve to provide a generic interface for platform-independent programming and platform-specific compiling. We also show how an abstract instruction set can play a pivotal role to support different programming styles mapping to different forwarding chip architectures. As an example, we compare the compiler-mode and interpreter-mode implementations for an NPU-based forwarding element and conclude that the compiler-mode implementation can achieve a performance similar to that of a conventional non-SDN implementation. Built upon our protocol-oblivious forwarding (POF) vision, this work presents our continuous efforts to complete the ecosystem and pave the SDN evolving path. The programming framework could be considered as a proposal for the OpenFlow 2.0 standard.
Binary Protector: Intrusion Detection in Multitier Web Applications
Venue: arXiv cs.CR 2014
Year: 2014

The services of internet place a key role in the daily life by enabling the in sequence from anywhere. To provide somewhere to stay the communication and management in applications the web services has stimulated to multitier design. In this multitier the web servers contain front end logic and data with database servers. In this paper, we present binary protector intrusion detection systems which designs the network behavior of user sessions across both the front-end web server and the back-end database. By examining both web and subsequent database requests, we are able to rummage out attacks that independent IDS would not be able to distinguish.
Inference Control for Privacy-Preserving Genome Matching
Venue: arXiv cs.CR 2014
Year: 2014

Privacy is of the utmost importance in genomic matching. Therefore a number of privacy-preserving protocols have been presented using secure computation. Nevertheless, none of these protocols prevents inferences from the result. Goodrich has shown that this resulting information is sufficient for an effective attack on genome databases. In this paper we present an approach that can detect and mitigate such an attack on encrypted messages while still preserving the privacy of both parties. Note that randomization, e.g.~using differential privacy, will almost certainly destroy the utility of the matching result. We combine two known cryptographic primitives -- secure computation of the edit distance and fuzzy commitments -- in order to prevent submission of similar genome sequences. Particularly, we contribute an efficient zero-knowledge proof that the same input has been used in both primitives. We show that using our approach it is feasible to preserve privacy in genome matching and also detect and mitigate Goodrich's attack.
Exchangeable Variable Models
Venue: arXiv cs.LG 2014
Year: 2014

A sequence of random variables is exchangeable if its joint distribution is invariant under variable permutations. We introduce exchangeable variable models (EVMs) as a novel class of probabilistic models whose basic building blocks are partially exchangeable sequences, a generalization of exchangeable sequences. We prove that a family of tractable EVMs is optimal under zero-one loss for a large class of functions, including parity and threshold functions, and strictly subsumes existing tractable independence-based model families. Extensive experiments show that EVMs outperform state of the art classifiers such as SVMs and probabilistic models which are solely based on independence assumptions.
Numerical Investigation of Effects of Compound Angle and Length to Diameter Ratio on Adiabatic Film Cooling Effectiveness
Venue: arXiv cs.CE 2014
Year: 2014

A modification has been done in the normal injection hole of 35 degree, by injecting the cold fluid at different angles(compound angle) in lateral direction, providing a significant change in the shape of holes which later we found in our numerical investigation giving good quality of effectiveness in cooling. Different L/D ratios are also studied for each compound angle. The numerical simulation is performed based on Reynolds Averaged Navier-Stokes(RANS) equations with k-epsilon turbulence model by using Fluent(Commercial Software). Adiabatic Film Cooling Effectiveness has been studied for compound angles of (0, 30, 45 and 60 degrees) and L/D ratios of (1, 2, 3 and 4) on a hole of 6mm diameter with blowing ratio 0.5. The findings are obtained from the results, concludes that the trend of laterally averaged adiabatic effectiveness is the function of L/D ratio and compound angle.