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

3 Darstellung der Forschungsvorhaben

Projekte

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

Die angestrebte qualitative spatio-temporale Repräsentation soll nur so viele Unterscheidungen wie nötig machen, um Bewegungen in einem gegebenen Kontext zu identifizieren. Auf diese Repräsentation sollen Operatoren u.a. zur Komposition, Konkatenation, Umkehrung und Generalisierung von Bewegungsverläufen definiert werden. Es soll untersucht werden, inwiefern dadurch vage räumliche Information effizient und zugleich kognitiv adäquat dargestellt wird und Aufgaben wie die Vorhersage von Bewegungsverläufen gelöst werden können. Zunächst werden einfache zweidimensionale Umgebungen, wie sie z.B. bei der Flugüberwachung vorkommen, betrachtet.

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

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

Spezielle Teilprojekte:

``Verteiltes maschinelles Lernen in Mehragentensystemen'', DFG-Projekt BR 609/5-2 (bis 9/96)
(Antragsteller: Brauer; Mitarbeiter: Weiß)

Im Mittelpunkt steht hier die Frage, wie mehrere Agenten lernen können, ihre Aktivitäten so zu koordinieren, daß eine vorgegebene Aufgabe gemeinsam gelöst wird. Zur Beantwortung dieser Frage werden folgende zwei Themenbereiche schwerpunktmäßig behandelt:

Test und experimentelle Analyse der Lernverfahren erfolgt mit Hilfe einer simulierten Schedulingumgebung.

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

Das Projekt wird vom DAAD im Rahmen des ARC Programms für den wissenschaftlichen Austausch mit Großbritannien gefördert.

``Qualitative Ansätze zum räumlichen Schließen aus multiplen Informationsquellen'': DAAD Projektbezogener Personenaustausch mit Schweden
(Schwedischer Partner: FOA, Linköping (Erland Jungert). Zunächst für 01.10.94 bis 30.09.96 bewilligt, inzwischen bis Ende 1997 verlängert. Projektverantwortlicher: Brauer. Projektleiter: Hernández.)

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

Brauer
Computationelle Intelligenz

(In Zusammenarbeit mit Arnoldi, Briegel, Deco, Kriebel, Pompl, Scherf, Schittenkopf, Storck, Stutz, Waschulzik)
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.

Butz
Neuronale Funktionsapproximation mit RBF-Schwerpunktnetzen

RBF-Schwerpunktnetze sind als Erweiterung der RBF-Netze anzusehen und besitzen insbesondere die Eigenschaften der verteilten Speicherung und der verteilten Ausgaberepräsentation. Eine einfache ``Schwerpunktlernregel'' ermöglicht eine schnelle Approximation und eröffnet damit den Weg für online Anwendungen (``rapid function approximation'').
Mit diesen Netzwerken ist es auch möglich, Klassifikationen auf der Basis einer ``simplizialen Kodierung'' auf der Ausgabeseite durchzuführen.

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.

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.

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.

Kunde, Rossmanith
Parallele Algorithmen und Komplexitätstheorie

Entwurf und Analyse paralleler Algorithmen auf getakteten Modellen wie Prozessorfeldern oder parallelen Registermaschinen sowie die komplexitätstheoretische Behandlung dieses Gebietes sind die Themengebiete dieses Forschungsbereiches.

Die Entwicklung von Basisalgorithmen, wie Sortieren und Datentransport auf Prozessornetzen, bilden dabei einen Schwerpunkt. Dabei wird der Einfluß verschiedener Systemparameter (Leitungszahl, Speichergröße, usw.) untersucht. Diese Basisalgorithmen sind Grundlage für nahezu alle komplizierteren parallelen Algorithmen.

Melzer
Verifikation von Systemeigenschaften mittels linearer Programmierung

Es wurde eine Verifikationsmethode entworfen und implementiert, die die Technik der Stelleninvarianten und Fallen zum Nachweis von Nichterreichbarkeit in Petrinetzen vereint. Bislang gab es kein solches kohärentes Verfahren. Die Implementierung wurde in das Verifikationstool PEP (Petrinetz-basierte Entwicklungs- und Programmierumgebung) integriert.

