next up previous contents
Next: 4 Veröffentlichungen Up: Tätigkeitsbericht 1998 Previous: 2 Drittmittel

Subsections

3 Darstellung der Forschungsvorhaben

3.1 Projekte

``Spezifikations-, Entwurfs- und Analyseformalismen für verteilte Systeme (SAM)'' , Teilprojekt A3 des SFB 0342
(Antragsteller: Brauer , Esparza ; Mitarbeiter: Kiehn , Mader , Mayr , Melzer , Röckl , Römer , Schröter , Schwoon , Wallner )

Im Mittelpunkt der Forschungsaktivitäten steht die Entwicklung eines Satzes von Analysemethoden für verteilte Systeme, aber auch deren Anwendung auf konkrete praxisrelevante Fragestellungen. Die Untersuchung verteilter Systeme gestaltet sich grundsätzlich schwieriger als die sequentieller Systeme, insbesondere ist schon bei kleinen Systemen aufgrund der Verteiltheit nicht unmittelbar einsichtig, ob sie sich korrekt verhalten. Es werden vorrangig verteilte Systeme betrachtet, die permanent auf externe Signale bzw. Ereignisse reagieren (reaktive Systeme). Systeme, die Ausgabewerte aufgrund von Eingabewerten liefern (transformationale Systeme) werden nur am Rande mitbetrachtet. Ein einfaches Beispiel eines reaktiven Systems ist eine Liftsteuerung, auf die verschiedene Benutzer auf mehreren Stockwerken räumlich verteilt zugreifen. Als Voraussetzung für die Systemanalyse wird ein formales Modell des Systems entworfen. Formal bedeutet, daß die syntaktische Darstellung eine eindeutig festgelegte Bedeutung (Semantik) hat. Zur Modellierung werden insbesondere Petrinetze und Prozeßalgebren verwendet. Beide Formalismen eignen sich zur Modellierung und Untersuchung verteilter Systeme, da sich mit ihnen Nebenläufigkeit, d.h. mögliche Parallelausführung ausdrücken läßt. Petrinetze zeichnen sich durch eine graphische Darstellung und vielfältige Analysemethoden aus. Prozeßalgebren wie z.B. CCS und CSP sind eine programmiersprachenähnliche Notation und optimal zugeschnitten für den Entwurf größerer Modelle aus Teilkomponenten. Formale Modelle sind einer exakten Analyse zugänglich. Vor allem interessant ist, ob das Modell tatsächlich wie gewünscht funktioniert. Dazu werden Eigenschaften formuliert, die das System erfüllen soll. Im Falle der Liftsteuerung sind dies z.B.

Die erste Eigenschaft muß von der Liftsteuerung irgendwann erfüllt werden (Lebendigkeitseigenschaft), die zweite muß in jedem Zustand gelten (Sicherheitseigenschaft). Für beide Arten von Eigenschaften bieten sich unterschiedliche Methoden zu ihrem Nachweis an, bei Lebendigkeitseigenschaften können auch zusätzlich zeitliche Aspekte von Interesse sein. Ein Ansatz zum Beweis von Systemeigenschaften basiert z.B. auf der temporallogischen Formulierung der Eigenschaften. Es wird geprüft, ob die temporallogischen Formeln vom System erfüllt werden. Dies geschieht entweder vollautomatisch (model checking) oder interaktiv mit einem Beweiskalkül unter Ausnutzung von Heuristiken. Ziel ist jedoch in jedem Fall eine rechnergestützte Überprüfung der Eigenschaften. Zu diesem Zweck werden Softwarewerkzeuge entwickelt, die neben dem Beweis auch die Simulation der modellierten Systeme unterstützen. Für mit Petrinetzen modellierte Systeme werden Methoden erarbeitet, die es ermöglichen, aus der Struktur, d.h. der Syntax der Modellierung, auf deren Verhalten zu schließen. Für Prozeßalgebren werden Konzepte für die Verhaltensgleichheit von zwei Modellen erforscht. Dies geschieht im Sinne einer gegenseitigen Simulation (Bisimulation) und ermöglicht die Übertragung bereits nachgewiesener Eigenschaften auf das verhaltensgleiche Modell. Weiterer Forschungsschwerpunkt ist die Betrachtung halbgeordneter Systemabläufe. Dabei wird die Semantik des Systems nicht als sequentielle Folge von Zuständen aufgefaßt, die das System beobachtbar durchläuft (bzw. als Sequenz von Ereignissen, die diese Zustandsüberführungen bewirken), sondern es wird explizit unterschieden, ob Ereignisse zufällig oder zwangsläufig nacheinander stattfinden. Diese Berücksichtigung von Nebenläufigkeit und Kausalität führt zu tieferen Einsichten beim Entwurf von verteilten Algorithmen und kann auch gewinnbringend bei deren Analyse verwendet werden.


