Research in automating classical higher-order logic (HOL) has been on the rise for several years now and as a result, automated theorem provers for HOL, such as Satallax or LEO-II, are readily available. The area of application for these new tools is vast: The expressivity of the logic makes it easy to translate deduction problems of many facades into equialent problems in higher-order logic. This work is particularly concerned with solving problems in software verification, which can be addressed by, among others, the technique of model checking. In model checking, the state space of a program is insprected and exhaustively tested to whether it fulfils a certain property of interest or not. Such a property is commonly expressed in a verification logic, mostly temporal logics like LTL or CTL. We show how both the state space inspection and the verification logic can be embedded in HOL, and therefore how problems in model checking can be converted to problems for HOL theorem provers. The result is a verification software  which is not optimised for one specific verification logic, but can interpret program properties in an arbitrary logic, given an appropriate embedding in HOL. Furthermore, we present improvements for the current automated provers, which are required to treat such generated problems efficiently. These additions might also be highly relevant for problems in different domains and therefore thoroughly discussed.

Motion Capturing ist aus der heutigen Unterhaltungsindustrie nicht mehr wegzudenken. In den großen Film- und Videospiel-Produktionen kommt das Verfahren immer wieder zum Einsatz, wenn etwa CG-Charaktere realitätsnah animiert werden sollen. Das Motion Capture-System erfasst hierzu den Bewegungsablauf eines echten Darstellers und überträgt diesen auf die virtuelle Figur. Mit Microsofts "Kinect" existiert inzwischen eine kostengünstige Sensoreinheit, welche das Verfahren grundsätzlich auch einer breiten Masse zugänglich macht. Drehbewegungen oder Bewegungen am Boden (z.B. Hocke, Schneidersitz, usw.) führen einen einzelnen Tiefensensor jedoch schnell an seine Grenzen. Das Ziel der vorliegenden Arbeit besteht darin, diesen Problemen entgegenzuwirken und somit eine genauere Erkennung zu erzielen. Das Dreherkennungsproblem wird mithilfe eines zweiten  Kinect-Sensors gelöst. Das Problem bodennaher Bewegungen wird hingegen als Klassifizierungsproblem behandelt. Das im Rahmen dieser Arbeit entwickelte Programmm trainiert hierfür ein neuronales Netz unter Verwendung des Backpropagation-Algorithmus, wobei markante Erkennungsfehler der unterschiedlichen Posen die Klassifizierungsgrundlage bilden.

Wildfires pose a threat to naure and human health especially in the age of global warming. Their early detection is key to an effective fighting, because once a wildfire reaches a certain size it can be hardly controlled.

Consequently, automated wildfire detection systems have been developed to aid rangers in their work to prevent wildfire hazards. One of the most successful sysems was developed by the German aerospace center DLR (Deutsches Zentrum für Luft- und Raumfahrt) and relies on sophisticated hand-crafted feature. The algorithm behind this system is called fshell.

Convolutional neural networks (CNN) are specialized artificial neural networks that are the state-of-the-art for image recognition tasks. It is therefore investigated if these trainable models can be applied to the wildfire dectection problem to improve the performance of existing systems. Besides CNNs that use spatial features only, C3D networks that can also extract temporal features are considered. To tackle the detection of smoke in a larger image, a selective search variant was developed, that preselects regions of observable motion, which are then classified by the actual models.

The results clearly show that the trained networks learned to distinguish wildfire smoke from other objects, although they do not reach the fshell's performance. However, fshell makes use of additional prior knowledge whereas the CNNs rely on image data only. The results also show that C3D networks are the best performing single models, suggesting that the use of temporal features is important for accurate detection.

Am Fraunhofer Heinrich-Hertz-Institut wurde im Rahmen des TiMELab-Projektes ein immersives Projektionssystem mit 180°-Leinwand entwickelt. Das Herzstück des Systems stellt die CineBox dar. Es handelt sich dabei um ein Linux-basiertes Ausgabe- und Hostsystem für die am Fraunhofer HHI entwickelte CineCard, welche eine Echtzeitbildverarbeitung vornimmt. Unter anderem ist es Aufgabe der CineBox, eine Vorverarbeitung der zu projizierenden Videodaten vorzunehmen. Um den wachsenden Ansprüchen in Bezug auf die Auflösung der dargestellten Video- und Bilddaten und den damit verbundenen steigenden Datenmengen zu begegnen, wird derzeit eine Weiterentwicklung der CineCard durchgeführt. Für diese weiterentwickelte Version der CineCard wurde ein Programm entwickelt, dass die Vorverarbeitung der nötigen Daten realisiert.

