Die Theorie Elementarer Netzsysteme (ENS) arbeitet auf zwei Ebenen: zum einen der Netzstruktur mit den Bedingungen und Ereignissen als Entitäten erster Stufe und andererseits dem aus der Anfangsmarkierung durch das Tokenspiel erzeugte Fallgraphen, der Entitäten zweiter Stufe miteinander verbindet.
Eine Vermittlung zwischen beiden Ebenen schaffen u.a. relationale Theorien, etwa die Halbordnungstheorie der Prozesse, die Concurrency-Theorie und die Theorie zyklischer Ordnungen. Thema meiner Dissertation ist ein kohärenter Auf- und Ausbau solcher Relationaltheorien hin zu einer Theorie 'generischer' ENS.
Der Vortrag beleuchtet einen Ausschnitt dieses Projekts, der mathematisch zum Zentrum gehört.
Es geht darum, die auf verschiedenen Konstruktionsstufen auftretenden Quotientenbildungen von Relationalstrukturen zu formalisieren:
Montag 16. Dezember 1996, 14 Uhr c.t. Raum D-220
A state space is a directed graph with a node for each reachable state and an arc for each possible state change. The talk describes how symmetries of the modelled system can be exploited to perform much more succinct state space analysis. The symmetries in duce equivalence classes of states and equivalence classes of state changes. It is then possible to construct a condensed state space where each node represents an equivalence class of state changes. Such a condensed state space is often much smaller than the full state space and it is also much faster to construct. Nevertheless, it is possible to use the condensed state space to verify the same kind of behavioural properties as the full state space. Hence, we do not lose analytic power. The talk defines state spaces and condensed state spaces in terms of Coloured Petri Nets. However, the techniques are general and they can be used for many other kinds of labelled transition systems.
The talk will be based on the paper: K. Jensen: Condensed State Spaces for Symmetrical Coloured Petri Nets. Formal Methods in System Design 9 (1996), Kluwer Academic Publishers, pp. 7-40.
The audience is expected to be familiar with the basic ideas of Coloured Petri Nets.
Dienstag 26. November 1996 14 Uhr c.t. Raum C-221
Processes are concisely defined in a way that some of them represent (concurrent) behaviour of elementary Petri nets. Thus, in constrast to standard definitions (Best, Reisig, Starke, etc.), a process is defined independently of any net, much like words or traces are defined regardless of any generative device (automaton, net or the like). Processes may be finite or infinite. Next, a simple definition of processes, concatenation is given and extended to sets of processes, i.e. process languages. Hence, we arrive to a considerable generalization of the ordinary algebra of regular (algebraic) languages. Some properties valid in the algebra of process languages will be demonstrated. Finally, analysis (''given a net, find a process language generated by it'') and synthesis (''given a process language, find a net that generates it'') problems will be posed and their solution outlined.
Dienstag 12. November 1996 14 Uhr c.t. Raum C-221
Strukturbisimulationen sind eine Klasse von Gleichheitsrelationen auf Petrinetzen mit vorteilhaften Eigenschaften. Im Rahmen meiner Diplomarbeit untersuche ich, wie sie auf höhere Petrinetze erweitert werden können, bzw. wie sie praktisch verwendbar sind (z.B. Abschluß unter Komposition und Verfeinerung).
Nach einer kurzen Einführung, in der ich die grundlegenden Begriffe und Definitionen erläutere, will ich mit den Teilnehmern meine bisherigen Ergebnisse diskutieren, um Schwächen an ihnen aufzudecken und neue Ideen zu sammeln.
Offene Fragen sind insbesondere die folgenden: