OpenRaiser/Intern-Atlas huggingface dataset:
The Causal Frame Problem: An Algorithmic Perspective
Venue: arXiv cs.AI 2017
Year: 2017

The Frame Problem (FP) is a puzzle in philosophy of mind and epistemology, articulated by the Stanford Encyclopedia of Philosophy as follows: "How do we account for our apparent ability to make decisions on the basis only of what is relevant to an ongoing situation without having explicitly to consider all that is not relevant?" In this work, we focus on the causal variant of the FP, the Causal Frame Problem (CFP). Assuming that a reasoner's mental causal model can be (implicitly) represented by a causal Bayes net, we first introduce a notion called Potential Level (PL). PL, in essence, encodes the relative position of a node with respect to its neighbors in a causal Bayes net. Drawing on the psychological literature on causal judgment, we substantiate the claim that PL may bear on how time is encoded in the mind. Using PL, we propose an inference framework, called the PL-based Inference Framework (PLIF), which permits a boundedly-rational approach to the CFP to be formally articulated at Marr's algorithmic level of analysis. We show that our proposed framework, PLIF, is consistent with a wide range of findings in causal judgment literature, and that PL and PLIF make a number of predictions, some of which are already supported by existing findings.
Relationship Maintenance in Software Language Repositories
Venue: arXiv cs.PL 2017
Year: 2017

The context of this research is testing and building software systems and, specifically, software language repositories (SLRs), i.e., repositories with components for language processing (interpreters, translators, analyzers, transformers, pretty printers, etc.). SLRs are typically set up for developing and using metaprogramming systems, language workbenches, language definition frameworks, executable semantic frameworks, and modeling frameworks. This work is an inquiry into testing and building SLRs in a manner that the repository is seen as a collection of language-typed artifacts being related by the applications of language-typed functions or relations which serve language processing. The notion of language is used in a broad sense to include text-, tree-, graph-based languages as well as representations based on interchange formats and also proprietary formats for serialization. The overall approach underlying this research is one of language design driven by a complex case study, i.e., a specific SLR with a significant number of processed languages and language processors as well as a noteworthy heterogeneity in terms of representation types and implementation languages. The knowledge gained by our research is best understood as a declarative language design for regression testing and build management, we introduce a corresponding language Ueber with an executable semantics which maintains relationships between language-typed artifacts in an SLR. The grounding of the reported research is based on the comprehensive, formal, executable (logic programming-based) definition of the Ueber language and its systematic application to the management of the SLR YAS which consists of hundreds of language definition and processing components (such as interpreters and transformations) for more than thirty languages (not counting different representation types) with Prolog, Haskell, Java, and Python being used as implementation languages. The importance of this work follows from the significant costs implied by regression testing and build management and also from the complexity of SLRs which calls for means to help with understanding.
Fast Simplified Successive-Cancellation List Decoding of Polar Codes
Venue: arXiv cs.IT 2017
Year: 2017

Polar codes are capacity achieving error correcting codes that can be decoded through the successive-cancellation algorithm. To improve its error-correction performance, a list-based version called successive-cancellation list (SCL) has been proposed in the past, that however substantially increases the number of time-steps in the decoding process. The simplified SCL (SSCL) decoding algorithm exploits constituent codes within the polar code structure to greatly reduce the required number of time-steps without introducing any error-correction performance loss. In this paper, we propose a faster decoding approach to decode one of these constituent codes, the Rate-1 node. We use this Rate-1 node decoder to develop Fast-SSCL. We demonstrate that only a list-size-bound number of bits needs to be estimated in Rate-1 nodes and Fast-SSCL exactly matches the error-correction performance of SCL and SSCL. This technique can potentially greatly reduce the total number of time-steps needed for polar codes decoding: analysis on a set of case studies show that Fast-SSCL has a number of time-steps requirement that is up to 66.6% lower than SSCL and 88.1% lower than SCL.
Balancing and Walking Using Full Dynamics LQR Control With Contact Constraints
Venue: arXiv cs.RO 2017
Year: 2017

Torque control algorithms which consider robot dynamics and contact constraints are important for creating dynamic behaviors for humanoids. As computational power increases, algorithms tend to also increase in complexity. However, it is not clear how much complexity is really required to create controllers which exhibit good performance. In this paper, we study the capabilities of a simple approach based on contact consistent LQR controllers designed around key poses to control various tasks on a humanoid robot. We present extensive experimental results on a hydraulic, torque controlled humanoid performing balancing and stepping tasks. This feedback control approach captures the necessary synergies between the DoFs of the robot to guarantee good control performance. We show that for the considered tasks, it is only necessary to re-linearize the dynamics of the robot at different contact configurations and that increasing the number of LQR controllers along desired trajectories does not improve performance. Our result suggest that very simple controllers can yield good performance competitive with current state of the art, but more complex, optimization-based whole-body controllers. A video of the experiments can be found at https://youtu.be/5T08CNKV1hw.
Implementing Open Call-by-Value (Extended Version)
Venue: arXiv cs.LO 2017
Year: 2017

