1,720,996 research outputs found
Composing FOCoRe Hybrid Automata
No full textThis paper addresses questions regarding the decidability ofhybrid automata that may be built hierarchically as is the case in many exemplar systems, be it natural or engineered. Parallel composition canbe considered a fundamental tool in such costructions. Somewhat surprisingly, this operation does not always preseve the decidability of reachability problem i.e., even if we prove the decidability of reachability overcomponent automata, we cannot guarantee the decidability over theirparallel composition. Despite these limitations, this paper provides a re-duction for the reachability problem over parallel composition of first-order constant reset automata (FOCoRe) to the satisfiability of a particular linear Diophantine system. Moreover, since such satisfiability problem have been proved decidable for systems with semi-algebraic coefficients,this paper presents an interesting class of hybrid automata for which the reachability problem of parallel composition is decidable. The resulting hybrid automata appear in systems biological modeling, and hence could be applied when one is interested in understanding a complex biological system composed of many smaller self-organizing systems
Decidability in robot manipulation planning
Full text linkConsider the problem of planning collision-free motion of n objects movable through contact with a robot that can autonomously translate in the plane and that can move a maximum of m ≤ n objects simultaneously. This represents the abstract formulation of a general class of manipulation planning problems that are proven to be decidable in this paper. The tools used for proving decidability of this simplified manipulation planning problem are, in fact, general enough to handle the decidability problem for the wider class of systems characterized by a stratified configuration space. These include, e.g., problems of legged and multi-contact locomotion, bi-manual manipulation. In addition, the approach described does not restrict the dynamics of the manipulation system modeled
Deception, identity, and security. The game theory of sybil attacks
No full textClassical mathematical game theory helps to evolve the emerging logic of identity in the cyber world
Inclusion dynamics hybrid automata
Full text linkHybrid systems are dynamical systems with the ability to describe mixed discrete-continuous evolution of a wide range of systems. Consequently, at first glance, hybrid systems appear powerful but recalcitrant, neither yielding to analysis and reasoning through a purely continuous-time modeling as with systems of differential equations, nor open to inferential processes commonly used for discrete state-transition systems such as finite state automata. A convenient and popular model, called hybrid automata, was introduced to model them and has spurred much interest on its tractability as a tool for inference and model checking in a general setting. Intuitively, a hybrid automaton is simply a "finite-state" automaton with each state augmented by continuous variables, which evolve according to a set of well-defined continuous laws, each specified separately for each state. This article investigates both the notion of hybrid automaton and the model checking problem over such a structure. In particular, it relates first-order theories and analysis results on multivalued maps and reduces the bounded reachability problem for hybrid automata whose continuous laws are expressed by inclusions (x ′ ∈ f (x, t)) to a decidability problem for first-order formulæ over the reals. Furthermore, the paper introduces a class of hybrid automata for which the reachability problem can be decided and shows that the problem of deciding whether a hybrid automaton belongs to this class can be again decided using first-order formulæ over the reals. Despite the fact that the bisimulation quotient for this class of hybrid automata can be infinite, we show that our techniques permit effective model checking for a nontrivial fragment of CTL. © 2008 Elsevier Inc. All rights reserved
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
Modular Development of Hybrid Systems for Verification in Coq
No full textIn this paper we present a formalization of the theory of hybrid automata and algorithms for building trajectory trees using module types and functors in the Coq proof assistan
Optimotaxis: A Stochastic Multi-agent on Site Optimization Procedure
No full textWe consider the problem of seeking the maximum of a scalar signal using a swarm of autonomous vehicles equipped with sensors that can take point measurements of the signal. Vehicles are not able to measure their current position or to communicate with each other. Our approach induces the vehicles to perform a biased random walk inspired by bacterial chemotaxis and controlled by a stochastic hybrid automaton. With such a controller, it is shown that the positions of the vehicles evolve towards a probability density that is a specified function of the spatial profile of the measured signal, granting higher vehicle densities near the signal maxima
Variations on the Author
Full text link“Variations on the Author” discusses two of Eduardo Coutinho’s recent films (Um Dia na Vida, from 2010, and Últimas Conversas, posthumously released in 2015) and their contribution to the general question of documentary authorship. The director’s filmography is characterized by a consistent yet self-effacing form of authorial self-inscription: Coutinho often features as an interviewer that rather than express opinions propels discourses; an interviewer that is good at listening. This mode of self-inscription characterizes him as an author who is not expressive but who is nonetheless markedly present on the screen. In Um Dia na Vida, however, Coutinho is completely absent form the image, while Últimas Conversas, on the contrary, includes a confessional prologue that moves the director from the margins to the center of his films. This article examines the ways in which these works stand out in the filmography of a director who offers new insights into the notion of cinematic authorship
- …
