004 Datenverarbeitung; Informatik
Filtern
Erscheinungsjahr
Dokumenttyp
- Dissertation (48) (entfernen)
Schlagworte
- Software Engineering (4)
- Information Retrieval (3)
- model-based (3)
- Abduktion <Logik> (2)
- Maschinelles Lernen (2)
- Modellgetriebene Entwicklung (2)
- Petri-Netz (2)
- Visualisierung (2)
- 3D Modell Referenz Bildsynthese (1)
- AUTOSAR (1)
Die Suche nach wissenschaftlicher Literatur ist eine Forschungsherausforderung für das Information Retrieval im besonderen Umfeld der digitalen Bibliotheken. Aktuelle Nutzerstudien zeigen, dass im klassischen IR-Modell zwei typische Schwächen auszumachen sind: das Ranking der gefundenen Dokumente und Probleme bei der Formulierung von Suchanfragen. Gleichzeitig ist zu sehen, dass traditionelle Retrievalsysteme, die primär textuelle Dokument- und Anfragemerkmale nutzen, bei IR-Evaluationskampagnen wie TREC und CLEF in ihrer Leistung seit Jahren stagnieren.
Zwei informetrisch-motivierte Verfahren zur Suchunterstützung werden vorgestellt und mittels einer Laborevaluation mit den beiden IR-Testkollektionen GIRT und iSearch sowie 150 und 65 Topics evaluiert. Die Verfahren sind: (1) eine auf der Kookkurrenz von Dokumentattributen basierende Anfrageerweiterung und (2) ein Rankingansatz, der informetrische Beobachtungen zur Produktivität von Informationserzeugern ausnutzt. Beide Verfahren wurden mit einer Referenzimplementation auf Basis der Suchmaschine Solr verglichen. Beide Verfahren zeigen positive Effekte beim Einsatz von zusätzlichen Dokumentattributen wie Autorennamen, ISSN-Codes und kontrollierten Schlagwörtern. Bei der Anfrageerweiterung konnte ein positiver Effekt in Form einer Verbesserung der Precision (bpref +12%) und des Recall (R +22%) erzielt werden. Die alternativen Rankingansätze konnten beim Ansatz von Autorennamen und ISSN-Codes die Baseline erreichen bzw. diese beim Einsatz der kontrollierten Schlagwörter über- treffen (MAP +14%). Einen negativen Einfluss auf das Ranking hatten allerdings die Einbeziehung von Faktoren wie Verlagsnamen oder Erscheinungsorten. Für beide Verfahren konnte eine substantiell andere Sortierung der Ergebnismenge, gemessen anhand von Kendalls, beobachtet werden. Zusätzlich zu der verbesserten Relevanz der Ergebnisliste kann der Nutzer so eine neue Sicht auf die Dokumentenmenge gewinnen.
Die Anfrageerweiterung mit Autorennamen, ISSN-Codes und Thesaurustermen zeigt das bisher ungenutzte Potential, das sich in digitalen Bibliotheken durch die Datenfülle und -qualität ergibt. Die Rankingverfahren konnten die Leistung des Baseline-Systems übertreffen, nachdem eine Überprüfung auf Vorliegen einer Power Law-Verteilung und eine anschließende Filterung durchgeführt wurde. Dies zeigt, dass die Rankingverfahren nicht universell für alle Suchanfragen anwendbar sind, sondern ein Vorhandensein bestimmter Häufigkeitsverteilungen voraussetzen. So wird die enge Verbindung der Verfahren zu informetrischen Gesetzmäßigkeiten wie Bradfords, Lotkas oder Zipfs Gesetz deutlich. Die beiden in der Arbeit evaluierten Verfahren sind als interaktive Suchunterstützungsdienste in der sozialwissenschaftlichen digitalen Bibliothek Sowiport implementiert. Die Verfahren lassen sich über entsprechende Web- Schnittstellen auch in anderen Anwendungskontexten einsetzen.
Leichte Sprache (LS) ist eine vereinfachte Varietät des Deutschen in der barrierefreie Texte für ein breites Spektrum von Menschen, einschließlich gering literalisierten Personen mit Lernschwierigkeiten, geistigen oder entwicklungsbedingten Behinderungen (IDD) und/oder komplexen Kommunikationsbedürfnissen (CCN), bereitgestellt werden. LS-Autor*innen sind i.d.R. der deutschen Standardsprache mächtig und gehören nicht der genannten Personengruppe an. Unser Ziel ist es, diese zu befähigen, selbst am schriftlichen Diskurs teilzunehmen. Hierfür bedarf es eines speziellen Schreibsystems, dessen linguistische Unterstützung und softwareergonomische Gestaltung den spezifischen Bedürfnissen der Zielgruppe gerecht wird. EasyTalk ist ein System basierend auf computerlinguistischer Verarbeitung natürlicher Sprache (NLP) für assistives Schreiben in einer erweiterten Variante von LS (ELS). Es stellt den Nutzenden ein personalisierbares Vokabular mit individualisierbaren Kommunikationssymbolen zur Verfügung und unterstützt sie entsprechend ihres persönlichen Fähigkeitslevels durch interaktive Benutzerführung beim Schreiben. Intuitive Formulierungen für linguistische Entscheidungen minimieren das erforderliche grammatikalische Wissen für die Erstellung korrekter und kohärenter komplexer Inhalte. Einfache Dialoge kommunizieren mit einem natürlichsprachlichen Paraphrasengenerator, der kontextsensitiv Vorschläge für Satzkomponenten und korrekt flektierte Wortformen bereitstellt. Außerdem regt EasyTalk die Nutzer*innen an, Textelemente hinzuzufügen, welche die Verständlichkeit des Textes für dessen Leserschaft fördern (z.B. Zeit- und Ortsangaben) und die Textkohärenz verbessern (z.B. explizite Diskurskonnektoren). Um das System auf die Bedürfnisse der Zielgruppe zuzuschneiden, folgte die Entwicklung von EasyTalk den Grundsätzen der menschzentrierten Gestaltung (UCD). Entsprechend wurde das System in iterativen Entwicklungszyklen ausgereift, kombiniert mit gezielten Evaluierungen bestimmter Aspekte durch Gruppen von Expert*innen aus den Bereichen CCN, LS und IT sowie L2-Lernende der deutschen Sprache. Eine Fallstudie, in welcher Mitglieder der Zielgruppe das freie Schreiben mit dem System testeten, bestätigte, dass Erwachsene mit geringen Lese-, Schreib- und Computerfähigkeiten mit IDD und/oder CCN mit EasyTalk eigene persönliche Texte in ELS verfassen können. Das positive Feedback aller Tests inspiriert Langzeitstudien mit EasyTalk und die Weiterentwicklung des prototypischen Systems, wie z.B. die Implementierung einer s.g. Schreibwerkstatt.
Folksonomien sind Web 2.0 Plattformen, in denen Benutzer verschiedene Inhalte miteinander teilen können. Die Inhalte können mit Hilfe von Stichwörtern, den sogenannten Tags, kategorisiert und organisiert werden. Die verschiedenen Folksonomien unterstützen unterschiedliche Inhaltstypen wie zum Beispiel Webseiten (Delicious), Bilder (Flickr) oder Videos (YouTube). Aufgrund ihrer einfachen Benutzungsweise haben Folksonomien viele Millionen Benutzer. Die einfache Benutzungsweise führt aber auch zu einigen Problemen. Diese Doktorarbeit beschäftigt sich mit drei der wichtigsten Probleme und beschreibt Methoden, wie sie gelöst werden können. Das erste dieser Probleme tritt auf, wenn Benutzer die Folksonomien nach bestimmten Inhalten durchsuchen wollen. Häufig können dabei nicht alle relevanten Inhalte gefunden werden, da diesen relevante Stichwörter fehlen. Dementsprechend tritt das zweite Problem während der Vergabe von Stichwörtern auf. Manche Folksonomien, wie zum Beispiel Delicious, unterstützen ihre Benutzer dabei, indem sie ihnen mögliche Stichwörter empfehlen. Andere Folksonomien, wie zum Beispiel Flickr, bieten keine solche Unterstützung. Die Empfehlung von Stichwörtern hilft dem Benutzer dabei, Inhalte auf einfache Art und Weise mit den jeweils relevanten Stichwörtern zu versehen. Das dritte Problem besteht darin, dass weder Stichwörter noch Inhalte mit einer festen Semantik versehen sind und mehrdeutig sein können. Das Problem entsteht dadurch, dass die Benutzer die Stichwörter vollkommen frei rnverwenden können. Die automatische Identifizierung der Semantik von Stichwörtern und Inhalten hilft dabei, die dadurch entstehenden Probleme zu reduzieren. Diese Doktorarbeit stellt mehrere Methoden vor, wie verschiedene Quellen für semantische Informationen benutzt werden können, um die vorher genannten drei Probleme zu lösen. In dieser Doktorarbeit benutzen wir als Quellen Internetsuchmaschinen, soziale Netzwerke im Internet und die gemeinsamen Vorkommen von Stichwörtern in Folksonomien. Die Verwendung der verschiedenen Quellen reduziert den Aufwand bei der Erstellung von Systemen, die die vorher genannten Probleme lösen. Die vorgestellten Methoden wurden auf einem großen Datensatz evaluiert. Die erzielten Ergebnisse legen nahe, dass semantische Informationen bei der Lösung der Probleme helfen, die während der Suche von Inhalten, der Empfehlung von Stichwörtern als auch der automatischen Identifizierung der Semantik von Stichwörtern und Inhalten auftreten.
In den letzten Jahren konzentrierte sich das E-Government auf die administrativen Aspekte der Verwaltungsmodernisierung. Im nächsten Schritt werden die E-Diskurse als Instrument der Bürgernähe und Mittel der E-Demokratie/E-Partizipation an Bedeutung gewinnen. Mit zunehmender Akzeptanz solcher E-Diskurse werden diese schnell eine Komplexität erreichen, die von den Teilnehmern nicht mehr zu bewältigen ist. Das Problem liegt in der eingeschränkten Möglichkeit, einen in Raum und Zeit verteilten Diskurs zu verfolgen und sich ein Bild von ihm zu machen. Viele Eindrücke, die sich aus Präsenzdiskussionen gewinnen lassen, fehlen. Deswegen hat die vorliegende Arbeit die Zielsetzung der Konzeption und der prototypischen Implementierung eines Instrumentariums (Diskursmeter), womit sich die Teilnehmer, insbesondere die Moderatoren, des E-Diskurses jederzeit einen Überblick über den E-Diskurs schaffen können und so zu ihrem Diskursverständnis (Discourse Awareness) zu gelangen. Über das aktuelle Geschehen im E-Diskurs informiert die gegenwartsorientierte und über das vergangene Geschehen die vergangenheitsorientierte Discourse Awareness, über die etwaige Trends sichtbar sind. Der Fokus der Discourse Awareness liegt in der quantitativen Betrachtung des Geschehens im E-Diskurs. Aus dem in dieser Arbeit entwickelten Modell des E-Diskurses resultieren die Fragestellungen zur Discourse Awareness, deren Konkretisierung Grundlage für die Implementierung des Diskursmeters ist. Die an das Modell des E-Diskurses angebrachten Diskurssensoren zeichnen das Geschehen im E-Diskurs auf, die zu Diskursereignissen führen, die das Diskursmeter in unterschiedlichen Visualisierungsformen präsentiert. Den Moderatoren des E-Diskurses bietet das Diskursmeter die gegenwartsorientierte Discourse Awareness als Monitoring und die vergangenheitsorientierte Discourse Awareness als Abfrage (quantitative Analyse) an.
Die weltweite Vernetzung von semantischen Information schreitet stetig voran und erfährt mit der Linked Data Initiative immer mehr Aufmerksamkeit. Bei Linked Data werden verschiedene Datensätze aus unterschiedlichen Domänen und von diversen Anbietern in einem einheitlichen Format (RDF) zur Verfügung gestellt und miteinander verknüpft. Strukturell ist das schnell wachsende Linked Data Netzwerk sehr ähnlich zum klassischen World Wide Web mit seinen verlinkten HTML Seiten. Bei Linked Data handelt es sich jedoch um URI-referenzierte Entitäten, deren Eigenschaften und Links durch RDF-Triple ausgedrückt werden. Neben dem Dereferenzieren von URIs besteht mit SPARQL auch die Möglichkeit, ähnlich wie bei Datenbanken, komplexe algebraische Anfragen zu formulieren und über sogenannte SPARQL Endpoints auf einer Datenquelle auswerten zu lassen. Eine SPARQL Anfrage über mehrere Linked Data Quellen ist jedoch kompliziert und bedarf einer föderierten Infrastruktur in der mehrere verteilte Datenquellen integriert werden, so dass es nach außen wie eine einzige große Datenquelle erscheint. Die Föderation von Linked Data hat viele Ähnlichkeiten mit verteilten und föderierten Datenbanken. Es gibt aber wichtige Unterschiede, die eine direkte Adpation von bestehenden Datenbanktechnologien schwierig machen. Dazu gehört unter anderem die große Anzahl heterogener Datenquellen in der Linked Data Cloud, Beschränkungen von SPARQL Endpoints, und die teils starke Korrelation in den RDF Daten. Daher befasst sich die vorliegende Arbeit primär mit der Optimierung von verteilten SPARQL Anfragen auf föderierten RDF Datenquellen. Die Grundlage dafür ist SPLENDID, ein effizientes Optimierungverfahren für die Ausführung von verteilten SPARQL Anfragen in einer skalierbaren und flexiblen Linked Data Föderationsinfrastruktur. Zwei Aspekte sind dabei besonders wichtig: die automatische Auswahl von passenden Datenquellen für beliebige SPARQL Anfragen und die Berechnung des optimalen Ausführungsplans (Join Reihenfolge) basierend auf einem Kostenmodell. Die dafür erforderlichen statistischen Information werden mit Hilfe von VOID-basierten Datenquellenbeschreibungen zur Verfügung gestellt. Darüberhinaus wird auch des Management verteilter statistischer Daten untersucht und eine Benchmark-Methodologie
Soziale Netzwerke sind allgegenwärtige Strukturen, die wir jeden Tag generieren und bereichern, während wir uns über Plattformen der sozialen Medien, E-Mails und jede andere Art von Interaktion mit Menschen verbinden. Während diese Strukturen für uns nicht greifbar sind, sind sie sehr wichtige Informationsträger. Zum Beispiel kann die politische Neigung unserer Freunde ein Näherungswert sein, um unsere eigenen politischen Präferenzen zu identifizieren. Gleichermaßen
kann die Kreditwürdigkeit unserer Freunde entscheidend bei der Gewährung oder Ablehnung unserer eigenen Kredite sein. Diese Erklärungskraft wird bei der Gesetzgebung, bei Unternehmensentscheidungen und in der Forschung genutzt, da sie maschinellen Lerntechniken hilft, genaue Vorhersagen zu treffen. Diese Verallgemeinerungen kommen jedoch häufig nur der Mehrheit der Menschen zugute, welche die allgemeine Struktur des Netzwerks prägen, und benachteiligen unterrepräsentierte Gruppen, indem sie ihre Mittel und Möglichkeiten begrenzen. Daher ist es wichtig zuerst zu verstehen, wie sich soziale Netzwerke bilden, um dann zu überprüfen, inwieweit ihre Mechanismen der Kantenbildung dazu beitragen, soziale Ungleichheiten in Algorithmen des maschinellen Lernens zu verstärken.
Zu diesem Zweck schlage ich im ersten Teil dieser Arbeit HopRank und Janus vor, zwei Methoden um die Mechanismen der Kantenbildung in realen ungerichteten sozialen Netzwerken zu charakterisieren. HopRank ist ein Modell der Daten-Hamsterei in Netzwerken. Sein Schlüsselkonzept ist ein gezinkter zufälliger Wanderer, der auf Übergangswahrscheinlichkeiten zwischen K-Hop-Nachbarschaften basiert. Janus ist ein Bayessches Rahmenwerk, mit dem wir plausible Hypothesen der Kantenbildung in Fällen identifizieren und bewerten können, in denen Knoten zusätzliche Daten enthalten. Im zweiten Teil dieser Arbeit untersuche ich die Auswirkungen dieser Mechanismen - welche die Kantenbildung in sozialen Netzwerken erklären - auf das maschinelle Lernen. Insbesondere untersuche ich den Einfluss von Homophilie, bevorzugter Bindung, Kantendichte, Anteil von Minderheiten und der Richtung von Verbindungen sowohl auf Leistung als auch auf systematische Fehler von kollektiver Klassifizierung und auf die Sichtbarkeit von Minderheiten in Top-K-Rängen. Meine Ergebnisse zeigen eine starke Korrelation zwischen der Netzwerkstruktur und den Ergebnissen des maschinellen Lernens. Dies legt nahe, dass die systematische Diskriminierung spezieller Personen: (i) durch den Netzwerktyp vorweggenommen und (ii) durch strategisches Verbinden im Netzwerk verhindert werden kann.
Mit der zunehmenden Verbreitung digitaler Kameras nimmt die Anzahl der aufgenommen Fotos drastisch zu. Fotos werden sowohl für den privaten Gebrauch aufgenommen und auf eigenen Festplatten gespeichert, als auch im Internet verbreitet. Die Verwaltung dieser großen Datenmengen stellt eine Herausforderung dar, bei der Benutzer zunehmend unterstützt werden müssen. Die automatische Analyse von Bildinhalten anhand von Algorithmen ist ein ungelöstes Problem und kann kaum die Bedürfnisse menschlicher Nutzer erfüllen. Daher werden häufig Metainformationen genutzt, um z.B. abgebildete Szenen textuell zu beschreiben oder Bewertungen zu Fotos zu speichern. Im Rahmen dieser Arbeit wird untersucht, wie diese Metainformationen ohne zusätzlichen Aufwand für Benutzer generiert werden können. Dazu werden Augenbewegungen von Benutzern mit einem Eyetrackinggerät erfasst und die daraus abgeleitete visuelle Aufmerksamkeit als Informationsquelle genutzt.
Aufgrund von fallenden Hardwarepreisen bei gleichzeitig zunehmender Konkurrenz sind die Preise für Eyetracker in den letzten Jahren stark gefallen und ihre Bedienbarkeit wurde vereinfacht. Es wird angenommen, dass die Erfassung von Blickdaten bald mit alltäglichen Geräten wie Laptops möglich sein wird, während Benutzer z.B. verschiedenen Beschäftigungen mit digitalen Bildern nachgehen. Die Auswertung dieser Blickinformationen erlaubt es, Informationen ohne zusätzlichen Aufwand für den Menschen bereitzustellen.
Im ersten Teil dieser Arbeit wird untersucht, ob durch die Auswertung von Blickinformationen, Schlagworte Bildregionen zugewiesen werden können, mit dem Ziel abgebildete Szenen zu beschreiben. Insgesamt wurden drei Experimente durchgeführt um die Qualität der Beschreibungen zu untersuchen. Im ersten Experiment entschieden Teilnehmer durch das Drücken bestimmter Tasten, ob ein gegebenes Objekt auf einem Foto zu sehen war. In der zweiten Studie suchten Benutzer mit einer simulierten Bildersuche nach Fotos von bestimmten Objekten. Im dritten Experiment klassifizierten Benutzer Fotos bezüglich gegebener Objektnamen in einem eyetracking-gesteuerten Spiel. In jedem Experiment wurden die Augenbewegungen aufgezeichnet und die Objektnamen bzw. Suchbegriffe entsprechenden Bildregionen zugeordnet. Die Ergebnisse zeigen, dass in den verschiedenen Anwendungen Bildinhalte durch Blickpfadanalysen sinnvoll beschrieben werden können. Im zweiten Teil wird die Identifizierung von interessanten Fotos in einer Sammlung von Fotos anhand von Blickbewegungen erforscht, mit dem Ziel, Benutzern individuelle Fotoauswahlen anzubieten, nachdem sie Fotos in einer Sammlung betrachtet haben. Durch den Vergleich der unter Einbeziehung der visuellen Aufmerksamkeit automatisch erstellten Auswahlen mit manuell von den Benutzer erstellten Auswahlen, wird das Potential von Blickinformation in der Erkennung wichtiger Fotos deutlich.
Die Ergebnisse dieser Arbeit zeigen das große und bisher ungenutzte Potential der impliziten Nutzung von Blickdaten. Es kann von menschlichen Fähigkeiten profitiert werden, besonders dort, wo Algorithmen die menschliche Wahrnehmung noch lange nicht simulieren können.
Software is vital for modern society. The efficient development of correct and reliable software is of ever-growing importance. An important technique to achieve this goal is deductive program verification: the construction of logical proofs that programs are correct. In this thesis, we address three important challenges for deductive verification on its way to a wider deployment in the industry: 1. verification of thread-based concurrent programs 2. correctness management of verification systems 3. change management in the verification process. These are consistently brought up by practitioners when applying otherwise mature verification systems. The three challenges correspond to the three parts of this thesis (not counting the introductory first part, providing technical background on the KeY verification approach). In the first part, we define a novel program logic for specifying correctness properties of object-oriented programs with unbounded thread-based concurrency. We also present a calculus for the above logic, which allows verifying actual Java programs. The calculus is based on symbolic execution resulting in its good understandability for the user. We describe the implementation of the calculus in the KeY verification system and present a case study. In the second part, we provide a first systematic survey and appraisal of factors involved in reliability of formal reasoning. We elucidate the potential and limitations of self-application of formal methods in this area and give recommendations based on our experience in design and operation of verification systems. In the third part, we show how the technique of similarity-based proof reuse can be applied to the problems of industrial verification life cycle. We address issues (e.g., coping with changes in the proof system) that are important in verification practice, but have been neglected by research so far.
Die Arbeit beschäftigt sich mit dem Einsatz moderner Grafikhardware (GPU) für die Visualisierung und Verarbeitung medizinischer Volumendaten. Die zunehmende Steigerung der Rechenleistung ermöglicht den Einsatz von Standardsystemen für Anwendungsgebiete, die bisher nur speziellen Workstations vorbehalten waren. Zusammen mit dem wesentlichen Vorteil von Grafikhardware Daten direkt anzeigen zu können, sind Verfahren wie visualisierungsgestütztes Berechnen ("visual computing") oder interaktives Steuern von Berechnungen ("computational steering") erst möglich geworden. Darauf wird anhand mehrerer Beispielanwendungen und umgesetzten Konzepten wie den "ray textures" im Detail eingegangen. Da die zu verarbeitenden und darzustellenden Datenmengen stetig ansteigen, ist aufgrund von Speicher- und Bandbreiteneinschränkungen eine kompakte Repräsentation der Daten notwendig. Während die Datenkompression selbst eingehend erforscht wurde, beschäftigt sich die vorliegende Arbeit mit Möglichkeiten, Berechnungen direkt auf den komprimierten Daten durchführen zu können. Dazu wurden verschiedene Algorithmenklassen identifiziert und in die Wavelet-Domäne übertragen. Mit Hilfe von speziellen Varianten der komprimierten Repräsentation ist eine effiziente Umsetzung grundlegender Bildverarbeitungsalgorithmen möglich und zeigt zugleich das Potential dieses Ansatzes auf. Aus technischer Sicht wurde im Laufe der Arbeit die GPU-basierte Programmierumgebung "Cascada" entwickelt. Sowohl die Einführung von objektorientierten Konzepten in die Shaderprogrammierung, als auch eine hierarchische Repräsentation von Berechnungs- und/oder Visualisierungsschritten vereinfacht den Einsatz von Grafikhardware ohne wesentliche Leistungseinbußen. Dies wird anhand verschiedener Implementationen in den jeweiligen Beiträgen und zwei klinischen Projekten im Bereich der Diagnoseunterstützung gezeigt. Hierbei geht es zum einen um die semi-automatische Segmentierung der Leber in niedrig aufgelösten MR-Datensätzen, zum anderen um Möglichkeiten zur Vermessung von abdominalen Aortenaneurysmen; jeweils unterstützt durch Grafikhardware. Darüber hinaus ermöglicht "cascada" auch die Erweiterung hinsichtlich aktueller Architekturen für den universellen Einsatz von Grafikhardware, sowie künftige Entwicklungen durch ein modulares Design.
Die Beschreibung des Verhaltens eines Multi-Agenten-Systems (MAS) ist eine fordernde Aufgabe, besonders dann, wenn es in sicherheitskritischen Umgebungen eingesetzt werden soll. Denn in solchen Umgebungen muss die Beschreibung besonders sorgfältig ausgeführt werden um Seiteneffekte zu vermeiden, die ungewünschte oder sogar zerstörerische Folgen haben könnten. Deshalb sind formale Methoden nützlich, die auf mathematischen Modellen des zu entwerfenden Systems basieren. Sie erlauben es nicht nur das System formal auf verschiedenen Abstraktionsebenen zu spezifizieren, sondern auch seine Konsistenz noch vor der Implementierung zu verifizieren. Das Ziel der formalen Spezifikation ist eine präzise und eindeutige Beschreibung des Verhaltens des Multi-Agenten-Systems, während die Verifikation darauf abzielt, geforderte Eigenschaften dieses Systems zu beweisen. Üblicherweise wird das Verhalten eines Agenten als diskrete Änderung seines Zustands im Bezug auf externe oder interne Aktionen aufgefasst. Jedes mal, wenn eine Aktion auftritt, ändert sich der Zustand des Agenten. Deshalb sind Zustandsübergangsdiagramme bzw. endliche Automaten ein naheliegender Ansatz das Verhalten zu modellieren. Ein weiterer Vorteil einer solchen Beschreibung ist, dass sie sich für das sogenannte Model Checking eignet. Dabei handelt es sich um eine automatische Analysetechnik, die bestimmt, ob das Modell des Systems spezifizierten Eigenschaften genügt. Allerdings muss in realistischen, physikalischen Umgebungen neben dem diskreten auch das kontinuierliche Verhalten des Multi-Agenten-Systems betrachtet werden. Dabei könnte es sich beispielsweise um die Schussbewegung eines Fußballspieler-Agenten, den Prozess des Löschens durch einen Feuerwehr-Agenten oder jedes andere Verhalten handeln, das auf zeitlichen physikalischen Gesetzen basiert. Die üblichen Zustandsübergangsdiagramme sind nicht ausreichend, um diese beiden Verhaltensarten zu kombinieren. Hybride Automaten stellen jedoch eine elegante Lösung dar. Im Wesentlichen erweitern sie die üblichen Zustandsübergangsdiagramme durch Methoden, die sich mit kontinuierlichen Aktionen befassen. Die Zustandsübergänge modellieren weiterhin die diskreten Verhaltenswechsel, während Differentialgleichungen verwendet werden um das kontinuierliche Verhalten zu beschreiben. Besonders geeignet erscheinen Hybride Automaten, weil ihre formale Semantik die Verifikation durch Model Checking erlaubt. Deshalb ist das Hauptziel dieser Arbeit, Hybride Automaten für die Modellierung und die Verifikation des Verhaltens von Multi-Agenten-Systemen einzusetzen. Jedoch bringt ihr Einsatz mehrere Probleme mit sich, die betrachtet werden sollten. Zu diesen Problemfeldern zählen Komplexität, Modularität und die Aussagestärke der Modelle. Diese Arbeit befasst sich mit diesen Problemen und liefert mögliche Lösungen.