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

3 Darstellung der Forschungsvorhaben

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, 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.

``Intelligente Systeme'', Teilprojekt im BMBF-Verbundprojekt ``ACON: Adaptive Control''
Adaptive Modellbildung zur Optimierung, Planung und Regelung
(Teilprojektleitung: Brauer; Mitarbeiter: Brychcy, Kirchmair, Sturm;
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.

``Qualitative Beschreibung von Bewegungsverläufen: Kognitive und Psychophysische Grundlagen'', Projekt BR 609/9-1 im DFG-Schwerpunktprogramm ``Raumkognition''
(Antragsteller: Brauer, Hernández, 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.

``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:

``Neuronale Semantikmodelle (NEUROSEM)'', DFG-Projekt BR 609/7-1
(Antragsteller: Brauer; Mitarbeiter: Scheler)
Die Aufgabenstellung der konnektionistischen Modellierung der Semantik, eingeschränkt auf die Semantik von Morphemen oder Wörtern, betrifft zum einen die praktische Analyse von Texten, Diskursen oder Korpora, und die dazu notwendigen Verfahren (Musterextraktion, statistische Analyse von Konkurrenzbeziehungen und Häufigkeiten bestimmter syntaktischer Konstruktionen, Vorverarbeitung (tagging, parsing)); zum anderen die theoretische Modellierung von Bedeutung auf der Basis von neuronalen Prinzipien der Klassifikation, Musterformation und Speicherung. Im Forschungsvorhaben wird die spatiale Bedeutungskomponente von Nomina, Präpositionen sowie Adverbien als wesentlicher paradigmatischer Fall betrachtet - andere Bereiche der Wort-/Morphemsemantik werden aber ebenfalls vergleichend untersucht.

``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)

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.

``Kausale Fixpunktlogiken'': DAAD Projektbezogener Personenaustausch mit Großbritannien
(Britischer Partner: Dr. Bradfield (Universität Edinburgh). Projektverantwortlicher: Esparza. Projektleiter: Mader.)
Temporale Fixpunktlogiken ermöglichen eine formale Spezifikation von Eigenschaften verteilter und reaktiver Systeme. Die meisten Logiken dieser Art erlauben es jedoch nicht, Aspekte wie kausale Abhängigkeiten und räumliche Verteiltheit auszudrücken. Ziel des Projekts ist die Definition einer kausalen Fixpunktlogik und einer damit konsistenten, formalen Semantik verteilter Systeme. Sie sollen mächtig genug sein, oben genannte Aspekte auszudrücken, in ihrer Struktur aber noch hinreichend einfach, um in Theorie und Praxis hilfreich zu sein. Darauf aufbauend sollen rechnergestützte Beweiswerkzeuge entwickelt werden.

``Qualitative Ansätze zum räumlichen Schließen aus multiplen Informationsquellen'': DAAD Projektbezogener Personenaustausch mit Schweden
(Schwedischer Partner: FOA, Linköping (Erland Jungert). Projektverantwortlicher: Brauer. Projektleiter: Hernández. Bis Ende 1997.)
Ziel der Zusammenarbeit ist die Untersuchung dynamischer Aspekte beim qualitativen räumlichen Schließen. Dabei stehen zwei Themen im Vordergrund: die Entwicklung eines qualitativen Modells zur Behandlung von ``Bewegung'' und die Entwicklung von Verfahren, um qualitative Information aus mehreren Quellen zusammenzufügen.

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, Strum, 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.

Hernández
Qualitative Repräsentation räumlichen Wissens
Menschliche Raumkonzepte sind qualitativer Natur, d.h. sie basieren weniger auf exakten Größen als vielmehr auf Vergleichen zwischen wahrgenommenen Größen. Ziel dieses Forschungsschwerpunkts ist es, ein qualitatives Modell zur Darstellung räumlichen Wissens zu entwickeln, das effizientes und zugleich intuitives Schließen erlaubt. Bisherige Arbeiten haben sich mit der Darstellung von Zeit sowie von Größe und Positionen im 2-dimensionalen Raum beschäftigt. Gegenwärtig wird untersucht, wie andere Aspekte wie z.B. Form und Bewegung (auch in 3-D) qualitativ dargestellt werden können, aber auch wie qualitative Ansätze in hybriden Systemen mit quantitativen und konnektionistischen Systemen integriert werden können. Diese Modelle finden Anwendung in vielen Bereichen, z.B. in geographischen Informationssystemen, computerunterstützten Entwurfssystemen in der Architektur, in der Mikroelektronik und im Maschinenbau, aber auch bei der Steuerung von Robotern oder bei natürlichsprachlichen Wegauskunftsystemen.

Hernández, Clementini, di Felice
Qualitative Darstellung von Entfernungen
Das qualitative Modell zur Repräsentation von Entfernungen ist weiterentwickelt worden. Getreu den qualitativen Prinzipien werden dabei nur so viele Entfernungen unterschieden, wie in einem gegebenen Kontext nötig. Die verschiedenen Unterscheidungsebenen bilden eine Hierarchie. Entscheidend ist die Möglichkeit, nicht nur die Anzahl der Entfernungsunterscheidungen, sondern auch die Art und Weise, wie die Entfernungsintervalle zueinander (etwa in ihrer Größe) stehen, festzulegen. Die Struktur der Entfernungssyteme wird mit Hilfe algebraischer Strukturen beschrieben. Es sind Algorithmen zur Komposition von Entfernungsrelationen in mehreren Sonderfällen sowie zur Anpassung unterschiedlicher Bezugsrahmen entwickelt worden.

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.

Melzer
Verifikation von Systemeigenschaften mittels Constraint Programming
Ausgehend von einer klassischen Beweistechnik - der Transitioneninvarianten - wurde eine Verfeinerung erarbeitet, die es erlaubt, die Grundlage eines Testverfahrens zur Überprüfung von Lebendigkeitseigenschaften zu bilden. Mit der Verfeinerung konnte die Berechnung mit Mitteln der reinen linearen Programmierung nicht mehr gewährleistet werden. Stattdessen ist auf die Theorie der Constraint Programmierung ausgewichen worden, die es erlaubte, einen automatischen Ansatz zu implementieren und anhand mehrerer Beispiele zu evaluieren.

Melzer
Anwendung von linearen Beweistechniken auf Netzentfaltungen
Mit Netzentfaltungen liegt eine Netzklasse vor, auf der die Markierungsgleichung der Petrinetztheorie nicht nur ein notwendiges, sondern auch ein hinreichendes Kriterium für Erreichbarkeit darstellt. Es wurde eine lineare Verifikationstechnik in Zusammenarbeit mit Stefan Römer erarbeitet, mit deren Hilfe Verklemmungen von Netzen auf ihren Netzentfaltungen erkannt werden können. Dabei zeigt die Implementierung ein orthogonales Verhalten zu einer bestehenden Technik nach McMillan.

Menden
Erweiterung der Temporalen Logik mit veränderlichen Funktionen
Die klassische Anwendung Temporaler Logik modelliert sequentielle wie parallele Prozesse ausgehend von einer Beschreibung in einer imperativen Programmiersprache. Wichtige Konzepte wie Prozeduraufrufe, call-by-referenz Variablen, Referenzen allgemein oder gar objektorientierte Konzepte wie Vererbung und Polymorphismus konnten aber noch nicht modelliert werden. Dieses Problem wird durch Erweiterung der Temporalen Logik mit veränderlichen Funktionen angegangen.

Ormoneit (Graduiertenkolleg ``Kooperation und Ressourcenmanagement in verteilten Systemen'')
Untersuchung der Verwendbarkeit von neuronalen Netzen zur Schätzung von Wahrscheinlichkeitsdichten
In Erweiterung der gewoehnlichen Funktionalitaet von neuronalen Netzen lassen sich insbesondere Netze zur Approximation von Wahrscheinlichkeitsdichten konstruieren. Der Vorteil einer derartigen Wissensrepraesentation 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 ebenfalls das Lernproblem in Multiagentensystemen, da sich auch hier die Strategien der Gegenspieler als verborgene Zustände interpretieren lassen.

Röckl
Modellierung paralleler imperativer Sprachen höherer Ordnung in mobilen Kalkülen
Unter Verwendung des tex2html_wrap_inline2278 -Kalküls wurde eine Prozeßsemantik für verteiltes ALGOL angegeben. Die Sprachen dieser Familie zeichnen sich durch eine Kombination eines einfachen imperativen Kerns mit einem Call-by-Name tex2html_wrap_inline2280 -Kalkül aus und bilden die Grundlage vieler gebräuchlicher Programmiersprachen. Untersucht wurde auch eine Erweiterung, die Sprachen mit Variablen höherer Ordnung umfaßt. Durch den Umfang der für den tex2html_wrap_inline2278 -Kalkül entwickelten Beweismethodologie ist es nun möglich, leicht Äquivalenzbeweise für parallele Programme anzugeben, was mit den bisherigen Techniken nur unter erheblichem Aufwand möglich ist. So wurden etwa Beweise für zahlreiche der Meyer-Sieber-Beispiele geführt.

Ziel ist es nun, Techniken und Werkzeuge für die (Semi-)Automatisierung derartiger auf Bisimulationen basierender Beweise zu erarbeiten. Die diesbezüglichen Verfahren sollen unter Einsatz des Theorembeweisers Isabelle entwickelt werden.

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. Dabei ist klar, daß sich dieser Mehraufwand sowieso nur in den kritischen Fällen lohnen wird.

In einem ersten Schritt wurden Such- und Sortieralgorithmen untersucht. Es zeigt sich, daß bei einer einfachen Modellannahme spezielle Suchalgorithmen wenig, Sortieralgorithmen unter Umständen viel einbringen.

Rossmanith
Stochastically Finite Learning
Es wurde eine neue Analyse des Lange-Wiehagen Algorithmus für das Lernen von Pattern Sprachen durchgeführt, welche für beinahe jede vernünftige Wahrscheinlichkeitsverteilung der zu lernenden Daten direkt anwendbar ist. Dabei muß die Verteilung nicht genau bekannt sein; es genügt eine recht grobe Information über sie.

Mit dieser Information läßt sich für eine gegebene Wahrscheinlichkeit eine Schranke angeben, wann mit dieser Wahrscheinlichkeit richtig gelernt wurde. Diese Schranke ist im allgemeinen günstiger als beim PAC-Lernen und läßt sich auch in Fällen finden, für welche PAC-Lernen unmöglich ist. Dieses neue Lernmodell läßt sich für allgemeine Fragestellungen definieren.

Ruge
Extraktion künstlicher semantischer Merkmale aus großen Korpora
In diesem Projekt wird untersucht, in wie weit Bedeutungsrepräsentationen für Wörter aus Korpora extrahiert werden können. Dabei wird kein semantisches Wissen eingesetzt, sondern rein syntaktisch und statistisch gearbeitet. Die Bedeutungsrepäsentationen sind den bekannten semantischen Merkmalen ähnlich. Es wird untersucht, wie gut sie verschiedene Probleme der Computerlinguistik lösen können. Zu diesen Problemen gehöhren die syntaktische Disambiguierung, die lexikalische Disambiguierung bei der maschinellen Übersetzung, die Generierung von Thesaurusrelationen, sowie Information Retrieval auf der Basis dieser Merkmalsrepräsentationen.

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.

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 sie etwa in der Raumplanung mit geographischen Informationssystemen anfallen, spielen qualitative Relationen (z.B. X liegt zwischen Y und Z) eine entscheidende Rolle. Mit diskreten Constraint-Netzen verfügt man über ein ausdrucksmächtiges, jedoch nicht immer effizientes Werkzeug zur Lösung solcher Aufgaben. Schwerpunkt dieses Forschungsvorhabens 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 zusätzlich die Strategien menschlicher Problemlöser, insbesondere die Verwendung visueller Vorstellungen, untersucht.

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.

Wallner
Model Checking LTL mit Netzentfaltungen
Es wurde gezeigt, daß McMillans endliches Präfix der Entfaltung eines sicheren Petrinetzes dafür geeignet ist, Linear-time Temporallogik (LTL) zu verifizieren. Es wird dabei der automatentheoretische Ansatz (Wolper et al.) auf den Petrinetz-Formalismus übertragen: nach dem Erzeugen eines Büchiautomaten A(-f), der alle Abläufe akzeptiert, die eine gegebene LTL-Spezifikation f nicht erfüllen, wird das zu verifizierende Petrinetz N mit A(-f) synchronisiert. Es entsteht ein Netz N(f) mit Akzeptanzbedingung, d.h. manche seiner Abläufe gelten als akzeptierend. Das zugrundeliegende System N erfüllt die Spezifikation f genau dann, wenn N(f) keinen akzeptierenden Ablauf besitzt. Dieser Test auf Leerheit kann nun in effizienter Weise auf dem Präfix der Entfaltung von N(f) durchgeführt werden. Es soll nun die Möglichkeit zu effizienter Integration von Fairness-Eigenschaften geschaffen werden.

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.

Präsentation von Forschungsvorhaben

Brauer, Brychcy, Kirchmair, Sturm
``Neuro Goes Business'' auf der Hannovermesse Industrie `97
Prof. Dr. Wilfried Brauer, Institut für Informatik der TU München, war einer von 20 Ausstellern des Gemeinschaftsstandes ``Neuro Goes Business'' auf der Hannovermesse Industrie 97. Dort präsentierten Forschungseinrichtungen, Universitäten, Industrie und mittelständische Unternehmen gemeinsam konkrete Anwendungen neuronaler Netze in Technik und Medizin. Durch dieses Forum wurde die Industrie auf neue, durch die Neuroinformatik geschaffene Möglichkeiten aufmerksam gemacht und der Weg für einen allgemeinen Einsatz der in der anwendungsorientierten Grundlagenforschung gewonnenen Ergebnisse bereitet. So wurden vom Lehrstuhl Brauer erste Resultate des BMBF-Verbundprojektes ACON (``Adaptive Control'') vorgestellt, bei dem der Einsatz von neuronalen Netzen, Fuzzy Logic und verwandten Verfahren in den Anwendungsgebieten Prüfstandsautomatisierung und Motorregelung untersucht wird.

Best, Esparza, Grahlmann, Melzer, Römer, Wallner
Tool-Präsentation: ``The PEP Verification System'' auf der FemSys'97, Workshop on Formal Design of Safety Critical Embedded Systems, München, 16. - 18. April 1997
PEP (Programming Environment based on Petri nets) ist ein Werkzeug zur Modellierung, Simulation, Analyse und Verifikation paralleler Programme. Vor einem Fachpublikum aus der Industrie wurden vor allen Dingen die neusten Entwicklungen an PEP vorgeführt. Neben dem neuen Ansatz mit Constraint Programmierung und einem LTL Model-Checker wurde eine neue Benutzeroberfläche präsentiert, die es erlaubt, große Petrinetze einfacher zu editieren.

Brauer, Bartmann
PSYLOCK
Messestand auf der SYSTEMS '97 vom 27.-31.10.97.

Bartmann
Identifikation eines Tastaturbenutzers durch Analyse des Tippverhaltens
Präsentation am ``Tag der Informatik'', 28.11.97

Esparza, Melzer, Römer,Wallner
Rechnergestützte Verifikation verteilter Systeme mit PEP
Präsentation am ``Tag der Informatik'', 28.11.97


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

Alexandra Musto, Fri Jun 26 15:46:55 MET DST 1998