OpenRaiser/Intern-Atlas huggingface dataset:
Magneto-mechanical actuation model for fin-based locomotion
Venue: arXiv cs.RO 2011
Year: 2011

In this paper, we report the results from the analysis of a numerical model used for the design of a magnetic linear actuator with applications to fin-based locomotion. Most of the current robotic fish generate bending motion using rotary motors which implies at least one mechanical conversion of the motion. We seek a solution that directly bends the fin and, at the same time, is able to exploit the magneto-mechanical properties of the fin material. This strong fin-actuator coupling blends the actuator and the body of the robot, allowing cross optimization of the system's elements. We study a simplified model of an elastic element, a spring-mass system representing a flexible fin, subjected to nonlinear forcing, emulating magnetic interaction. The dynamics of the system is studied under unforced and periodic forcing conditions. The analysis is focused on the limit cycles present in the system, which allows the periodic bending of the fin and the generation of thrust. The frequency, maximum amplitude and center of the periodic orbits (offset of the bending) depend directly on the stiffness of the fin and the intensity of the forcing; we use this dependency to sketch a simple parameter controller. Although the model is strongly simplified, it provides means to estimate first values of the parameters for this kind of actuator and it is useful to evaluate the feasibility of minimal actuation control of such systems.
Graphical representation of covariant-contravariant modal formulae
Venue: arXiv cs.LO 2011
Year: 2011

Covariant-contravariant simulation is a combination of standard (covariant) simulation, its contravariant counterpart and bisimulation. We have previously studied its logical characterization by means of the covariant-contravariant modal logic. Moreover, we have investigated the relationships between this model and that of modal transition systems, where two kinds of transitions (the so-called may and must transitions) were combined in order to obtain a simple framework to express a notion of refinement over state-transition models. In a classic paper, Boudol and Larsen established a precise connection between the graphical approach, by means of modal transition systems, and the logical approach, based on Hennessy-Milner logic without negation, to system specification. They obtained a (graphical) representation theorem proving that a formula can be represented by a term if, and only if, it is consistent and prime. We show in this paper that the formulae from the covariant-contravariant modal logic that admit a "graphical" representation by means of processes, modulo the covariant-contravariant simulation preorder, are also the consistent and prime ones. In order to obtain the desired graphical representation result, we first restrict ourselves to the case of covariant-contravariant systems without bivariant actions. Bivariant actions can be incorporated later by means of an encoding that splits each bivariant action into its covariant and its contravariant parts.
Read Operators and their Expressiveness in Process Algebras
Venue: arXiv cs.LO 2011
Year: 2011

We study two different ways to enhance PAFAS, a process algebra for modelling asynchronous timed concurrent systems, with non-blocking reading actions. We first add reading in the form of a read-action prefix operator. This operator is very flexible, but its somewhat complex semantics requires two types of transition relations. We also present a read-set prefix operator with a simpler semantics, but with syntactic restrictions. We discuss the expressiveness of read prefixes; in particular, we compare them to read-arcs in Petri nets and justify the simple semantics of the second variant by showing that its processes can be translated into processes of the first with timed-bisimilar behaviour. It is still an open problem whether the first algebra is more expressive than the second; we give a number of laws that are interesting in their own right, and can help to find a backward translation.
Automatically Creating Design Models from 3D Anthropometry Data
Venue: arXiv cs.CG 2011
Year: 2011

When designing a product that needs to fit the human shape, designers often use a small set of 3D models, called design models, either in physical or digital form, as representative shapes to cover the shape variabilities of the population for which the products are designed. Until recently, the process of creating these models has been an art involving manual interaction and empirical guesswork. The availability of the 3D anthropometric databases provides an opportunity to create design models optimally. In this paper, we propose a novel way to use 3D anthropometric databases to generate design models that represent a given population for design applications such as the sizing of garments and gear. We generate the representative shapes by solving a covering problem in a parameter space. Well-known techniques in computational geometry are used to solve this problem. We demonstrate the method using examples in designing glasses and helmets.
Least Squares Temporal Difference Actor-Critic Methods with Applications to Robot Motion Control
Venue: arXiv cs.RO 2011
Year: 2011

We consider the problem of finding a control policy for a Markov Decision Process (MDP) to maximize the probability of reaching some states while avoiding some other states. This problem is motivated by applications in robotics, where such problems naturally arise when probabilistic models of robot motion are required to satisfy temporal logic task specifications. We transform this problem into a Stochastic Shortest Path (SSP) problem and develop a new approximate dynamic programming algorithm to solve it. This algorithm is of the actor-critic type and uses a least-square temporal difference learning method. It operates on sample paths of the system and optimizes the policy within a pre-specified class parameterized by a parsimonious set of parameters. We show its convergence to a policy corresponding to a stationary point in the parameters' space. Simulation results confirm the effectiveness of the proposed solution.
Stepping Lazy Programs
Venue: arXiv cs.PL 2011
Year: 2011

Debugging lazy functional programs poses serious challenges. In support of the "stop, examine, and resume" debugging style of imperative languages, some debugging tools abandon lazy evaluation. Other debuggers preserve laziness but present it in a way that may confuse programmers because the focus of evaluation jumps around in a seemingly random manner. In this paper, we introduce a supplemental tool, the algebraic program stepper. An algebraic stepper shows computation as a mathematical calculation. Algebraic stepping could be particularly useful for novice programmers or programmers new to lazy programming. Mathematically speaking, an algebraic stepper renders computation as the standard rewriting sequence of a lazy lambda-calculus. Our novel lazy semantics introduces lazy evaluation as a form of parallel program rewriting. It represents a compromise between Launchbury's store-based semantics and a simple, axiomatic description of lazy computation as sharing-via-parameters. Finally, we prove that the stepper's run-time machinery correctly reconstructs the standard rewriting sequence.
Supervised Rank Aggregation for Predicting Influence in Networks
Venue: arXiv cs.SI 2011
Year: 2011

Much work in Social Network Analysis has focused on the identification of the most important actors in a social network. This has resulted in several measures of influence and authority. While most of such sociometrics (e.g., PageRank) are driven by intuitions based on an actors location in a network, asking for the "most influential" actors in itself is an ill-posed question, unless it is put in context with a specific measurable task. Constructing a predictive task of interest in a given domain provides a mechanism to quantitatively compare different measures of influence. Furthermore, when we know what type of actionable insight to gather, we need not rely on a single network centrality measure. A combination of measures is more likely to capture various aspects of the social network that are predictive and beneficial for the task. Towards this end, we propose an approach to supervised rank aggregation, driven by techniques from Social Choice Theory. We illustrate the effectiveness of this method through experiments on Twitter and citation networks.
Algorithms for integrals of holonomic functions over domains defined by polynomial inequalities
Venue: arXiv cs.SC 2011
Year: 2011

We present an algorithm for computing a holonomic system for a definite integral of a holonomic function over a domain defined by polynomial inequalities. If the integrand satisfies a holonomic difference-differential system including parameters, then a holonomic difference-differential system for the integral can also be computed. In the algorithm, holonomic distributions (generalized functions in the sense of L. Schwartz) are inevitably involved even if the integrand is a usual function.
Une analyse basée sur la S-DRT pour la modélisation de dialogues pathologiques
Venue: arXiv cs.CL 2011
Year: 2011

In this article, we present a corpus of dialogues between a schizophrenic speaker and an interlocutor who drives the dialogue. We had identified specific discontinuities for paranoid schizophrenics. We propose a modeling of these discontinuities with S-DRT (its pragmatic part)
Encoding Phases using Commutativity and Non-commutativity in a Logical Framework
Venue: arXiv cs.CL 2011
Year: 2011

This article presents an extension of Minimalist Categorial Gram- mars (MCG) to encode Chomsky's phases. These grammars are based on Par- tially Commutative Logic (PCL) and encode properties of Minimalist Grammars (MG) of Stabler. The first implementation of MCG were using both non- commutative properties (to respect the linear word order in an utterance) and commutative ones (to model features of different constituents). Here, we pro- pose to adding Chomsky's phases with the non-commutative tensor product of the logic. Then we could give account of the PIC just by using logical prop- erties of the framework.
On the Quality of Wireless Network Connectivity
Venue: arXiv cs.NI 2011
Year: 2011

Despite intensive research in the area of network connectivity, there is an important category of problems that remain unsolved: how to measure the quality of connectivity of a wireless multi-hop network which has a realistic number of nodes, not necessarily large enough to warrant the use of asymptotic analysis, and has unreliable connections, reflecting the inherent unreliable characteristics of wireless communications? The quality of connectivity measures how easily and reliably a packet sent by a node can reach another node. It complements the use of \emph{capacity} to measure the quality of a network in saturated traffic scenarios and provides a native measure of the quality of (end-to-end) network connections. In this paper, we explore the use of probabilistic connectivity matrix as a possible tool to measure the quality of network connectivity. Some interesting properties of the probabilistic connectivity matrix and their connections to the quality of connectivity are demonstrated. We argue that the largest eigenvalue of the probabilistic connectivity matrix can serve as a good measure of the quality of network connectivity.
A convex formulation of strict anisotropic norm bounded real lemma
Venue: arXiv cs.SY 2011
Year: 2011

This paper is aimed at extending the H-infinity Bounded Real Lemma to stochastic systems under random disturbances with imprecisely known probability distributions. The statistical uncertainty is measured in entropy theoretic terms using the mean anisotropy functional. The disturbance attenuation capabilities of the system are quantified by the anisotropic norm which is a stochastic counterpart of the H-infinity norm. A state-space sufficient criterion for the anisotropic norm of a linear discrete time invariant system to be bounded by a given threshold value is derived. The resulting Strict Anisotropic Norm Bounded Real Lemma involves an inequality on the determinant of a positive definite matrix and a linear matrix inequality. It is shown that slight reformulation of these conditions allows the anisotropic norm of a system to be efficiently computed via convex optimization.
Deinterleaving Finite Memory Processes via Penalized Maximum Likelihood
Venue: arXiv cs.IT 2011
Year: 2011

We study the problem of deinterleaving a set of finite-memory (Markov) processes over disjoint finite alphabets, which have been randomly interleaved by a finite-memory switch. The deinterleaver has access to a sample of the resulting interleaved process, but no knowledge of the number or structure of the component Markov processes, or of the switch. We study conditions for uniqueness of the interleaved representation of a process, showing that certain switch configurations, as well as memoryless component processes, can cause ambiguities in the representation. We show that a deinterleaving scheme based on minimizing a penalized maximum-likelihood cost function is strongly consistent, in the sense of reconstructing, almost surely as the observed sequence length tends to infinity, a set of component and switch Markov processes compatible with the original interleaved process. Furthermore, under certain conditions on the structure of the switch (including the special case of a memoryless switch), we show that the scheme recovers \emph{all} possible interleaved representations of the original process. Experimental results are presented demonstrating that the proposed scheme performs well in practice, even for relatively short input samples.
Unit Testing in ASPIDE
Venue: arXiv cs.PL 2011
Year: 2011

Answer Set Programming (ASP) is a declarative logic programming formalism, which is employed nowadays in both academic and industrial real-world applications. Although some tools for supporting the development of ASP programs have been proposed in the last few years, the crucial task of testing ASP programs received less attention, and is an Achilles' heel of the available programming environments. In this paper we present a language for specifying and running unit tests on ASP programs. The testing language has been implemented in ASPIDE, a comprehensive IDE for ASP, which supports the entire life-cycle of ASP development with a collection of user-friendly graphical tools for program composition, testing, debugging, profiling, solver execution configuration, and output-handling.
The update complexity of selection and related problems
Venue: arXiv cs.DS 2011
Year: 2011

We present a framework for computing with input data specified by intervals, representing uncertainty in the values of the input parameters. To compute a solution, the algorithm can query the input parameters that yield more refined estimates in form of sub-intervals and the objective is to minimize the number of queries. The previous approaches address the scenario where every query returns an exact value. Our framework is more general as it can deal with a wider variety of inputs and query responses and we establish interesting relationships between them that have not been investigated previously. Although some of the approaches of the previous restricted models can be adapted to the more general model, we require more sophisticated techniques for the analysis and we also obtain improved algorithms for the previous model. We address selection problems in the generalized model and show that there exist 2-update competitive algorithms that do not depend on the lengths or distribution of the sub-intervals and hold against the worst case adversary. We also obtain similar bounds on the competitive ratio for the MST problem in graphs.
Parsing Combinatory Categorial Grammar with Answer Set Programming: Preliminary Report
Venue: arXiv cs.AI 2011
Year: 2011

Combinatory categorial grammar (CCG) is a grammar formalism used for natural language parsing. CCG assigns structured lexical categories to words and uses a small set of combinatory rules to combine these categories to parse a sentence. In this work we propose and implement a new approach to CCG parsing that relies on a prominent knowledge representation formalism, answer set programming (ASP) - a declarative programming paradigm. We formulate the task of CCG parsing as a planning problem and use an ASP computational tool to compute solutions that correspond to valid parses. Compared to other approaches, there is no need to implement a specific parsing algorithm using such a declarative method. Our approach aims at producing all semantically distinct parse trees for a given sentence. From this goal, normalization and efficiency issues arise, and we deal with them by combining and extending existing strategies. We have implemented a CCG parsing tool kit - AspCcgTk - that uses ASP as its main computational means. The C&C supertagger can be used as a preprocessor within AspCcgTk, which allows us to achieve wide-coverage natural language parsing.
Optimization of Lyapunov Invariants in Verification of Software Systems (Extended Version)
Venue: arXiv cs.SY 2011
Year: 2011

The paper proposes a control-theoretic framework for verification of numerical software systems, and puts forward software verification as an important application of control and systems theory. The idea is to transfer Lyapunov functions and the associated computational techniques from control systems analysis and convex optimization to verification of various software safety and performance specifications. These include but are not limited to absence of overflow, absence of division-by-zero, termination in finite time, presence of dead-code, and certain user-specified assertions. Central to this framework are Lyapunov invariants. These are properly constructed functions of the program variables, and satisfy certain properties-resembling those of Lyapunov functions-along the execution trace. The search for the invariants can be formulated as a convex optimization problem. If the associated optimization problem is feasible, the result is a certificate for the specification.
Datum-Wise Classification: A Sequential Approach to Sparsity
Venue: arXiv cs.AI 2011
Year: 2011

