004 Datenverarbeitung; Informatik
Refine
Year of publication
- 2011 (30) (remove)
Document Type
- Article (9)
- Doctoral Thesis (7)
- Working Paper (7)
- Conference Proceeding (2)
- Diploma Thesis (2)
- Bachelor Thesis (1)
- Book (1)
- Part of Periodical (1)
Has Fulltext
- yes (30)
Is part of the Bibliography
- no (30)
Keywords
- Deutschland (3)
- Digital Rights (2)
- Formale Semantik (2)
- Verifikation (2)
- (mobile) Internet (1)
- Analog Circuits (1)
- Analoges System (1)
- Analogschaltungen (1)
- Andreas Gebhard (1)
- Aufklärungsquote (1)
- Aufwandsschätzung (1)
- Automata theory (1)
- BigBrother Awards (1)
- CDU (1)
- Cost estimation (1)
- Data loss prevention (1)
- Data protection (1)
- Data security (1)
- Datenschutz (1)
- Depression (1)
- Digitale Gesellschaft (1)
- Diskrete Mathematik (1)
- Effort estimation (1)
- Elektronik (1)
- Entwicklungsprojekt (1)
- Entwurfsautomation (1)
- Facebook (1)
- Formal Verification (1)
- Formale Verifikation (1)
- Freiheit (1)
- Funktionale Programmierung (1)
- Google (1)
- Induktive Inferenz (1)
- Infinite games with perfect information (1)
- Informational self-determination (1)
- Internet (1)
- Internetnutzung (1)
- Kritik (1)
- Lambda-Kalkül (1)
- Logics (1)
- Logik (1)
- Machine learning (1)
- Markus Beckedahl (1)
- Nebenläufigkeit (1)
- NetzKultur (1)
- Netzaktivismus (1)
- Netzdebatte (1)
- Netzneutralität (1)
- Netzpolitik (1)
- Netzsperren (1)
- Netzzensur (1)
- NeuroXidence (1)
- Online privacy (1)
- Outlier detection (1)
- Parkinson Effekt (1)
- Parkinson effect (1)
- Pattern classification (1)
- Patternsprachen (1)
- Peter Tauber (1)
- Procrastination (1)
- Projektmanagement (1)
- Prokrastination (1)
- Pseudonym (1)
- Schätzwert (1)
- Self-fulfilling Prophecy (1)
- Semantics (1)
- Sicherheit (1)
- Software Engineering (1)
- Spiele (1)
- Sprachtheorie (1)
- Support Vector Machine (1)
- Theoretische Informatik (1)
- Transparenz (1)
- Vergessen (1)
- Verification (1)
- Vorratsdatenspeicherung (1)
- Web 2.0 (1)
- Zensur (1)
- Zensursula (1)
- algorithms (1)
- bivariate (1)
- combinatorics (1)
- data structures (1)
- descriptive patterns (1)
- deskriptive Pattern (1)
- fMRI (1)
- factor (1)
- grammar-based compression (1)
- hierarchies and reducibilities (1)
- inductive inference (1)
- joint-spike-event (1)
- logic (1)
- machine translation (1)
- modulation of synchrony (1)
- multivariate (1)
- natural language (1)
- pattern languages (1)
- randomized algorithms (1)
- re:publica (1)
- reactive systems (1)
- specification and verification (1)
- straight line programs (1)
- synchronous firing (1)
- verification (1)
In this paper we analyze the semantics of a higher-order functional language with concurrent threads, monadic IO and synchronizing variables as in Concurrent Haskell. To assure declarativeness of concurrent programming we extend the language by implicit, monadic, and concurrent futures. As semantic model we introduce and analyze the process calculus CHF, which represents a typed core language of Concurrent Haskell extended by concurrent futures. Evaluation in CHF is defined by a small-step reduction relation. Using contextual equivalence based on may- and should-convergence as program equivalence, we show that various transformations preserve program equivalence. We establish a context lemma easing those correctness proofs. An important result is that call-by-need and call-by-name evaluation are equivalent in CHF, since they induce the same program equivalence. Finally we show that the monad laws hold in CHF under mild restrictions on Haskell’s seq-operator, which for instance justifies the use of the do-notation.
This article shows that there exist two particular linear orders such that first-order logic with these two linear orders has the same expressive power as first-order logic with the Bit-predicate FO(Bit). As a corollary we obtain that there also exists a built-in permutation such that first-order logic with a linear order and this permutation is as expressive as FO(Bit).
From 12.12.2010 to 17.12.2010, the Dagstuhl Seminar 10501 "Advances and Applications of Automata on Words and Trees" was held in Schloss Dagstuhl - Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Seminar: 10501 - Advances and Applications of Automata on Words and Trees. The aim of the seminar was to discuss and systematize the recent fast progress in automata theory and to identify important directions for future research. For this, the seminar brought together more than 40 researchers from automata theory and related fields of applications. We had 19 talks of 30 minutes and 5 one-hour lectures leaving ample room for discussions. In the following we describe the topics in more detail.
Visual perception has increasingly grown important during the last decades in the robotics domain. Mobile robots have to localize themselves in known environments and carry out complex navigation tasks. This thesis presents an appearance-based or view-based approach to robot self-localization and robot navigation using holistic, spherical views obtained by cameras with large fields of view. For view-based methods, it is crucial to have a compressed image representation where different views can be stored and compared efficiently. Our approach relies on the spherical Fourier transform, which transforms a signal defined on the sphere to a small set of coefficients, approximating the original signal by a weighted sum of orthonormal basis functions, the so-called spherical harmonics. The truncated low order expansion of the image signal allows to compare input images efficiently, and the mathematical properties of spherical harmonics also allow for estimating rotation between two views, even in 3D. Since no geometrical measurements need to be done, modest quality of the vision system is sufficient. All experiments shown in this thesis are purely based on visual information to show the applicability of the approach. The research presented on robot self localization was focused on demonstrating the usability of the compressed spherical harmonics representation to solve the well-known kidnapped robot problem. To address this problem, the basic idea is to compare the current view to a set of images from a known environment to obtain a likelihood of robot positions. To localize the robot, one could choose the most probable position from the likelihood map; however, it is more beneficial to apply standard methods to integrate information over time while the robot moves, that is, particle or Kalman filters. The first step was to design a fast expansion method to obtain coefficient vectors directly in image space. This was achieved by back-projecting basis functions on the input image. The next steps were to develop a dissimilarity measure, an estimator for rotations between coefficient vectors, and a rotation-invariant dissimilarity measure, all of them purely based on the compact signal representation. With all these techniques at hand, generating likelihood maps is straightforward, but first experiments indicated strong dependence on illumination conditions. This is obviously a challenge for all holistic methods, in particular for a spherical harmonics approach, since local changes usually affect each single element of the coefficient vector. To cope with illumination changes, we investigated preprocessing steps leading to feature images (e.g. edge images, depth images), which bring together our holistic approach and classical feature-based methods. Furthermore, we concentrated on building a statistical model for typical changes of the coefficient vectors in presence of changes in illumination. This task is more demanding but leads to even better results. The second major topic of this thesis is appearance-based robot navigation. I present a view-based approach called Optical Rails (ORails), which leads a robot along a prerecorded track. The robot navigates in a network of known locations which are denoted as waypoints. At each waypoint, we store a compressed view representation. A visual servoing method is used to reach a current target waypoint based on the appearance and the current camera image. Navigating in a network of views is achieved by reaching a sequence of stopover locations, one after another. The main contribution of this work is a model which allows to deduce the best driving direction of the robot based purely on the coefficient vectors of the current and the target image. It is based on image registration as the classical method by Lucas-Kanade, but has been transferred to the spectral domain, which allows for great speedup. ORails also includes a waypoint selection strategy and a module for steering our nonholonomic robot. As for our self-localization algorithm, dependance on illumination changes is also problematic in ORails. Furthermore, occlusions have to be handled for ORails to work properly. I present a solution based on the optimal expansion, which is able to deal with incomplete image signals. To handle dynamic occlusions, i.e. objects appearing in an arbitrary region of the image, we use the linearity of the expansion process and cut the image into segments. These segments can be treated separately, and finally we merge the results. At this point, we can decide to disregard certain segments. Slicing the view allows for local illumination compensation, which is inherently non-robust if applied to the whole view. In conclusion, this approach allows to handle the most important criticism to holistic view-based approaches, that is, occlusions and illumination changes, and consequently improves the performance of Optical Rails.
Synchronous neuronal firing has been proposed as a potential neuronal code. To determine whether synchronous firing is really involved in different forms of information processing, one needs to directly compare the amount of synchronous firing due to various factors, such as different experimental or behavioral conditions. In order to address this issue, we present an extended version of the previously published method, NeuroXidence. The improved method incorporates bi- and multivariate testing to determine whether different factors result in synchronous firing occurring above the chance level. We demonstrate through the use of simulated data sets that bi- and multivariate NeuroXidence reliably and robustly detects joint-spike-events across different factors.
Correctness of program transformations in extended lambda calculi with a contextual semantics is usually based on reasoning about the operational semantics which is a rewrite semantics. A successful approach to proving correctness is the combination of a context lemma with the computation of overlaps between program transformations and the reduction rules.The method is similar to the computation of critical pairs for the completion of term rewriting systems. We describe an effective unification algorithm to determine all overlaps of transformations with reduction rules for the lambda calculus LR which comprises a recursive let-expressions, constructor applications, case expressions and a seq construct for strict evaluation. The unification algorithm employs many-sorted terms, the equational theory of left-commutativity modeling multi-sets, context variables of different kinds and a mechanism for compactly representing binding chains in recursive let-expressions. As a result the algorithm computes a finite set of overlappings for the reduction rules of the calculus LR that serve as a starting point to the automatization of the analysis of program transformations.
Online Privacy: Towards Informational Self-Determination on the Internet (Dagstuhl Perspectives Workshop 11061) : Simone Fischer-Hübner, Chris Hoofnagle, Kai Rannenberg, Michael Waidner, Ioannis Krontiris and Michael Marhöfer Self-Repairing Programs (Dagstuhl Seminar 11062) : Mauro Pezzé, Martin C. Rinard, Westley Weimer and Andreas Zeller Theory and Applications of Graph Searching Problems (Dagstuhl Seminar 11071) : Fedor V. Fomin, Pierre Fraigniaud, Stephan Kreutzer and Dimitrios M. Thilikos Combinatorial and Algorithmic Aspects of Sequence Processing (Dagstuhl Seminar 11081) : Maxime Crochemore, Lila Kari, Mehryar Mohri and Dirk Nowotka Packing and Scheduling Algorithms for Information and Communication Services (Dagstuhl Seminar 11091) Klaus Jansen, Claire Mathieu, Hadas Shachnai and Neal E. Young