EXTRA-Treffen Archiv WS 98/99 und SS 99

Vorträge bisher (SS99, WS '98/99)

• 18.06.99
Kompositionsgraphen und freie Erweiterungen von Kategorien

Lutz Schröder

Überraschend häufig begegnet man in der Mathematik Strukturen, die schwächer sind als Kategorien in dem Sinne, daß die Komponierbarkeit von Morphismen nur eingschränkt gegeben oder gar etwa das Assoziativgesetz verletzt ist. Beispiele sind einerseits "schlechte Konstrukte", d.h. Ansammlungen strukturierter Mengen (etwa Wahrscheinlichkeitsräume) mit nicht kompositionsstabilen Morphismen, andererseits auch "naiv" gebildete Quotienten von Kategorien. Ferner dienen solche Strukturen als Systeme von Erzeugenden und Relationen für Kategorien.

Ein Formalisierungsansatz für dieses Phänomen ist der Begriff des Kompositionsgraphen, d.h. eines Graphen mit einer partiellen Komposition, die einzig dem Axiom genügt, daß komponierbare Paare kommutative Dreiecke ergeben; die Bedeutung weiterer Axiome, insbesondere verschiedener Assoziativ- und Identitätsgesetze, wird dann im einzelnen untersucht. Ein Hauptaspekt bei der weiteren Nachforschung ist die Frage, welche Teile der Kategorientheorie sich in diesen allgemeineren Kontext übertragen lassen; es zeigt sich hierbei, daß sich insbesondere für die Begriffe "natürliche Transformation", "natürlicher Isomorphismus", "adjungierter Funktor" und "Äquivalenz" Verallgemeinerungen angeben lassen, die sich anhand damit verbundener Resultate als die "richtigen" Definitionen darstellen.

• 25.06.99
Aufgrund des Bremer CoFI-Treffens findet kein Extra-Treffen statt.
• 02.07.99
Visuelle regelbasierte objektorientierte Programmierung

Berthold Hoffmann

Mit Graphtransformationen lässt sich das Verhalten von Systemen spezifizieren, insbesondere wenn diese Systeme interaktiv sind und graphisch sind.

Im Vortrag geht es um Ideen, das Konzept der Graphtransformation zu einer vollständigen visuellen Spezifikations- und Programmiersprache weiter zu entwickeln.

Im Vordergrund stehen Überlegungen zu folgenden Aspekten:

• Graphstrukturierung (hierarchische Graphen)
• funktionale Abstraktion (Graphprozeduren)
• Datenabstraktion (Graphklassen)
• 11.06.99
Eine Einführung in Coalgebraische Methoden

Christoph Lüth

In den letzten Jahren sind sog. coalgebraische Methoden immer öfter in Erscheinung getreten, als genereller Rahmen für Bisimulationen (Co-Induktion), als Semantik für unendliche Datentypen (Listen/Streams) oder auch im Zusammenhang mit "hiding" und beobachtbarer oder Verhaltensgleichheit.

In diesem Vortrag würde ich gerne zeigen, wie man Coalgebra als einfache Dualisierung von Algebra erhält, indem man die Äquivalenz von Algebra und Monaden ausnutzt, und in der Basiskategorie des Monaden einfach alle Pfeile umdreht. Etwas allgemeiner können wir induktive Datentypen als kleinste Fixpunkte und initiale Algebren betrachten; der entsprechende duale Begriff ist der größte Fixpunkt und terminale Algebren. Ich werde versuchen, diese Begriffe alle in einen allgemeinen Rahmen zu bringen, zu zeigen, wie man coalgebraische Methoden als einfache und systematische Dualisierung von algebraischen Methoden erhält, und mit Beispielen zu zeigen, wozu all dieses nützlich sein kann.

• 21.05.99
The semantics of the Common Algebraic Specification Language (CASL)

Till Mossakowski

CASL is a language that has been designed in a collaborative effort with the goal to achieve a standard in the area of specification languages. An important aspect of CASL is that it has a complete mathematical semantics. In this talk, I will present some aspects of the CASL semantics:

• The role of the semantics in the design process of CASL
• Why and where is the CASL semantics needed?
• The style of the rules of the CASL semantics
• Example rules of the CASL semantics
• Institution independence of the semantics of CASL-in-the-large

More about CASL and the Common Framework Initiative.

• 23.04.99
Conference Report: ETAPS'99

Christoph Lüth.

The European Joint Conferences on Theory and Practice of Software ETAPS'99 bill themselves as

the new European forum for academic and industrial researchers working on topics relating to Software Science. During 8 days, ETAPS will give you the opportunity to choose between more than 100 regular papers covering a wide range of topics from Theory to Practice, 7 invited lectures, 6 tutorials, and 5 satellite events offering dozens more talks!

I shall endeavour to truthfully report on this extravaganza.
• 09.04.99
ROSI, IKS und Wahrnehmung

Björn Gottfried

Es wird der Roboter-Simulator ROSI und das Forschungsprojekt Integration Kognitiver Systeme an der FH-Hamburg beschrieben, in dem es um den Bau autonomer mobiler Roboter geht.

Aufgrund der Bedeutung der Wahrnehmung bei mobilen Robotern werden einige Aspekte der Robotik aus der Perspektive der Wahrnehmungspsychologie beschrieben.

• 16.04.99
Conference Reports: FEmSys'99 and HSCC'99

Peter Amthor

The talk is about two conferences I visited recently and shall give an overview accompanied by several more detailed remarks to certain contributions.

FEmSys'99- Workshop on Formal Design of Safety Critical Embedded Systems This workshop combined academic tutorials and industrial user's lectures with a tool exhibition with respect to the following topics:
• Hybrid modelling & simulation
• Object-orientation and reactive programming
• Synchronous Programming
• Distribution of Reactive Programs
• Model-checking
• Tool certification and code validation
HSCC'99 - HYBRID SYSTEMS: COMPUTATION AND CONTROL The focus of this workshop was on modeling, control synthesis, design and verification of hybrid systems.
• 12.03.99
Multi-Logik-Systeme als Basis für heterogene Spezifikation und Entwicklung

Till Mossakowski

Motivation:

Bei dem Einsatz formaler Methoden zur Entwicklung korrekter Software, insbesondere bei großen Softwareentwicklungsprojekten, an denen viele Personen und möglicherweise auch mehrere Entwicklungsteams beteiligt sind, kann man nicht davon ausgehen, das eine einzige formale Spezifikationssprache mit einer einheitlichen Entwicklungsumgebung zum Einsatz kommt. Für verschiedene Zwecke werden von unterschiedlichen Beteiligten mehrere Sprachen und Werkzeuge gleichzeitig in die Entwicklung eingebracht. Um die Wirksamkeit vielfältiger Konzepte und Methoden innerhalb einer Systementwicklung zu gewährleisten, müssen sie semantisch verträglich sein.

Inhalte:

Was ist eine Logik? Formalisierung des Begriffs
Logik-unabhängige Spezifiktionssprachen
Zwei Typen von Abbildungen zwischen Logiken: Repräsentation und Projektion/Kombination
"Ausleihen" von Theorembeweisern
Heterogene Spezifikationssprachen (basierend auf einem Logik-Graph)

• 05.03.99
CSP und temporale Logik

Holger Schlingloff

In diesem informellen Vortrag will ich einige Folklore zu Logik und Automaten rezitieren; Themen sind u.a.: Temporallogik - mu-Kalkül - Büchi-Automaten - Transitionssysteme - CSP
• 26.02.99
Eine kleine Einführung in den pi-Kalkül

Christoph Lüth

Der pi-Kalkül ist ein auf Robin Milner, David Walker und Joachim Parrow zurückgehender Kalkül zur Studie der Theorie von nebenläufigen Prozessen. Der pi-Kalkül soll dabei weniger eine weitere Spezifikationssprache für nebenläufige Systeme à la CSP oder CCS sein, sondern vielmehr ein grundlegender Kalkül zur Modellierung dieser Systeme (wie der lambda-Kalkül für sequentielle Programme) wobei die Benennung von Prozessen die grundlegende Operation ist.

Mein Vortrag gründet sich im wesentlichen auf Robin's Papier The Polyadic pi-Calculus: a Tutorial. Ich werde den einfachen (monadischen) pi-Kalkül vorstellen, die Erweiterung zum polyadischen pi-Kalkül sowie Sorting und higher-order, und die Verbindungen zu linearer Logik skizzieren.

• 12.02.99
Algebraische Spezifikation Nebenläufiger Systeme

Markus Roggenbach

Der Vortrag beruht auf dem Kapitel

E.Astesiano, M.Broy, G.Reggio:
Algebraic Specification of Concurrent Systems

aus dem IFIP Buch

Astesiono, Kreowski, Krieg-Brückner (eds):
Algebraic Foundations of Systems Specification.

Dieses Kapitel stellt Methoden zusammen, die es erlauben, sowohl nebenläufige als auch algebraische Aspekte eines Systems zu spezifizieren. Die AutorInnen ordnen die Spezifikationsmethoden in vier Gruppen:
• A1: algebraic techniques are used at the metalevel
• A2: a concurrent specification language is complemented with the possibility of abstractly specifying the (static) data
• A3: algebraic specifications having ¨dynamic sorts¨
• A4:abstract data types which change along time

Für den Vortrag habe ich aus der Vielzahl der vorgestellten Methoden für jede dieser Gruppen eine repräsentative ausgewählt. Dies sind im einzelnen CCS (A1), Lotos (A2), Labelled Transition Logic (A3) und Evolving Algebras (A4). An einem einfachen Musterbeispiel will ich sowohl die Möglichkeiten als auch die Grenzen dieser Spezifikationsmethoden aufzeigen. Dabei hoffe ich auf eine intensive Diskussion mit Euch, was an den verschiedenen Methoden überzeugt, aber auch darüber, an welchen Stellen sie ¨verbesserungswürdig¨ sind.

• 05.02.99
Partielle Logik höherer Stufe mit Untersorten als Erweiterung von CASL

Till Mossakowski

CASL (The Common Algebraic Specification Language) ist eine Sprache zur Spezifikation von Datyentypen, die Logik erster Stufe, partielle Funktionen und Untersorten kombiniert. In dieser Arbeit wird CASL mit Funktionen und Prädikaten höherer Stufe verallgemeinert. Dies ist insbesondere wichtig, um funktionale Programme, die oft mit höheren Funktionen arbeiten, spezifizieren zu können.

Die Kombination von Partialität, Untersorten und höheren Funktionen wird schrittweise über eine Reduktion auf den jeweils vorhergehenden Schritt eingeführt. Durch diese modulare Vorgehensweise kann die Interaktion verschiedener Features besser in den Griff bekommen werden. Verschiedene Entwurfsalternativen werden u.a. unter dem Aspekt einer treuen Einbettung von CASL nach higher-order CASL diskutiert.

(In Zusammenarbeit mit Anne Haxthausen und Bernd Krieg-Brückner)

• 15.01.99: Bericht von der 11. Internationalen Konferenz der Z-Benutzer ZUM'98

  Christoph Lüth

  Die ZUM ist die zentrale Konferenz für alle Z-Benutzer, Entwickler (insbesondere von Tools) und Interessierte; diese Konferenz gibt deshalb einen repräsentativen Eindruck vom Stand der Kunst auf diesem Gebiet.