The theory of the call-by-value lambda-calculus relies on weak evaluation and closed terms, that are natural hypotheses in the study of programming languages. To model proof assistants, however, strong evaluation and open terms are required. Open call-by-value is the intermediate setting of weak evaluation with open terms, on top of which Grégoire and Leroy designed the abstract machine of Coq. This paper provides a theory of abstract machines for open call-by-value. The literature contains machines that are either simple but inefficient, as they have an exponential overhead, or efficient but heavy, as they rely on a labelling of environments and a technical optimization. We introduce a machine that is simple and efficient: it does not use labels and it implements open call-by-value within a bilinear overhead. Moreover, we provide a new fine understanding of how different optimizations impact on the complexity of the overhead.
How to Search the Internet Archive Without Indexing It
Venue: arXiv cs.DL 2017
Year: 2017

Significant parts of cultural heritage are produced on the web during the last decades. While easy accessibility to the current web is a good baseline, optimal access to the past web faces several challenges. This includes dealing with large-scale web archive collections and lacking of usage logs that contain implicit human feedback most relevant for today's web search. In this paper, we propose an entity-oriented search system to support retrieval and analytics on the Internet Archive. We use Bing to retrieve a ranked list of results from the current web. In addition, we link retrieved results to the WayBack Machine; thus allowing keyword search on the Internet Archive without processing and indexing its raw archived content. Our search system complements existing web archive search tools through a user-friendly interface, which comes close to the functionalities of modern web search engines (e.g., keyword search, query auto-completion and related query suggestion), and provides a great benefit of taking user feedback on the current web into account also for web archive search. Through extensive experiments, we conduct quantitative and qualitative analyses in order to provide insights that enable further research on and practical applications of web archives.
Detection, Segmentation and Recognition of Face and its Features Using Neural Network
Venue: arXiv cs.CV 2017
Year: 2017

Face detection and recognition has been prevalent with research scholars and diverse approaches have been incorporated till date to serve purpose. The rampant advent of biometric analysis systems, which may be full body scanners, or iris detection and recognition systems and the finger print recognition systems, and surveillance systems deployed for safety and security purposes have contributed to inclination towards same. Advances has been made with frontal view, lateral view of the face or using facial expressions such as anger, happiness and gloominess, still images and video image to be used for detection and recognition. This led to newer methods for face detection and recognition to be introduced in achieving accurate results and economically feasible and extremely secure. Techniques such as Principal Component analysis (PCA), Independent component analysis (ICA), Linear Discriminant Analysis (LDA), have been the predominant ones to be used. But with improvements needed in the previous approaches Neural Networks based recognition was like boon to the industry. It not only enhanced the recognition but also the efficiency of the process. Choosing Backpropagation as the learning method was clearly out of its efficiency to recognize nonlinear faces with an acceptance ratio of more than 90% and execution time of only few seconds.
Anonymous or not? Understanding the Factors Affecting Personal Mobile Data Disclosure
Venue: arXiv cs.CY 2017
Year: 2017

The wide adoption of mobile devices and social media platforms have dramatically increased the collection and sharing of personal information. More and more frequently, users are called to take decisions concerning the disclosure of their personal information. In this study, we investigate the factors affecting users' choices toward the disclosure of their personal data, including not only their demographic and self-reported individual characteristics, but also their social interactions and their mobility patterns inferred from months of mobile phone data activity. We report the findings of a field-study conducted with a community of 63 subjects provided with (i) a smart-phone and (ii) a Personal Data Store (PDS) enabling them to control the disclosure of their data. We monitor the sharing behavior of our participants through the PDS, and evaluate the contribution of different factors affecting their disclosing choices of location and social interaction data. Our analysis shows that social interaction inferred by mobile phones is an important factor revealing willingness to share, regardless of the data type. In addition, we provide further insights on the individual traits relevant to the prediction of sharing behavior.
ClipAudit: A Simple Risk-Limiting Post-Election Audit
Venue: arXiv cs.CR 2017
Year: 2017

We propose a simple risk-limiting audit for elections, ClipAudit. To determine whether candidate A (the reported winner) actually beat candidate B in a plurality election, ClipAudit draws ballots at random, without replacement, until either all cast ballots have been drawn, or until \[ a - b \ge β\sqrt{a+b} \] where $a$ is the number of ballots in the sample for the reported winner A, and $b$ is the number of ballots in the sample for opponent B, and where $β$ is a constant determined a priori as a function of the number $n$ of ballots cast and the risk-limit $α$. ClipAudit doesn't depend on the unofficial margin (as does Bravo). We show how to extend ClipAudit to contests with multiple winners or losers, or to multiple contests.
On Cooperation and Interference in the Weak Interference Regime (Full Version with Detailed Proofs)
Venue: arXiv cs.IT 2017
Year: 2017