We propose a novel classification technique whose aim is to select an appropriate representation for each datapoint, in contrast to the usual approach of selecting a representation encompassing the whole dataset. This datum-wise representation is found by using a sparsity inducing empirical risk, which is a relaxation of the standard L 0 regularized risk. The classification problem is modeled as a sequential decision process that sequentially chooses, for each datapoint, which features to use before classifying. Datum-Wise Classification extends naturally to multi-class tasks, and we describe a specific case where our inference has equivalent complexity to a traditional linear classifier, while still using a variable number of features. We compare our classifier to classical L 1 regularized linear models (L 1-SVM and LARS) on a set of common binary and multi-class datasets and show that for an equal average number of features used we can get improved performance using our method.
Probability Ranking in Vector Spaces
Venue: arXiv cs.IR 2011
Year: 2011

The Probability Ranking Principle states that the document set with the highest values of probability of relevance optimizes information retrieval effectiveness given the probabilities are estimated as accurately as possible. The key point of the principle is the separation of the document set into two subsets with a given level of fallout and with the highest recall. The paper introduces the separation between two vector subspaces and shows that the separation yields a more effective performance than the optimal separation into subsets with the same available evidence, the performance being measured with recall and fallout. The result is proved mathematically and exemplified experimentally.
A Constraint Logic Programming Approach for Computing Ordinal Conditional Functions
Venue: arXiv cs.AI 2011
Year: 2011

In order to give appropriate semantics to qualitative conditionals of the form "if A then normally B", ordinal conditional functions (OCFs) ranking the possible worlds according to their degree of plausibility can be used. An OCF accepting all conditionals of a knowledge base R can be characterized as the solution of a constraint satisfaction problem. We present a high-level, declarative approach using constraint logic programming techniques for solving this constraint satisfaction problem. In particular, the approach developed here supports the generation of all minimal solutions; these minimal solutions are of special interest as they provide a basis for model-based inference from R.
Show Me Your Cookie And I Will Tell You Who You Are
Venue: arXiv cs.CR 2011
Year: 2011

With the success of Web applications, most of our data is now stored on various third-party servers where they are processed to deliver personalized services. Naturally we must be authenticated to access this personal information, but the use of personalized services only restricted by identification could indirectly and silently leak sensitive data. We analyzed Google Web Search access mechanisms and found that the current policy applied to session cookies could be used to retrieve users' personal data. We describe an attack scheme leveraging the search personalization (based on the same SID cookie) to retrieve a part of the victim's click history and even some of her contacts. We implemented a proof of concept of this attack on Firefox and Chrome Web browsers and conducted an experiment with ten volunteers. Thanks to this prototype we were able to recover up to 80% of the user's search click history.
Improving Entity Resolution with Global Constraints
Venue: arXiv cs.DB 2011
Year: 2011

Some of the greatest advances in web search have come from leveraging socio-economic properties of online user behavior. Past advances include PageRank, anchor text, hubs-authorities, and TF-IDF. In this paper, we investigate another socio-economic property that, to our knowledge, has not yet been exploited: sites that create lists of entities, such as IMDB and Netflix, have an incentive to avoid gratuitous duplicates. We leverage this property to resolve entities across the different web sites, and find that we can obtain substantial improvements in resolution accuracy. This improvement in accuracy also translates into robustness, which often reduces the amount of training data that must be labeled for comparing entities across many sites. Furthermore, the technique provides robustness when resolving sites that have some duplicates, even without first removing these duplicates. We present algorithms with very strong precision and recall, and show that max weight matching, while appearing to be a natural choice turns out to have poor performance in some situations. The presented techniques are now being used in the back-end entity resolution system at a major Internet search engine.
No Internal Regret via Neighborhood Watch
Venue: arXiv cs.LG 2011
Year: 2011

We present an algorithm which attains O(\sqrt{T}) internal (and thus external) regret for finite games with partial monitoring under the local observability condition. Recently, this condition has been shown by (Bartok, Pal, and Szepesvari, 2011) to imply the O(\sqrt{T}) rate for partial monitoring games against an i.i.d. opponent, and the authors conjectured that the same holds for non-stochastic adversaries. Our result is in the affirmative, and it completes the characterization of possible rates for finite partial-monitoring games, an open question stated by (Cesa-Bianchi, Lugosi, and Stoltz, 2006). Our regret guarantees also hold for the more general model of partial monitoring with random signals.