ACON -``Adaptive Control'' , BMBF Verbundprojekt im Förderrahmen ``Intelligente Systeme''
Adaptive Modellbildung zur Optimierung, Planung und Regelung
(Teilprojektleitung: Brauer ; Mitarbeiter: Brychcy , Kirchmair , Sturm , Ungerer ;
Partner: Kratzer Automatisierung GmbH, Unterschleißheim; Michael Zoche Antriebstechnik, München ; Lehrstuhl für Elektrische Antriebstechnik, Prof. Schröder, TU München ; Institut für Elektrische Energietechnik - Antriebstechnik, Prof. Theuerkauf, GH Kassel )

Im Rahmen des BMBF-Verbundprojektes ``Adaptive Control'' ACON sollen durch Kombination und Erweiterung adaptiver, datengetriebener Verfahren zur Modellbildung die Grundlagen für das Ziel ``intelligente Prüfstandsautomatisierung'' erarbeitet werden. Zur Modellierung komplexer Systeme werden, auf der Basis neuronaler Methoden, Verfahren entwickelt, die gegebenenfalls durch Fuzzy-Logic bzw. Fuzzy-Control, Evolutionsstrategien sowie Multi-Agenten-Systeme zu ergänzen sind. Es ist geplant, auch Erkenntnisse aus dem Teilgebiet ``Verteilte Systeme'' der traditionellen Informatik einfließen zu lassen.
Der Schwerpunkt der bisherigen Arbeiten lag in der Modellbildung mit neuronalen Netzen. In Zusammenarbeit mit den Projektpartnern wurde das Problem der Modellbildung der Prozesse Verbrennungsmotor, Elektromotor und Prüfstand als Lernproblem für künstliche Neuronale Netze erarbeitet und in Teilprobleme modularisiert. Es wurden zunächst künstliche Beispielfunktionen erarbeitet, welche die charakteristischen Schwierigkeiten von solchen Teilproblemen enthalten, wie etwa Hysteresen, Totzeiten, systeminterne Nichtlinearitäten und Nichtstetigkeiten bei Zustandsübergängen. Die Modellierung dieser Beispiele mit geeigneten neuronalen Netzen wurde untersucht und dabei wurden, wo nötig, erweiterte und neue neuronale Verfahren entwickelt. Verfahren zur Integration von Teilmodellen zu Gesamtmodellen wurden entwickelt - wobei einerseits eine Aufteilung auf Teilmodelle für verschiedene Systemzustände und andererseits eine Aufteilung für verschiedene physikalische Komponenten berücksichtigt wurde. Um dies zu ermöglichen, wurde eine allgemeine Modellierungssoftwareumgebung geschaffen, welche Schnittstellen zu wichtigen Softwaretools wie Matlab enthält. Nach Verfügbarkeit durch die Projektpartner wurde von der Bearbeitung von künstlichen Beispielen zu Untersuchungen an Hand von realen Daten übergegangen.


``Qualitative Beschreibung von Bewegungsverläufen: Kognitive und Psychophysische Grundlagen'' , Projekt BR 609/9-1 im DFG-Schwerpunktprogramm ``Raumkognition''
(Antragsteller: Brauer , Schill (LMU); Mitarbeiter: Musto , Eisenkolb (LMU))

In dem insgesamt auf 6 Jahre ausgelegten Projekt sollen in interdisziplinärer Zusammenarbeit Aussagen über die Repräsentation und Verarbeitung von Bewegungsverläufen sowie ihrer Prädiktion gewonnen werden. Dazu soll u.a. untersucht werden, welche Zusammenhänge zwischen der Speicherung und Verarbeitung von Bewegungsverläufen im visuellen System und einer geeigneten qualitativen Beschreibung auf sprachlicher Ebene existieren. Grundlage der psychophysischen Untersuchungen ist ein spatio-temporales Gedächtnismodell, das notwendige Voraussetzungen für die Verarbeitung von sich örtlich-zeitlich verändernden Situationen definiert und mit dem bereits wichtige Resultate zur Kurzzeitspeicherung von visueller Information hergeleitet wurden. Darauf aufbauend sollen u.a. Untersuchungen zur Erkennung, Kategorisierung und Prädiktion von Bewegungverläufen, sowie der Integrationsfähigkeit von zusammengesetzten Bewegungssegmenten und den Regeln ihrer Kombination und schließlich auch zum Einfluß aktiver Exploration auf die Bewegungswahrnehmung durchgeführt werden.

Experimente zu Diskriminationsschwellen bezüglich der Richtungsunterscheidung von geradlinig-gleichförmigen Bewegungen ergaben, daß Richtung und Position nicht unabhängig voneinander gespeichert werden, sondern eine spatio-temporale Einheit ergeben.

Die qualitative spatio-temporale Repräsentation hat zwei Schichten, von denen eine den Bewegungsverlauf durch qualitative Bewegungsvektoren (QMV's) repräsentiert und relativ genau ist, während die zweite den Bewegungsverlauf durch eine Abfolge von Bewegungsformen (``motion shapes'') charakterisiert, die ein Entdecken von Perdiodizität und Mustern vereinfachen. Dies ermöglicht die Vorhersage von Bewegungsverläufen. Die zweite Schicht wird mittels Generalisierung, Segmentierung und Klassifizierung der QMV-Sequenz generiert.

Die entwickelte Repräsentation soll nicht nur kognitive Prozesse erklären, sondern auch für Anwendungen geeignet sein, z.B. in der Robotik (Bewegungsplanung), Verkehrsüberwachung oder Indizierung von Bildfolgen in Multimediadatenbanken. Erste Anwendungen in der Robotik bewiesen die Eignung der entwickelten Algorithmen, um mittels aufgezeichneter Eigenbewegung zu navigieren.



``Komplexität, Information, Redundanz und Neuronale Netze'', DFG-Projekt SCHM 942/3-1
(Antragsteller: Schmidhuber , Brauer ; Mitarbeiter: Hochreiter )

Ziel dieses Forschungsprojekts ist, geeignete formale Definitionen der Begriffe ``Einfachheit'', ``Komplexität'', ``Redundanzarmut'' und ``Information'' auf adaptive künstliche neuronale Netze anzuwenden und dadurch existierende Lernverfahren zu verbessern (zu beschleunigen und ihre Generalisierungsfähigkeit zu erhöhen). Zentrale Aufgabenstellungen sind hierbei:

``Kooperation und Ressourcenmanagement in verteilten Systemen'', Graduiertenkolleg Nr. 188 der DFG

Teilprojekte:
1.1 Kooperierende Agenten in verteilten Systemen -- Grundlagen.
(Leitung: Brauer , Kollegiaten: Ormoneit , Bücherl , Stein )
2.1 Verteilte Algorithmen -- Spezifikation, Modellierung, Korrektheit.
(Leitung: Esparza , Reisig (Berlin), Kollegiat: Mayr )


``Verifikation- und Analysemethoden für Systeme mit unendlichen Zustandsräumen'': DAAD PROCOPE Programm für den wissenschaftlichen Austausch mit Frankreich
Projektpartner: Institut VERIMAG, Grenoble
(Leiter des deutschen Projektteils: Esparza , Mitarbeiter: Mayr )

Der Zweck dieses Projekts ist die Entwicklung von Beweisalgorithmen für unterschiedliche Klassen von Systemen mit einer unendlichen Anzahl von Zustandsräumen. Die Algorithmen basieren auf der Approximation und Abstraktion von Techniken, die die formale Behandlung von Zustandsräumen und Daten unterstützen. Diese Techniken sind mächtig genug, um damit auch praktische Probleme zu lösen. Hauptanwendungsgebiete sind Modelle, in denen parallel laufende Prozesse über Kanäle mit unbeschränkter Speicherkapazität kommunizieren.


``Verifikationstechniken für imperative parallele Sprachen höherer Ordnung'': DAAD-Projekt im Rahmen des PROCOPE-Programms

Projektpartner: INRIA Institut zu Sophia Antipolis.
(Leiter des deutschen Projektteils: Brauer , Co-Leiter: Esparza , Mitarbeiter Röckl )

Unter Verwendung des $\pi$ -Kalküls wurde eine Prozeßsemantik für verteiltes ALGOL (Concurrent Idealized ALGOL, CIA) angegeben. Diese Sprache vereint Parallelismus und imperative Elemente mit einem prozeduralen Mechanismus beliebig höherer Ordnung (vgl. Tätigkeitsbericht 1997). Ziel ist es, Techniken und Werkzeuge für eine Mechanisierung von Bisimulationsbeweisen für den $\pi$ -Kalkül, und damit auch für Sprachen wie CIA, zu entwickeln. Vorteil der Bisimilarität ist ihre Kompositionalität, d.h. um die Äquivalenz zweier Systeme zu zeigen, genügt es die Äquivalenz entsprechend gewählter Teilsysteme nachzuweisen. Eine Fallstudie mit (statischen) Prozeßkalkülen hat gezeigt, daß eine Mechanisierung von Bisimulationsbeweisen durch Angabe konkreter Bisimulationsrelationen eine Alternative zu den sonst in Mechanisierungen verwendeten algebraischen Techniken darstellt. Eine Verbindung beider Techniken in Bisimulationen ,,up to`` kann es erlauben, auch größere Systeme zu verifizieren. Im weiteren Verlauf soll nun der $\pi$ -Kalkül auf Isabelle/HOL implementiert und Beweistechniken für ihn angegeben werden. Die Implementierung soll durch weitere Fallstudien untermauert werden. Ein Anwendungsfeld der Implementierung kann auch die Verifikation von Ausdrücken in Sprachen wie CIA sein.



3.2 Weitere Forschungsvorhaben


Bartmann
Identifikation eines Tastaturbenutzers durch Analyse des Tippverhaltens

Dieses Projekt beschäftigt sich mit einem neuartigen Authentifikationssystem, das auf dem psychometrischen Merkmal ``Tippverhalten'' basiert. Durch Analyse von Schreibrhythmus, Anschlagfolge und anderen Aspekten des Tippverhaltens soll es damit möglich sein, auf Grund eines ca. 100 Zeichen langen, beliebigen Eingabestrings, eine Person mit Hilfe gewöhlicher Hardware zu identifizieren. Dazu werden klassische statistische Verfahren mit Methoden aus dem Bereich der KI kombiniert. Das Einsatzgebiet reicht von der einmaligen Identifikation bei der Zutrittskontrolle über elektronische Unterschrift und Textautorisierung bis hin zur ständigen Identitätsüberwachung im laufenden System.


Brauer
Computational Intelligence
(In Zusammenarbeit mit Arnoldi, Briegel, Deco, Gilsdorf, Hofmann, Hollatz, Kriebel, Pompl, Scherf, Schittenkopf, Storck, Sturm, Stutz, Waschulzik, Wei)

Suche nach naturanalogen und mathematischen Verfahren der unüberwachten Analyse von Daten (Sensordaten, symbolische Daten) im Hinblick auf strukturelle Zusammenhänge (Struktur-/Gestalt-Erkennung, Klassifikation, statistische Zusammenhänge) oder von Zeitreihen im Hinblick auf Eigenschaften des erzeugenden dynamischen Systems (Rauschen oder deterministisches Chaos, Markov-Ketten, lineares System, ...) zum Zwecke der Datenvorverarbeitung, der Adaption oder des Lernens (und Wiedererkennens oder Vorhersagens) unter Verwendung von konnektionistischen, informationstheoretischen, statistischen, automatentheoretischen und fuzzy-theoretischen Methoden.
Bearbeitung von Anwendungsproblemen aus verschiedenen Bereichen, insbesondere der Medizin und Umweltforschung.


Bücherl (Graduiertenkolleg ``Kooperation und Ressourcenmanagement in verteilten Systemen'')
Formale Methoden zur Modellierung von Multiagenten-System

Ein wesentliches Problem bei der Entwicklung einer geeigneten formalen Modellierungsmethode für Multiagenten-Systemen stellt die Integration der lokalen Agentenperspektive, die sich mit den Eigenschaften und Fähigkeiten der einzelnen Agenten beschäftigt, und der globalen Systemperspektive, die sich mit der Organisation des Kooperationsverhaltens des gesamten Multiagenten-Systems auseinandersetzt, dar. In dieser Hinsicht wird das Konzept der logischen Faserungen untersucht und an einer Weiterentwicklung gearbeitet, da der Faserungenansatz durch seine inhärente Möglichkeit, lokal-global Beziehungen verschiedener Strukturen in einem Konzept auszudrücken, dazu besonders geeignet erscheint.


Kiehn
Non-Interleaving-Semantiken

Non-Interleaving-Semantiken beschreiben das Verhalten von nebenläufigen Prozessen, wobei explizit Aspekte wie Nichtdeterminismus und Nebenläufigkeit ausgedrückt werden. Für die Prozeßalgebra CCS wurde gezeigt, daß sich viele der bekannten Beweistechniken der Standardsemantik (observation equivalence) auf das Non-Interleaving übertragen lassen, wenn die Algebra um einen History-Operator erweitert wird.


Kriebel
Explorative konnektionistische Modellierung von natürlichen Systemen zu deren Analyse und Vorhersage

Die Analyse und Vorhersage von natürlichen Phänomenen ist in den letzten Jahren zunehmend sowohl in das wissenschaftliche, als auch in das öffentliche Interesse gerückt. Naturereignisse, wie beispielsweise das derzeit sehr ausgiebig untersuchte und diskutierte Phänomen ``El Niño'', werden verantwortlich für Katastrophen und Klimaannormalitäten gemacht, obgleich die synergetischen Effekte der beobachteten Parameter und die zugrundeliegenden biologischen, chemischen und physikalischen Systeme nur wenig bekannt sind.

Übliche Vorhersagemodelle basieren auf mehrdimensionalen numerischen Modellen, in denen versucht wird vorhandenes Wissen zu kodieren. Die Güte der Vorhersagen hängt hier wesentlich von der Komplexität des natürlichen Systems, bzw. von dem implementierten Expertenwissen ab. Vorhersagen mit diesen Systemen sind in der Regel sehr aufwendig und nur mit großen Entwicklungs- und Anwendungskosten zu realisieren.

Seit man mit Satellitensensoren die Erde in regelmäßigen Zeitabständen großflächig beobachtet, stehen Zeitreihen von Parametern zur Verfügung die man zur Analyse von natürlichen Phänomenen heranzieht. In der Zwischenzeit kann man auch auf mehrjährige Zeitreihen zurückgreifen, die einen Ansatz zur inversen Modellierung ermöglichen, der in zunehmenden Maße in der Erforschung von Klima- und ozeanographischen Phänomenen an Bedeutung gewinnt.

In der Regel sind nichtlineare Systeme zu modellieren, die prinzipiell die Anwendung von künstlichen neuronalen Netzen bei der inversen Modellierung nahelegen. Da die Systeme auch oft nichtstationär und nichtdeterministisch sind, ist das Ziel dieser Arbeit die Entwicklung eines adaptiven explorativen konnektionistischen Analyse- und Vorhersagewerkzeugs, das die Behandlung von Zeitreihen unter genannten Randbedingungen erlaubt.


Melzer
Verifikation von Systemeigenschaften mittels linearer Programmierung

Das numerische Verhalten einer entwickelten Beweistechnik, der sog. Fallenungleichung wurde untersucht. Es hat sich gezeigt, daß für kleine Netze diese Methode zu numerischen Problemen führt und somit praktisch nicht sicher einsatzfähig ist. Es wurde zuerst ein Separierungsverfahren angegangen, welches zwar die numerischen Probleme zu umgehen vermag, aber ein doppelt-exponentielles Verhalten zeigt. Darauf aufbauend ist ein Branch-and-Cut-Verfahren entworfen und implementiert worden, das mit seinem einfach-exponentiellen Verhalten der Komplexität des zugrundeliegenden Problems entspricht.



Ormoneit (Graduiertenkolleg ``Kooperation und Ressourcenmanagement in verteilten Systemen'')
Verwendbarkeit von neuronalen Netzen zur Schätzung von Wahrscheinlichkeitsdichten

In Erweiterung der gewöhnlichen Funktionalitaet von neuronalen Netzen lassen sich insbesondere Netze zur Approximation von Wahrscheinlichkeitsdichten konstruieren. Der Vorteil einer derartigen Wissensrepräsentation ist die Möglichkeit des Erlernens von allgemeineren probabilistischen Abhaengigkeiten, als dies für gewöhnliche neuronale Netze möglich ist. Ein zweiter Arbeitsschwerpunkt ist die Analyse des statistischen Lernens in nichtstationären (d.h. zeitlich veränderlichen) Umgebungen. Entsprechende Ansätze führen zu Inferenzproblemen in sogenannten ``State-Space Models'', in denen aus einer Reihe von Beobachtungen der ``wahre'' Zustand eines Systems identifiziert werden soll. Eng verwandt mit der State-Space-Problematik ist das Lernproblem in Multiagentensystemen, da sich auch hier die Strategien der Gegenspieler als verborgene Zustände interpretieren lassen.



Pompl
MELDOQ

Das maligne Melanom der Haut ist die boesartigste Hauterkrankung beim Menschen. Sein Auftreten hat sich in den letzten Jahren dramatisch erhoeht. Fruehzeitig erkannt bestehen gute Heilungschancen durch Exzision. In spaeteren Stadien allerdings ist die Sterblichkeitsrate bedingt durch aggressive Metastasenbildung sehr hoch. Die leistungsfaehigste diagnostische Methode ist die Dermatoskopie (Auflichtmikroskopie bei 10facher Vergroesserung) und die dazugehoerige ABCD-Regel. Deren Anwendung erfordert jedoch viel dermatoskopisches Expertenwissen und Erfahrung. Zur Verbesserung der Frueherkennung wird ein dermatoskopischer Arbeitsplatz entwickelt, mit dem der niedergelassene Dermatologe Hautveraenderungen digital erfassen und patientenbezogen archivieren kann. Darueberhinaus bietet das System dem Dermatologen ein Bildanalysemodul an, das die Merkmale der ABCD-Regel auf reproduzierbare quantitative Parameterskalen abbildet. Die Ergebnisse der Analyse werden objektnah visualisiert und zu einem Diagnosevorschlag zusammengefasst. Dadurch wird dem Dermatologen eine wichtige Diagnoseunterstuetzung angeboten.



Röckl
Beweiserunterstützte Verifikation von Prozeßäquivalenzen

Die Beobachtungsäquivalenz ist gerade im Hinblick auf die Verifikation verteilter reaktiver Systeme interessant, da sie von internen Vorgängen abstrahiert, gleichzeitig jedoch durch die Verteilung entstehende Nichtdeterminismen reflektiert und Verklemmungen berücksichtigt. Man kann sie einsetzen, indem man das System sowie die Spezifikation als Prozesse modelliert und versucht, eine geeignete Bisimulationsrelation anzugeben. Das hat die folgenden Vorteile:

Obwohl zur Modellierung verteilter Systeme in der Regel eine eingeschränkte Prozeßklasse ausreicht (Basic Process Algebra), so ist dennoch auch hier die Beobachtungsäquivalenz unentscheidbar (Restriktion zur Modellierung interner Verbindungen). Dies macht in Bezug auf Computerunterstützung die Verwendung von Theorembeweisern unumgänglich.

In einer Fallstudie wurden mit der Unterstützung von Isabelle/HOL drei Beweise mit folgenden Szenarien durchgeführt:

Diese ersten Erfahrungen mit der Anwendung von Isabelle/HOL auf Prozeßalgebren können als positiv gewertet werden, da sich ein erstaunlich hoher Grad an Automatisierung ergeben hat. Damit wurde der erste Schritt der im letzten Tätigkeitsbericht angekündigten Entwicklung von Techniken und Werkzeugen für Bisimulationsbeweise mit Theorembeweisern vollzogen.


Römer
Entwicklung und Implementierung von Verifikationstechniken auf der Basis von Netzentfaltungen

Themengebiete dieses Forschungsbereichs sind die Entwicklung und Umsetzung effizienter Datenstrukturen und Algorithmen zur Darstellung und Manipulation von Petrinetzen. Schwerpunkt der Arbeiten bilden Model-Checking-Verfahren zur Verifikation nebenläufiger Systeme mit Hilfe von Netzentfaltungen. Es werden Implementierungen und Optimierungen rechenzeitkritischer Programmprototypen vorgenommen, sowie deren Einbindung in das Analysewerkzeug PEP (Programming Environment based on Petri nets).


Rossmanith
Effiziente Algorithmen für eng gekoppelte Multiprozessoren

Moderne Mikroprozessoren haben bereits einen hohen Grad an Paralletität bei der Verarbeitung von eigentlich sequentiellen Programmen. Diese Parallelität äußert sich unter anderem in überlappter Abarbeitung (Pipelining) und echter Übergabe von mehreren Befehlen in einem Taktschritt (Superskalare Prozessoren). Der Trend geht weiter in diese Richtung.

Es soll erforscht werden, ob speziell entworfene Algorithmen den üblichen sequentiellen Algorithmen auf solchen Prozessoren überlegen sind.

Rossmanith
Stochastically Finite Learning (mit Zeugmann, Kyushu University)

Es wird untersucht, wie schnell mit positiven Beispielen im allgemeinen gelernt werden kann. Insbesondere wurde untersucht, wie schnell die Fehlerwahrscheinlichkeit abnehmen kann. Es stellte sich heraus, dass man Algorithmen im allgemeinen durch ein festes Schema so modifizieren kann, dass die Fehlerwahrscheinlichkeit exponentiell schnell abnimmt.

Rossmanith
Effiziente parametrisierte Algorithmen (mit Niedermeier, Tübingen)

Es wurden schnellere parametrisierte Algorithmen für Vertex Cover und MaxSat entwickelt. Für MaxSat wurde darüberhinaus auch der bisher schnellste Algorithmus in der Anzahl der Klauseln und der Länge der Formel gewonnen. Gleiches gilt für das eingeschränkte Problem Max2Sat, welches immer noch NP-vollständig ist.


Scherf
EUBAFES

Es wurde das distanzbasierte Merkmalsselektionsverfahren EUBAFES (Euclidean Based Feature Selection) entwickelt. EUBAFES bestimmt auf der Basis einer Menge vorklassifizierter Fälle automatisch diejenigen Merkmale, die zur Beschreibung einer gegeben Klassifikationsaufgabe notwendig sind. Primäres Ziel dieses Ansatzes ist die Optimierung von Neuronalen Netzen mit radialen Basisfunktionen (RBF-Netze) durch die Abschwächung des curse of dimensionality.

Anwendung fand EUBAFES in Zusammenhang mit der Entwicklung eines entscheidungsunterstützenden Systems zur Glaukomfrüherkennung, das im Rahmen des europäisch geförderten Projektes OPHTEL (Telematics in Ophthalmology) entwickelt wurde. Hier wurde EUBAFES bei der Klassifikation von Perimetriedaten eingesetzt. Weiterhin fand EUBAFES im Zusammenhang mit der Klassifikation von Hirntumordaten Anwendung.


Schlieder
Räumliche Konfigurierung als algorithmisches und kognitives Problem

Bei räumlichen Konfigurierungsaufgaben wie dem automatischen Layout von Dokumenten spielen qualitative Relationen (z.B. Textfeld X liegt linksbündig mit Abbildung Y) eine wichtige Rolle. Mit diskreten Constraint-Netzen verfügt man über ein ausdrucksmächtiges, jedoch nicht immer effizientes Werkzeug zur Lösung solcher Aufgaben. Schwerpunkt dieser Forschungsarbeit ist die heuristische Optimierung der Constraint-Propagierung und Instanziierung unter Verwendung von Resultaten und Methoden der kombinatorischen Geometrie. Um nicht nur ein algorithmisch effizientes, sondern auch ein unter kognitivem Gesichtspunkt ergonomisches Konfigurierungssystem zu erhalten, müssen bei der Aufgabenteilung zwischen System und Benutzer dessen Denkstrategien berücksichtigt werden. In denkpsychologischen Experimenten werden daher die Strategien menschlicher Problemlöser, insbesondere die Verwendung visueller Vorstellungen, untersucht.


Schmidhuber
Überwachtes Lernen, unüberwachtes Lernen und ``Reinforcement''-Lernen

Schwerpunkte bilden hierbei:

1.
Adaptive rekurrente dynamische neuronale Netzwerke für die zielgerichtete Verarbeitung sequentieller Eingabeströme.
2.
Unüberwachtes Lernen, Datenkompression und automatische Generierung statistisch redundanzarmer Eingabecodierungen.
3.
Aktive Datenselektion zur Verbesserung der Performanz von Reinforcement-Lernverfahren.
4.
Entwurf von Algorithmen zur adaptiven Erstellung von neuronalen Netzwerken niedriger informationstheoretischer Komplexität und hoher Generalisierungsfähigkeit.
5.
Algorithmische Informationstheorie (Theorie der Kolmogorov-Komplexität) und ihre praktische Verwertbarkeit für maschinelles Lernen. Dabei werden geeignete berechenbare Erweiterungen von Kolmogorov-Komplexität (wie beispielsweise Levin-Komplexität) verwendet. Ziel ist ein inkrementell lernendes System, welches sich die vielfältige algorithmische Redundanz in der realen Welt zunutze macht und nicht aufhört, Sinnvolles zu lernen.


Schröter
Verifikation von Systemeigenschaften auf Netzentfaltungen

Für die Untersuchung von Erreichbarkeitsfragen auf Netzentfaltungen gibt es verschiedene Methoden, die zum Beispiel auf linearer Programmierung oder Constraint-Programmierung basieren. Als Alternative zu diesen Techniken wurde ein graphentheoretisches Verfahren für Erreichbarkeitsfragen auf Netzentfaltungen implementiert. Das Verfahren überprüft anhand der Co-Relation, die während des Entfaltungsprozesses erzeugt wird, ob eine Teilmarkierung erreichbar ist oder nicht. Durch Verwendung verschiedener Heuristiken soll untersucht werden, inwiefern die Effizienz des Algorithmus noch verbessert werden kann.


Schwoon (Graduiertenkolleg ``Kooperation und Ressourcenmanagement in verteilten Systemen'')
Entwicklung einer Shell zur Integration verschiedener Verifikationspakete

Wir arbeiten an einer gemeinsamen Schnittstelle für verschiedene Modelchecking-Tools. Es soll die Möglichkeit geschaffen werden, verschiedene Verifikations-Algorithmen auf Systeme anzuwenden, die sich als 1-sichere Petri-Netze beschreiben lassen. Als Eingabesprachen für solche Systeme kommen neben Petri-Netzen (in verschiedenen Dateiformaten) auch parallele endliche Automaten in Frage. Bei den z.Zt. unterstützten Tools handelt es sich um PEP, PROD, APNN und SMV. Durch die gemeinsame Oberfläche soll der Vergleich dieser Tools erleichtert und es dem Benutzer ermöglicht werden, auf der Basis einer einheitlichen Modellierung das jeweils passende Tool auszuwählen. Die Schnittstelle ist offen, d.h., es können (evtl. in Kooperation mit anderen Wissenschaftlern) in Zukunft weitere Eingabesprachen und Tools leicht integriert werden.


Stein (Graduiertenkolleg ``Kooperation und Ressourcenmanagement in verteilten Systemen'')
Qualitative Raumrepräsentation

Repräsentation und Bearbeitung räumlicher Informationen durch die Maschine (vielfach Verarbeitung numerischer Daten) unterscheidet sich von der Sicht des Menschen (qualitative Beschreibungen mittels sichtbarer Landmarken oder Beziehungen zwischen Objekten). Bezüglich der Beschreibung und Verarbeitung (Planung, Kontrolle, ...) von Bewegungsverläufen wird untersucht, wie sich numerische und qualitative Representationen ineinander überführen lassen, um einfache Mensch-Maschine-Interaktion zu ermöglichen, aber auch inwieweit sich qualitative Verfahren direkt zur informatischen Verarbeitung eignen, ohne dabei auf eine numerische Darstellung zurückzugreifen.


Stutz
Datenanalyse und Modellierung mit partiell überwachten Fuzzy-Clusterverfahren

Es werden in Zusammenarbeit mit der Siemens AG Methoden entwickelt, um verschiedene Formen des anwendungsspezifischen Wissens für die Datenanalyse und Modellierung zu nutzen. Dafür werden partiell überwachte Fuzzy-Clusterverfahren eingesetzt. Diese Methoden werden zur Analyse von Straßenverkehrsdaten verwendet. Die Anwendungen sind Prognose von Verkehrsaufkommen und Beurteilung der Qualität des Verkehrsablaufs.


Wallner
Model Checking von Halbordnungslogiken
Zusammen mit Huhn, Niebert (Universität Hildesheim)

Nach ersten Ergebnissen zur Anwendbarkeit von Netzentfaltungen für Model-Checking-Algorithmen auf Halbordnungslogiken, soll diese Forschungslinie weitergeführt und erweitert werden. Netzentfaltungen eignen sich durch explizit enthaltene Information über Nebenläufigkeit und Konflikte besonders als Modelle für kausale und lokale Halbordnungslogiken. Es wird untersucht, inwieweit für Verallgemeinerungen der bereits vorgeschlagenen lokalen Fixpunkt-Logik das Model Checking Problem effizient entscheidbar bleibt.


Wei
Ein Verfahren zur Stereokorrespondenz mittels eines RBF-Netzwerks

Die stereooptische Formerfassung räumlicher Objekte hat ein weites Anwendungsfeld in vielen, sehr unterschiedlichen Bereichen. Eine der schwierigsten Aufgaben im Stereosehen ist die Korrespondenzsuche, die die physikalisch korrespondierenden Punkte in beiden Bildern identifiziert. Wir haben ein neues Verfahren zur Lösung des Problems vorgestellt. Mittels eines RBF-Netzwerks parametrisieren wir die Disparitätskarte. Das RBF-Netzwerk wird in einer hierarchischen Weise aufgebaut. Dann wird die Intensitätsfehler der Stereobilder minimiert bezueglich der RBF-Parameter. Das Endergebnis ist eine dichte Disparitätskarte.


Weiß
Lernen in verteilten intelligenten Systemen

Im Mittelpunkt dieses Vorhabens steht die Frage, wie die Komponenten eines verteilten Systems lernen können, ihre Aktivitäten geeignet zu koordinieren. Ausgehend davon ergaben sich folgende Arbeitsrichtungen:

Für die experimentelle Analyse der entwickelten Verfahren und Modelle wurden die Anwendungsbereiche Job-Assignment, Lastverteilung und Robotic Soccer gewählt.


next up previous contents
Next: 4 Veröffentlichungen Up: Tätigkeitsbericht 1998 Previous: 2 Drittmittel
Alexandra Musto, Tue Jul 13 15:19:24 MET DST 1999