Handling interference is one of the main challenges in the design of wireless networks. In this paper we study the application of cooperation for interference management in the weak interference (WI) regime, focusing on the Z-interference channel with a causal relay (Z-ICR), when the channel coefficients are subject to ergodic phase fading, all transmission powers are finite, and the relay is full-duplex. In order to provide a comprehensive understanding of the benefits of cooperation in the WI regime, we characterize, for the first time, two major performance measures for the ergodic phase fading Z-ICR in the WI regime: The sum-rate capacity and the maximal generalized degrees-of-freedom (GDoF). In the capacity analysis, we obtain conditions on the channel coefficients, subject to which the sum-rate capacity of the ergodic phase fading Z-ICR is achieved by treating interference as noise at each receiver, and explicitly state the corresponding sum-rate capacity. In the GDoF analysis, we derive conditions on the exponents of the magnitudes of the channel coefficients, under which treating interference as noise achieves the maximal GDoF, which is explicitly characterized as well. It is shown that under certain conditions on the channel coefficients, {\em relaying strictly increases} both the sum-rate capacity and the maximal GDoF of the ergodic phase fading Z-interference channel in the WI regime. Our results demonstrate {\em for the first time} the gains from relaying in the presence of interference, {\em when interference is weak and the relay power is finite}, both in increasing the sum-rate capacity and in increasing the maximal GDoF, compared to the channel without a relay.
Using English as Pivot to Extract Persian-Italian Parallel Sentences from Non-Parallel Corpora
Venue: arXiv cs.CL 2017
Year: 2017

The effectiveness of a statistical machine translation system (SMT) is very dependent upon the amount of parallel corpus used in the training phase. For low-resource language pairs there are not enough parallel corpora to build an accurate SMT. In this paper, a novel approach is presented to extract bilingual Persian-Italian parallel sentences from a non-parallel (comparable) corpus. In this study, English is used as the pivot language to compute the matching scores between source and target sentences and candidate selection phase. Additionally, a new monolingual sentence similarity metric, Normalized Google Distance (NGD) is proposed to improve the matching process. Moreover, some extensions of the baseline system are applied to improve the quality of extracted sentences measured with BLEU. Experimental results show that using the new pivot based extraction can increase the quality of bilingual corpus significantly and consequently improves the performance of the Persian-Italian SMT system.
Exact Approach for Survivable Regenerator Placement in Translucent WDM Networks
Venue: arXiv cs.NI 2017
Year: 2017

Most studies addressing translucent network design targeted a trade-off between minimizing the number of deployed regenerators and minimizing the number of regeneration sites. The latter highly depends on the carrier's strategy and is motivated by various considerations such as power consumption, maintenance and supervision costs. However, concentrating regenerators into a small number of nodes exposes the network to a high risk of data losses in the eventual case of regenerator pool failure. In this paper, we address the problem of survivable translucent network design taking into account the simultaneous effect of four transmission impairments. We propose an exact approach based on a mathematical formulation to solve the problem of regenerator placement while ensuring the network survivability in the hazardous event of a regenerator pool failure. For this purpose, for each accepted request requiring regeneration, the network management plane computes in advance several routing paths along with associated valid wavelengths going through different regeneration sites. In doing so, we target to implement an M : N shared regenerator pool protection scheme. Simulation results highlight the gain obtained by reducing the number of regeneration sites without sacrificing network survivability.
Computable Operations on Compact Subsets of Metric Spaces with Applications to Fréchet Distance and Shape Optimization
Venue: arXiv cs.LO 2017
Year: 2017

We extend the Theory of Computation on real numbers, continuous real functions, and bounded closed Euclidean subsets, to compact metric spaces $(X,d)$: thereby generically including computational and optimization problems over higher types, such as the compact 'hyper' spaces of (i) nonempty closed subsets of $X$ w.r.t. Hausdorff metric, and of (ii) equicontinuous functions on $X$. The thus obtained Cartesian closure is shown to exhibit the same structural properties as in the Euclidean case, particularly regarding function pre/image. This allows us to assert the computability of (iii) Fréchet Distances between curves and between loops, as well as of (iv) constrained/Shape Optimization.
A review on cloud robotics based frameworks to solve simultaneous localization and mapping (slam) problem
Venue: arXiv cs.RO 2017
Year: 2017