Die Analyse numerischer Instabilitäten des Verfahrens ist Gegenstand der aktuellen Forschung.

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

Der besondere Fokus ist hierbei auf der Charakterisierung der Transitionsdichten von stochastischen Prozessen. Zu diesem Zweck werden zahlreiche parametrische Dichten sowie neuronale Lernstrukturen miteinander verglichen.

Röckl
Modellierung paralleler imperativer Sprachen höherer Ordnung in mobilen Kalkülen

Es wurde begonnen, parallele imperative Programmiersprachen mit lokalen und globalen Variablen höherer Ordnung mit Hilfe des tex2html_wrap_inline2165 -Kalküls zu beschreiben. Versuche mit klassischen denotationellen Ansätzen führten bislang nur zu unzureichenden Resultaten. Aufgrund seiner Konzepte zur Beschreibung wechselnder Bindungsstrukturen (Mobilität) und der daraus resultierenden Möglichkeit zu Kommunikation höherer Ordnung eignet sich der tex2html_wrap_inline2165 -Kalkül besonders zur Modellierung des zu untersuchenden Programmierparadigmas. Viele für den tex2html_wrap_inline2165 -Kalkül entwickelte Beweistechniken lassen sich somit auf die Verifikation obengenannter Programmiersprachen übertragen.

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 das Lernen von One-Variable Patterns

Angluins Algorithmus für das Berechnen eines descriptive patterns einer Menge von Zeichenketten benötigt tex2html_wrap_inline2171 Schritte. Es wurde ein neuer Algorithmus entworfen, dessen Laufzeit nur noch tex2html_wrap_inline2173 beträgt.

Mit Hilfe eines Algorithmus für descriptive patterns lassen sich one-variable patterns lernen. Sie lassen sich auch aktiv mit superset queries lernen. Dies war für allgemeine pattern bekannt und gilt nun auch für one-variable patterns. Es wurde bewiesen, daß zum Lernen mit polynomiell vielen Fragen genau zwei Gegenbeispiele benötigt werden. Eines reicht nicht aus.

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.

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.

Präsentation von Forschungsvorhaben

Brauer, Brychcy, Kirchmair, Sturm
``NeuroVisionen'' auf der Hannovermesse

Prof. Dr. Wilfried Brauer, Institut für Informatik der TU München, war einer von 20 Ausstellern des Gemeinschaftsstandes ``NeuroVisionen'' auf der Hannovermesse Industrie 96. 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 Resultate des vor kurzem abgeschlossenen BMBF-Verbundprojektes NERES (``Neuronale Regelung und Steuerung von Industrierobotern'') dargestellt, in welchem unter anderem neuartige, an Hand von Beispielen lernende Bewegungsplanungsverfahren entwickelt wurden. Weiterhin wurde das BMBF Verbundprojekt 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.

Esparza, Melzer, Römer
Tool-Präsentation: ``Verification using PEP'' auf der AMAST '96, 5th International Conference on Algebraic Methodology and Software Technology, LMU München, 1.-5. Juli 1996

PEP (Programming Environment based on Petri nets) ist ein Werkzeug zur Modellierung, Simulation, Analyse und Verifikation paralleler Programme. Zwei der von uns schwerpunktmäßig untersuchten Ansätze zur Verifikation nebenläufiger Systeme wurden auf der AMAST vorgestellt, nämlich

Aktuelle Programmumsetzungen und deren Integration in die Oberfläche von PEP wurden anhand aussagefähiger Anwendungsbeispiele in typischen Benutzungssitzungen einem interessierten Fachpublikum vorgeführt. Damit konnte ein Eindruck der Mächtigkeit und Effizienz der entwickelten Verfahren vermittelt werden.


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

Gerhard Müller, Alexandra Musto, Mon Jul 21 21:46:51 MET DST 1997