Menschen lernen kontinuierlich, weil sie immer "angeschaltet" sind. Soll auch ein autonomer Roboter immer angeschaltet sein, muss er wissen, wie seine verschiedenen Verhaltensweisen zusammenhängen, damit er bewusst handeln kann. Beispielsweise muss ein Roboter im ununterbrochenen Betrieb regelmäßig in einen Zustand wechseln, in dem seine Akkus geladen werden. In der vorliegenden Arbeit wird eine Verhaltenssteuerung vorgestellt, die es dem humanoiden Roboter Myon ermöglicht, zwischen verschiedenen Verhaltensweisen wie Sitzen, Stehen und Laufen interaktiv zu wechseln, wodurch komplexe Bewegungsabfolgen möglich sind. Es wird demonstriert, wie der Roboter vom Sitzen über eine Aufstehbewegung ins Stehen gelangt, von dort aus eine Laufbewegung ausführen kann, wieder zurück ins Stehen wechselt und letztendlich durch eine Hinsetzbewegung wieder im Sitzen endet. Sowohl die einzelnen Bewegungen als auch die Übergänge zwischen ihnen werden detailliert dargestellt. Die Bewegungen zum Aufstehen und Hinsetzen sind so entworfen, dass eine Interaktion mit einem Anwender gezielt ausgenutzt wird. Für die Aufstehbewegung werden drei Varianten vorgestellt und diskutiert, wobei die Motoren bei einer Bewegung rein adaptiv geregelt werden. Die Übergänge zwischen den Bewegungen werden durch propriozeptive, auditive oder visuelle Signale ausgelöst.

American Football ist eine sehr taktisch geprägte Sportart, oft entscheiden nur wenige Yards ein Spiel. Umso wichtiger ist es, Statistiken und auch den Gegner zu analysieren. Da dies aber in Deutschland nur handschriftlich bzw. in vielen unterschiedlichen und veralteten Systemen passiert, können die Daten praktisch nicht genutzt werden. Als Lösung dieser Probleme wurde ein einheitliches System bestehend aus 4 iOS-Apps entwickelt, die sowohl für das Erheben der Daten als auch deren Auswertung zuständig sind. Alle Daten stehen für alle Apps bereit und können weitreichend ausgewertet werden. Der Trainer kann folglich anhand gespielter Spielzüge eine strategisch günstigere Auswahl der eigenen Spielzüge treffen

Für wissenschaftliche Texte, die heutzutage oft in digitaler Form angefertigt werden, benötigt man häufig Diagramme oder Modelle, welche sich jedoh bequemer und schneller mit der Hand gezeichnet anfertigen lassen. Eingescannt oder ab fotografiert sind diese Zeichnungen aber selten von so guter Qualität, dass sie sich nahtlos in ein digitales Dokument einfügen lassen. Im Rahmen dieser Arbeit wurde ein Programm entwickelt, das für das Erkennenn der einzelnen Formen eines Diagramms die generalisierte Hough-Transformation verwendet und das Diagramm mit einer Zeichenfunktion neu erstellt.

With the increase of computing power and computing possibilities, especially the rise of cloud computing, more and more data accumulates, commonly named Big Data. This development leads to the need of scalable algorithms. Machine learning always had an emphasis on scalability, but few well scaling algorithms are known. Often, this property is reached by approximation. In this thesis, through a well structured parallelization we enhance the Bump Boost and Multi Bump Boost algorithms. We show that with increasing data set sizes, the algorithms are able to reach almost perfect scalability. Furthermore, we investigate empirically how suitable Big-Data-frameworks, i.e. Apache Spark and Apache Flink, are for implementing Bump Boost and Multi Bump Boost.

The objective of advanced driver assistance systems (ADAS) in automobiles is to support the driver in his driving tasks and increase safety for all traffic participants. In this context, motion planning is responsible for the generation of feasible driving maneuvers.

The primary purpose of the thesis is to conceptualize and imiplement a planning system for highway driving scenarios. Based on environment and traffic, feasible driving maneuvers are planned and executed by the system. First, the vehicle and the environment are transferred into a phase space (positions, velocity, acceleration, time) to get an abstract model of the problem. Continuous paths, defined by their curvature as polynomial over arc length, describe the spatial movement of the car. Various acceleration profiles define how the paths are  followed. Complex maneuvers are achieved by combining trajectories. The behavior  of the vehicle is defined by cost components that evaluated aspects like lane and distance keeping  fo the trajectories. The planning system was integrated into an existing development and simulation framework for driver assistance systems.  The simulation results show, that the proposed systems is able to drive in highway scenarios. Relatively slower moving vehicles are being followed. Lane changes are planned and executed, when obastacles appear on the road.