Cloud Robotics is one of the emerging area of robotics. It has created a lot of attention due to its direct practical implications on Robotics. In Cloud Robotics, the concept of cloud computing is used to offload computational extensive jobs of the robots to the cloud. Apart from this, additional functionalities can also be offered on run to the robots on demand. Simultaneous Localization and Mapping (SLAM) is one of the computational intensive algorithm in robotics used by robots for navigation and map building in an unknown environment. Several Cloud based frameworks are proposed specifically to address the problem of SLAM, DAvinCi, Rapyuta and C2TAM are some of those framework. In this paper, we presented a detailed review of all these framework implementation for SLAM problem.
Industrial Experience Report on the Formal Specification of a Packet Filtering Language Using the K Framework
Venue: arXiv cs.PL 2017
Year: 2017

Many project-specific languages, including in particular filtering languages, are defined using non-formal specifications written in natural languages. This leads to ambiguities and errors in the specification of those languages. This paper reports on an industrial experiment on using a tool-supported language specification framework (K) for the formal specification of the syntax and semantics of a filtering language having a complexity similar to those of real-life projects. This experimentation aims at estimating, in a specific industrial setting, the difficulty and benefits of formally specifying a packet filtering language using a tool-supported formal approach.
Extending a User Interface Prototyping Tool with Automatic MISRA C Code Generation
Venue: arXiv cs.SE 2017
Year: 2017

We are concerned with systems, particularly safety-critical systems, that involve interaction between users and devices, such as the user interface of medical devices. We therefore developed a MISRA C code generator for formal models expressed in the PVSio-web prototyping toolkit. PVSio-web allows developers to rapidly generate realistic interactive prototypes for verifying usability and safety requirements in human-machine interfaces. The visual appearance of the prototypes is based on a picture of a physical device, and the behaviour of the prototype is defined by an executable formal model. Our approach transforms the PVSio-web prototyping tool into a model-based engineering toolkit that, starting from a formally verified user interface design model, will produce MISRA C code that can be compiled and linked into a final product. An initial validation of our tool is presented for the data entry system of an actual medical device.
The KeYmaera X Proof IDE - Concepts on Usability in Hybrid Systems Theorem Proving
Venue: arXiv cs.LO 2017
Year: 2017

Hybrid systems verification is quite important for developing correct controllers for physical systems, but is also challenging. Verification engineers, thus, need to be empowered with ways of guiding hybrid systems verification while receiving as much help from automation as possible. Due to undecidability, verification tools need sufficient means for intervening during the verification and need to allow verification engineers to provide system design insights. This paper presents the design ideas behind the user interface for the hybrid systems theorem prover KeYmaera X. We discuss how they make it easier to prove hybrid systems as well as help learn how to conduct proofs in the first place. Unsurprisingly, the most difficult user interface challenges come from the desire to integrate automation and human guidance. We also share thoughts how the success of such a user interface design could be evaluated and anecdotal observations about it.
Model-based Classification and Novelty Detection For Point Pattern Data
Venue: arXiv cs.LG 2017
Year: 2017

Point patterns are sets or multi-sets of unordered elements that can be found in numerous data sources. However, in data analysis tasks such as classification and novelty detection, appropriate statistical models for point pattern data have not received much attention. This paper proposes the modelling of point pattern data via random finite sets (RFS). In particular, we propose appropriate likelihood functions, and a maximum likelihood estimator for learning a tractable family of RFS models. In novelty detection, we propose novel ranking functions based on RFS models, which substantially improve performance.
IFCIoT: Integrated Fog Cloud IoT Architectural Paradigm for Future Internet of Things
Venue: arXiv cs.DC 2017
Year: 2017

We propose a novel integrated fog cloud IoT (IFCIoT) architectural paradigm that promises increased performance, energy efficiency, reduced latency, quicker response time, scalability, and better localized accuracy for future IoT applications. The fog nodes (e.g., edge servers, smart routers, base stations) receive computation offloading requests and sensed data from various IoT devices. To enhance performance, energy efficiency, and real-time responsiveness of applications, we propose a reconfigurable and layered fog node (edge server) architecture that analyzes the applications' characteristics and reconfigure the architectural resources to better meet the peak workload demands. The layers of the proposed fog node architecture include application layer, analytics layer, virtualization layer, reconfiguration layer, and hardware layer. The layered architecture facilitates abstraction and implementation for fog computing paradigm that is distributed in nature and where multiple vendors (e.g., applications, services, data and content providers) are involved. We also elaborate the potential applications of IFCIoT architecture, such as smart cities, intelligent transportation systems, localized weather maps and environmental monitoring, and real-time agricultural data analytics and control.
Binary adaptive embeddings from order statistics of random projections
Venue: arXiv cs.LG 2017
Year: 2017

We use some of the largest order statistics of the random projections of a reference signal to construct a binary embedding that is adapted to signals correlated with such signal. The embedding is characterized from the analytical standpoint and shown to provide improved performance on tasks such as classification in a reduced-dimensionality space.