In the domain of image based localization, alternatives to image feature based algorithms have been developed making use of similarity metrics that operate directly on pixel intensity values. These approaches can work robustly and efficiently in cases when the recognition process needs to deal for example with varying lighting conditions or changes in scenery detail. In addition to employing such a pixel based similarity metric a recent algorithm called OpenSeqSLAM processes image sequences instead of single images to improve the recognition. However OpenSeqSLAM is not robust in cases of perspective change. This makes it problematic to use in many robotic applications when the camera perspective is not fixed to certain positions with fixed orientations. In this contribution an approach is developed and evaluated that aims to mitigate the effect of perspective change on recognition performance by combining the concept of OpenSeqSLAM with an alternative similarity metric called tangent distance. It was further analyzed if the algorithm can be suitably designed to run on a humanoid robotic platform and how  it can utilize the robots capabilities. To enable evaluation a test application called Dream Viewer for image sequence based localization algorithms has been developed. In result of the first tests an adapted and heuristic version of the algorithm was developed and evaluated as well. This algorithm aims to run on hardware performance constraint robotic embedded systems. Developed algorithms were tested offline with recorded image data as well as online on a humanoid robot platform called Myon. Results indicated that the developed algorithms using tangent distance can perform superior in terms of recognition performance compared to the standard OpenSeqSLAM algorithm in the tested cased of perspective change.

Im Rahmen des BeesBook-Projektes fallen in Experimenten über 170 TB an Bildmaterial an. Aufgrund fehlender Kapazitäten, diese Datenmenge lokal zu speichern und auszuwerten, wird dafür ein Supercomputer des HLRN (Norddeutscher Verbund für Hoch- und Höchstleitsungsrechner) benutzt. Diese Arbeit entwickelt eine Schnittstelle zwischen den lokalen Computern und dem Supercomputer. Es wird ein System präsentiert, dass die Bilddaten in Echtzeit auf den Supercomputer überträgt. Auftretende Probleme in der Übertragung werden über einen Zwischenspeicher aufgefangen. Watchdogs sorgen dafür, dass das System zu jederzeit aktiv ist. Die 170 TB Daten aus dem Experiment sind mit diesem System aufgenommen worden. Ein zweites System sorgt dafür, dass die Ergebnisse vom Supercomputer in eine Datenbank überführt werden.  Die Datenbank ist so konzipiert, dass spezifische Anfragen in kurzer Zeit beantwortet werden können. Interfaces forgen für einen besseren Zugriff auf die Daten.

Brain computer interfaces (BCIs) are still not wide-spread. Compared to other means of control, they currently do not provide much usability. However, for highly motor-disabled people they are the only means of communication to the outside world. Using them to provide such people a way to command some devices, these devices could expand the abilities of a person. Thus, giving highly disabled people back some of their autonomy.

Considering the usually high price of recording technology necessary to build BCIs, this work examines the question, whether it is possible to also employ a consumer-priced EEG headset. Towards this goal an Emotiv EPOC EEG headset is used to design and build a proof-of-concept system that realises a BCI for arbitrary control over some device.

As a result, a prototype has been implemented that comprises analysis, transformation, and classification through a linear discriminant analysis of the recorded signals and that allows device control through the means of brain signals. In addition to the evaluation whether the concept is working, a number of possible further improvements and considerations are given in order to achieve a more mature state.

In dieser Arbeit wird ausgehend vom sogenannten ABC-Learning eine Situationserkennung für einen Roboter auf Basis sensomotorischer Daten realisiert. Dabei wird der Roboter inklusive seiner Umwelt als ein dynamisches System aufgefasst und die Einflüsse der verschiedenen Situationen auf dieses System untersucht. Anschließend wird das ABC-Learning um ein Verfahren ertweitert, das mittels Diffusionsprozessen diese Einflüsse erkennen und den entsprechenden Situationen zuordnen kann. Zusätzlich wird eine Modifikationn dieses Verfahrens erläutert und in den Auswertungen der Experimente gezeigt, dass diese zu einer deutlichen Verbesserung führt.