close

Anmelden

Neues Passwort anfordern?

Anmeldung mit OpenID

Laufzeitersetzung offener Workflownetze - im Institut für Informatik

EinbettenHerunterladen
Diplomarbeit
Laufzeitersetzung offener
Workflownetze
Nannette Liske
15. Juli 2008
Gutachter:
◦ Prof. Dr. Karsten Wolf
Institut f¨ur Informatik, Universit¨at Rostock
◦ Prof. Dr. Wolfgang Reisig
Institut f¨ur Informatik, Humboldt-Universit¨at zu Berlin
Hiermit erkl¨are ich, dass ich die vorliegende Diplomarbeit
selbsta¨ndig angefertigt habe. Es wurden nur die in der Arbeit
genannten Quellen benutzt. W¨ortlich oder sinngem¨aß
u¨bernommenes Gedankengut habe ich als solches
gekennzeichnet.
Ich bin damit einverstanden, dass ein Exemplar dieser Arbeit in
der Bibliothek des Instituts fu¨r Informatik der
Humboldt-Universita¨t zu Berlin ausgestellt wird.
Berlin, den 15. Juli 2008.
Nannette Liske
Inhaltsverzeichnis
Abbildungsverzeichnis
1 Einleitung
1.1 Motivation . . . . .
1.2 Ziele der Arbeit . .
1.3 Verwandte Themen
1.4 Gliederung . . . . .
7
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
9
9
10
11
12
2 Grundlagen
2.1 Modelle . . . . . . . . . . . .
2.1.1 Petrinetze . . . . . . .
2.1.2 Offene Workflownetze .
2.1.3 Serviceautomaten . . .
2.2 Bedienungsanleitung . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
13
13
14
15
17
21
.
.
.
.
.
25
25
25
26
31
33
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
3 neue Definitionen
3.1 Wissensfunktionen . . . . . . . .
3.1.1 Erreichbarkeitsfunktion . .
3.1.2 Fortf¨
uhrbarkeitsfunktion .
3.2 Laufzeitersetzung . . . . . . . . .
3.2.1 Eingabepl¨atze neu belegen
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
4 Instantane Laufzeitersetzungen
4.1 Algorithmus zur Bestimmung instantaner Laufzeitersetzungen
¨
4.1.1 Notwendigkeit der Uberpr¨
ufung auf Fortf¨
uhrbarkeit . .
4.2 Einschr¨ankungen der Netze . . . . . . . . . . . . . . . . . . .
4.2.1 Leere Transitionen im inneren Netz . . . . . . . . . . .
¨
4.2.2 Uberdeckte
Endmarkierungen . . . . . . . . . . . . . .
¨
4.2.3 Uberdeckte Markierungen . . . . . . . . . . . . . . . .
4.3 Korrektheit des Algorithmus InstantaneLE . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
35
37
40
41
41
42
43
45
5 Nebenl¨
aufige Laufzeitersetzungen
5.1 Algorithmus zum Erzeugen nebenl¨aufiger
5.2 Korrektheit . . . . . . . . . . . . . . . .
5.2.1 Leerer Vorbereich . . . . . . . . .
5.2.2 Nicht u
uhrbare Markierungen
¨berf¨
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
47
48
53
53
55
Laufzeitersetzungen
. . . . . . . . . . . .
. . . . . . . . . . . .
. . . . . . . . . . . .
5
Inhaltsverzeichnis
5.2.3 Korrektheit des Algorithmus Zerteilung . . . .
5.3 Heuristik . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.3.1 differenzierte Deadlockpr¨
ufung . . . . . . . . . . .
5.3.2 Verkleinung der Menge B . . . . . . . . . . . . .
5.4 Gr¨oßenreduktion durch nebenl¨aufige Laufzeitersetzungen
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
57
58
59
64
66
6 Fazit
69
Literaturverzeichnis
71
6
Abbildungsverzeichnis
2.1
2.2
2.3
2.4
2.5
oWFNs zweier Getr¨ankeautomaten . . . . . . . . . . .
Partnerautomat f¨
ur das Netz N1 aus Abb. 2.1 . . . . .
Komposition von N1 aus Abb. 2.1 und R aus Abb. 2.2
Bedienungsanleitung f¨
ur das Netz N1 aus Abb. 2.1 . . .
Teilmenge von Strategien ( -Relation) . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
17
19
20
22
23
3.1
3.2
3.3
3.4
3.5
3.6
3.7
3.8
oWFN mit Erreichbarkeitsfunktion . . . . . . . . . . . . . . . . . .
Berechnung der Fortf¨
uhrbarkeitsfunktion . . . . . . . . . . . . . . .
umgekehrtes Netz und umgekehrter Automat . . . . . . . . . . . . .
oWFN mit Fortf¨
uhrbarkeitsfunktion . . . . . . . . . . . . . . . . . .
Fortf¨
uhrbarkeitsfunktion f¨
ur nicht bedienbares oWFN . . . . . . . .
oWFN mit Fortf¨
uhrbarkeitsfunktion bei unbeschr¨ankter Umkehrung
Laufzeitersetzung offener Workflownetze gem¨aß OG aus Abb. 2.5 . .
Laufzeitersetzung, die keinen Eingabeplatz belegt . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
26
27
28
29
29
30
33
34
4.1
4.2
4.3
4.4
4.5
4.6
4.7
4.8
4.9
instantane Laufzeitersetzung gem¨aß OG von Abb. 2.4
Berechnung der instantanen Laufzeitersetzung . . . .
Wissensfunktionen K1 und K2 f¨
ur die Netze aus Abb.
Ausschnitt der Wissensfunktionen f¨
ur Abb. 4.3 . . . .
vollst¨andige instantane Laufzeitersetzung . . . . . . .
¨
Notwendigkeit der Uberpr¨
ufung in Zeile 9 . . . . . .
leere Transitionen im inneren Netz . . . . . . . . . .
u
¨berdeckte Endmarkierung . . . . . . . . . . . . . . .
u
¨berdeckte Markierung . . . . . . . . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
36
38
38
39
39
40
41
43
44
5.1
5.2
5.3
5.4
5.5
5.6
5.7
5.8
5.9
5.10
5.11
Berechnung nebenl¨aufiger Laufzeitersetzungen . . . . . . . . . .
Zerteilung von Laufzeitersetzungstransitionen . . . . . . . . . .
zwei offene Worfklownetze . . . . . . . . . . . . . . . . . . . . .
instantane Laufzeitersetzung zu Abb. 5.3 . . . . . . . . . . . . .
berechnete nebenl¨aufige Laufzeitersetzung . . . . . . . . . . . .
zerteilte Laufzeitersetzungstransitionen zur Tab. 5.4 . . . . . . .
anders zerteilte Laufzeitersetzungstransitionen zur Tab. 5.4 . . .
Test auf leeren Vorbereich . . . . . . . . . . . . . . . . . . . . .
Test auf nicht-¨
uberf¨
uhrbare Markierungen . . . . . . . . . . . .
Beispielnetze f¨
ur Heuristiken . . . . . . . . . . . . . . . . . . . .
Serviceautomat mit Wissensfunktion f¨
ur die Netze aus Abb. 5.10
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
49
49
50
51
52
52
52
53
56
59
60
. .
. .
4.1
. .
. .
. .
. .
. .
. .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
7
Abbildungsverzeichnis
5.12
5.13
5.14
5.15
5.16
8
nicht u
uhrbare Markierungen . . . . . . . . . . . . . .
¨berf¨
modifizierter Ausschnitt aus ZerteilungsSchritt . . . .
Problembeispiel f¨
ur Heuristiken . . . . . . . . . . . . . . .
modifizierter Ausschnitt aus Zerteilung . . . . . . . . .
exponentiell viele instantane Laufzeitersetzungstransitionen
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
60
61
63
65
67
1 Einleitung
Gesch¨aftsprozesse sind ein standardisiertes Verfahren, um organisatorische Vorg¨ange zu
beschreiben und zu realisieren. Dabei besteht ein Gesch¨aftsprozess aus einer Menge von
Aktivit¨aten, denen eine Ausf¨
uhrungsvorschrift in beliebiger Form zugrundeliegt. Umfasst ein Gesch¨aftsprozess mehrere, untereinander kommunizierende Teile, welche r¨aumlich oder organisatorisch unabh¨angig voneinander verlaufen, so spricht man auch vom
verteilten Gesch¨aftsprozess. Die Teile eines solchen Prozesses werden Services genannt.
In der Gesch¨aftswelt spielt die Ersetzbarkeit von Services durchaus eine große Rolle.
¨
Firmenstrukturen unterliegen st¨andigen Ver¨anderungen, Ubernahmen
ganzer Gesch¨aftszweige durch andere Firmen sind keine Seltenheit. Mitunter m¨ochte auch eine Firma
einen Kundenstamm, oder einen bestimmten Teil davon, in einen neuen (rentableren)
Gesch¨aftsprozess u
¨bernehmen.
1.1 Motivation
In verschiedenen Arbeiten ist die Ersetzbarkeit von Services bereits untersucht worden
(siehe Verwandte Themen). Dabei wurde allerdings oft das Augenmerk nur auf die Austauschbarkeit, also die Ersetzung zur Entwurfszeit, gerichtet. Das bedeutet, es wurde
untersucht, inwiefern ein bestimmter Service anstelle eines anderen verwendet werden
kann. In manchen F¨allen ist die Ersetzung zur Entwurfszeit jedoch nur bedingt sinnvoll,
weil es sich um sehr langlebige oder kritische Vorg¨ange handelt. Ebenso ist das Szenario
denkbar, dass nicht genug Ressourcen vorhanden sind, um alle laufenden Instanzen eines
alten Service bis zu Ende zu f¨
uhren und gleichzeitig alle neuen Interaktionen mit dem
neuen Service zu beginnen.
Beispiele f¨
ur langwierige Gesch¨aftsprozesse bieten h¨aufig jene Abl¨aufe, welche in Beh¨orden und Verwaltungen vorkommen. Bei diesen verteilten Gesch¨aftsprozessen k¨onnen sich
mitunter aufgrund ver¨anderter Gesetzeslagen die Abarbeitungsvorschriften a¨ndern, zum
Beispiel bei Lebensversicherungen. In solch einem Fall sollen die laufenden Vertr¨age
nat¨
urlich nicht gek¨
undigt werden. Vielmehr m¨ochte man das neue Gesetz soweit wie
m¨oglich auf die laufenden Services anwenden. Eine erste theoretische Arbeit auf die-
9
1 Einleitung
sem Gebiet stammt von Ryu et al. [RCS+ 08]. Die Autoren haben die Ver¨anderungen
eines laufenden Service betrachtet und ihre Auswirkungen hinsichtlich seiner Bedienung
untersucht.
1.2 Ziele der Arbeit
Die vorliegende Arbeit f¨
uhrt ein neues Konzept zur Ersetzung von Services zur Laufzeit
ein. Das gesuchte Szenario erf¨
ullt folgende Bedingungen:
1. Ein Service wird zur Laufzeit in einen anderen Service u
uhrt.
¨ berf¨
2. Die bislang geleistete Arbeit soll bewahrt bleiben, d.h. ein Abbruch der Kommunikation ist ausgeschlossen.
3. Der Austausch geschieht unbemerkt vom Kommunikationspartner (Kunden).
Oft enthalten Gesch¨aftsprozesse mehrere, zeitlich unabh¨angige Arbeitsabl¨aufe. Diese nebenl¨aufigen Aspekte sollen sich auch in der Laufzeitersetzung der Services widerspiegeln,
weshalb die Ziele noch um folgende Punkte erg¨anzt werden:
4. Sofern m¨oglich, soll die Laufzeitersetzung der Services nebenl¨aufig, in mehreren
Schritten, durchgef¨
uhrt werden.
5. Die Laufzeitersetzung soll sowohl f¨
ur alle m¨oglichen Kommunikationspartner als
auch f¨
ur einen beliebig ausgew¨ahlten Teil bestimmt werden k¨onnen.
Als Modell zur Beschreibung der Gesch¨aftspozesse werden offene Workflownetze verwendet. Das zu ber¨
ucksichtigende Verhalten der Partner, die Strategien, sind in Form
von Bedienungsanleitungen bzw. annotierten Automaten gegeben. Die Berechnung der
sogenannten Laufzeitersetzungen erfolgt in zwei Stufen:
◦ Zun¨achst wird ein Algorithmus pr¨asentiert und in seiner Korrektheit bewiesen,
welcher zu zwei gegebenen offenen Workflownetzen sowie einer als annotierter Automat gegebenen Strategiemenge die vollst¨andige instantane Laufzeitersetzung findet.
◦ Darauf aufbauend kann ein Algorithmus angegeben werden, der Nebenl¨aufigkeiten
der Workflownetze ber¨
ucksichtigt. Dazu werden instantane Laufzeitersetzungen
derart modifiziert, dass nebenl¨aufige Arbeitsabl¨aufe auch nebenl¨aufig vom einen
Netz in das andere u
uhrt werden.
¨berf¨
10
1.3 Verwandte Themen
1.3 Verwandte Themen
¨
In der Literatur finden sich viele verschiedene Aquivalenzbegriffe
f¨
ur Gesch¨aftsprozesse bzw. Services. Bereits 1971 definiert Milner die Simulation von Prozessen [Mil71].
Es handelt sich dabei um eine Relation zwischen den Zust¨anden zweier Prozesse (Zustandsautomaten). In [Mil89] erweitert der Autor das Konzept noch um die Bisimulation
zweier Prozesse.
¨
Neue Aquivalenzbegriffe,
welche sich nicht auf die Vorg¨ange innerhalb der Prozesse beziehen sondern auf die Bedienung (Interaktion mit dem Partner), tauchen im Wesentlichen
erst nach der Jahrtausendwende in der Literatur auf. Beispielsweise beschreibt Martens
in [Mar03] die Bedienbarkeits¨aquivalenz von Services. Dabei gilt, dass ein Service gegen
einen anderen Service zur Entwurfszeit ausgetauscht werden kann, wenn alle Strategien
des einen auch Strategien des anderen Service sind. Ist die Menge der Strategien beider
Services identisch, so heißen sie bedienbarkeits¨aquivalent. Auf Grundlage der Bedienbarkeits¨aquivalenz besch¨aftigt sich Richter mit der Frage, ob ein Service durch einen
anderen ausgetauscht werden kann, wenn dabei nur eine bestimmte Strategie erhalten
bleiben soll [Ric02].
¨
¨
Van Glabbeek gibt in [Gla01] eine Ubersicht
weiterer gebr¨auchlicher Aquivalenzbegriffe.
+
¨
Auf Basis dieser Begriffe wurden in [HDvdA 05] verschiedene Aquivalenbegriffe
Workflownetze untersucht.
In [SMB08] definieren die Autoren die Austauschbarkeit von Services anhand von Bedienungsanleitungen (Operating Guidelines). Ihre Herangehensweise erlaubt die Beschr¨ankung auf eine beliebige Teilmenge von Strategien. Das bedeutet, dass die Services f¨
ur eine beliebig ausgew¨ahlte Klasse von Partnern austauschbar sind. Mithilfe des
Software-Tool Fiona [LMSW06] l¨asst sich diese Form der Austauschbarkeit, und damit
auch die Bedienbarkeits¨aquivalenz [Mar03], effizient bestimmen.
¨
Die bisher genannten Aquivalenzbegriffe
f¨
ur Services bzw. Workflownetze beziehen sich
auf die Austauschbarkeit, also die Ersetzung zur Entwurfszeit. Seit kurzer Zeit ist auch die
Ersetzung zur Laufzeit Gegenstand theoretischer Arbeiten. So untersuchen in [RCS+ 08]
die Autoren f¨
ur Gesch¨aftsprotokolle (business protocols) – einem zustandsbasierten Modell f¨
ur Gesch¨aftsprozesse – die Ersetzbarkeit von Zust¨anden zur Laufzeit. Dabei entscheiden sie, ob ein Kommunikationspartner von einem Zustand p eines solchen Protokolls dasselbe Kommunikationsmuster verwenden kann wie von einem Zustand q eines
anderen Protkolls. Lassen sich alle Zust¨ande eines Gesch¨aftsprotokolls P1 ersetzen durch
Zust¨ande von P2 , dann heißt P1 gesamt zur Laufzeit ersetzbar durch P2 . Die Autoren
betrachten bereits die Beschr¨ankung auf bestimmte Kommunikationspartner und geben
auch einen Algorithmus zur Bestimmung der Ersetzungsregeln an.
11
1 Einleitung
Im Gegensatz zu zustandsbasierten Gesch¨aftsprotokollen mit synchroner Kommunikation m¨ochten wir auch Prozesse mit asynchroner Kommunikation zur Laufzeit ersetzen k¨onnen. Als erste Arbeit beschreibt [Lis07] ein solches Szenario – die Laufzeitersetzung von Serviceautomaten. Serviceautomaten sind Zustandsautomaten mit asynchronem Nachrichtenkanal. Die Kommunikationspartner sind als Bedienungsanleitung dargestellt. Als Ergebnis der Arbeit kann folgendes Problem algorithmisch gel¨ost werden:
Gegeben seien zwei Serviceautomaten P1 und P2 sowie eine Bedienungsanleitung OG.
Es soll die maximale Laufzeitersetzung von P1 nach P2 berechnet werden, wobei als
Interaktionspartner nur solche gem¨aß OG in Frage kommen.
Die vorliegende Diplomarbeit greift das Konzept der Laufzeitersetzung von Serviceautomaten auf und u
¨ bertr¨agt es auf offene Workflownetze [MRS05, LMW07]. Dieses Modell ist in der Lage, nebenl¨aufige Arbeitsabl¨aufe, welche in Gesch¨aftsprozessen h¨aufig
vorhanden sind, explizit darzustellen. Die asynchrone Kommunikation wird in offenen
Workflownetzen beibehalten.
1.4 Gliederung
Die weitere Arbeit ist folgendermaßen aufgebaut: Das Kapitel Grundlagen f¨
uhrt zun¨achst
die zugrundeliegenden Modelle zur Darstellung von Gesch¨aftsprozessen ein. Darauf aufbauend folgen die Definitionen von Wissensfunktionen und Laufzeitersetzung im Abschnitt neue Definitionen. Die Wissensfunktionen dienen der Berechnung von Laufzeitersetzungen. Eine einfache Form von Laufzeitersetzungen, die instantanen Laufzeitersetzungen, werden im vierten Kapitel untersucht. Neben der Definition und einigen Beispielen enth¨alt dieser Abschnitt auch einen Algorithmus zur Bestimmung der vollst¨andigen
instantanen Laufzeitersetzung sowie den Beweis seiner Korrektheit.
Es folgt im Kapitel Nebenl¨aufige Laufzeitersetzungen die Erweiterung auf beliebige Laufzeitersetzungen. Die Ergebnisse eines vergleichsweise einfachen Algorithmus werden anhand von erl¨auternden Beispielen diskutiert. Anschließend pr¨asentieren wir eine heuristische Modifikation des Algorithmus, welche deutlich mehr Nebenl¨aufigkeiten finden
kann. Die Korrektheit der Algorithmen wird jeweils formal bewiesen.
Im Fazit findet sich eine inhaltliche Zusammenfassung der gewonnenen Erkenntnisse.
Daran kn¨
upft ein Ausblick, welcher offene Fragen nennt und M¨oglichkeiten zur Weiterentwicklung der in dieser Arbeit vorgestellten Konzepte ausf¨
uhrt.
12
2 Grundlagen
2.1 Modelle
Typischerweise wird ein Service von anderen Services eingebunden oder bindet selbst
weitere Services ein. Das Paradigma des Service-Oriented Computing (SOC) beschreibt
die Interaktion von Services [Pap01]. Eine h¨aufige Form der Implementation von Services stellen Web Services [GGKS02] dar. Verschiedene große Firmen, darunter IBM und
Microsoft, haben 2002 einen gemeinsamen, XML-basierten Standard zur Spezifikation
von Web Services, die Business Process Execution Language (BPEL) [AAA+ 06], festgelegt. Es gibt verschiedene M¨oglichkeiten, den von einem BPEL-Programm beschriebe¨
nen Service, mathematisch zu modellieren. Einen guten Uberblick
bietet [BK06]. Offene
Workflownetze (oWFN) [MRS05, LMW07] basieren auf den von van der Aalst vorgeschlagenen Workflownetzen [Aal98]. Sie stellen eine spezielle Form von Petrinetzen
[Rei82] dar und eignen sich besonders gut f¨
ur theoretische Analyseverfahren [LMSW06].
Ein offenes Workflownetz beschreibt sowohl das interne Verhalten eines Service als
auch sein Interface, also die Schnittstelle zur Kommunikation mit anderen Services.
Durch die asynchrone Arbeitsweise von Petrinetzen lassen sich die in Gesch¨aftsprozessen auftretenden Nebenl¨aufigkeiten hervorragend darstellen. Mithilfe von BPEL2oWFN
k¨onnen BPEL-Programme zu Analysezwecken in offene Workflownetze konvertiert werden [HSS05, Loh08].
Bedienbare Services sind solche, f¨
ur die es einen Partner-Service gibt, mit dem er sinnvoll
interagieren kann [Mar03, Sch05]. Fehler im Design von Services werden somit durch die
Untersuchung seiner Bedienbarkeit erkannt. Ein Analysewerkzeug f¨
ur die Bedienbarkeit
offener Workflownetze ist mit Fiona gegeben [LMSW06]. Dar¨
uberhinaus l¨asst sich mit
Fiona die Bedienungsanleitung [MS05, LMW07] eines Service konstruieren. Die Bedienungsanleitung charakterisiert alle sinnvoll interagierenden Partner in einer kompakten
Darstellung. Weitere Analysen des zugrundeliegenden Petrinetzes lassen sich beispielsweise mit dem Low Level Analyzer (LoLA) [Sch00] durchf¨
uhren .
13
2 Grundlagen
2.1.1 Petrinetze
Definition 2.1 (Petrinetz)
Ein Petrinetz N ist ein Tupel N = [P, T, F, W, m0] aus den endlichen, disjunkten Mengen
P (Pl¨atze) und T (Transitionen), der Relation F ⊆ (T × P ) ∪ (P × T ) (B¨ogen), der
Abbildung W : F → N (Bogenvielfachheit) sowie einer initialen Markierung m0 .
F¨ur nicht-vorhandene B¨ogen, also Paare [x, y] ∈
/ F , vereinbaren wir, dass der Ausdruck
W ([x, y]) dem Wert 0 entspricht.
Wir sagen, in einem Petrinetz gibt es von einem Element x (Platz oder Transition) einen
Pfad zu einem Element y, falls es weitere Elemente x0 . . . xn ∈ P ∪ T gibt, sodass x = x0 ,
y = xn und [xi , xi+1 ] ∈ F .
Definition 2.2 (Markierung)
Als bags(X) bezeichnen wir die Menge aller Multimengen ¨uber X, das sind alle Abbildungen X → N. Eine Markierung m eines Petrinetzes ist eine Multimenge von Pl¨atzen des
Netzes, also m ∈ bags(P ). Wir schreiben f¨ur Markierungen auch kurz m = [p0 , . . . , pn ],
wobei jeder Platz entsprechend h¨aufig der Anzahl seines Vorkommens in der Multimenge
auftritt. Die Markierung [] heißt leere Markierung.
Jede Markierung m : P → N entspricht kanonisch einer Markierung m⊇ auf einer
m(p), p ∈ P
. Zur Vereinfachung der
gr¨oßeren Platzmenge P ⊇ P mit m⊇ (p) =
0,
sonst
Schreibweise ist im folgenden bei gr¨oßeren Platzmengen einfach von m die Rede.
Grundlegende Rechenoperationen und Vergleiche lassen sich auf Markierungen u
¨bertragen, indem sie platzweise angewendet werden. In diesem Sinne sind die Summe
bzw. die Differenz von Markierungen zu verstehen als Summe bzw. Differenz von Multimengen:

(m1 + m2 )(p) := m1 (p) + m2 (p)

(m1 − m2 )(p) := m1 (p) − m2 (p)
∀p ∈ P

m1 ≤ m2 ⇔ m1 (p) ≤ m2 (p)
Die grafische Darstellung von Petrinetzen erfolgt u
ur Pl¨atze),
¨blicherweise durch Kreise (f¨
Rechtecke (f¨
ur Transitionen) und Pfeile (f¨
ur B¨ogen). Die Bogenvielfachheiten werden als
Zahl an den entsprechenden Pfeilen markiert. Eine Ausnahme bilden dabei einfache
¨
B¨ogen – hier wird der Ubersichtlichkeit
die 1 weggelassen. B¨ogen mit Vielfachheit 0
werden als nicht vorhanden betrachtet und auch nicht eingezeichnet. Anfangsmarkierung
der abgebildeten Netze ist – wenn nicht anders erw¨ahnt – [p0 ] bzw. [v0 ].
14
2.1 Modelle
Definition 2.3 (Vor- und Nachbereich)
Der Vorbereich einer Transition t ist die Markierung •t mit •t(p) = W ([p, t]). Analog
ist der Nachbereich definiert als Markierung t• mit t•(p) = W ([t, p]). Eine Transition
mit leerem Vor- und Nachbereich heißt leere Transition.
Definition 2.4 (Schalten von Transitionen)
Eine Transition t ist aktiviert in einer Markierung m, wenn gilt: m ≥ •t. Befindet
sich das Petrinetz in der Markierung m, so kann eine aktivierte Transition t zu einer
t
Folgemarkierung m = m − •t + t• schalten (m −
→ m ).
Definition 2.5 (Erreichbarkeit)
Die Erreichbarkeit von Markierungen ist induktiv definiert. Dabei heißt im Netz N eine
Markierung m von m aus erreichbar, wenn
◦ m = m oder
t
◦ es eine Transition t mit m −
→ m gibt und m von m aus erreichbar ist.
Im Petrinetz N sei RN (m) die Menge aller von m aus erreichbaren Markierungen. Dann
enth¨alt RN (m0 ) alle erreichbaren Markierungen des Netzes N.
Definition 2.6 (Beschr¨
anktheit)
Ein Petrinetz heißt beschr¨ankt, wenn die Menge aller erreichbaren Markierungen endlich ist. k-beschr¨ankt heißt das Netz, falls bei allen erreichbaren Markierungen kein Platz
mehr als k Marken besitzt.
2.1.2 Offene Workflownetze
Workflownetze sind spezielle Petrinetze zur Beschreibung von Gesch¨aftsprozessen. Bei
offenen Workflownetzen existiert zus¨atzlich ein Interface. Dabei handelt es sich um Einund Ausgabepl¨atze, welche zur Kommunikation mehrerer offener Workflownetze untereinander dienen. Dadurch lassen sich auch verteilte Gesch¨aftsprozesse theoretisch beschreiben.
Im u
¨bertragenen Sinne ist das Interface als Nachrichtenkanal zu verstehen, wobei vom
¨
Inhalt der Nachrichten und der Art der Ubertragung
(Brief, E-Mail, . . . ) abstrahiert wird
auf ihre bloße Existenz. Die Richtung einer Nachricht ist darin kodiert, ob sie auf einem
Eingabe- oder einem Ausgabeplatz liegt. F¨
ur die Systemanalyse ist diese Modellebene
vollkommen ausreichend.
15
2 Grundlagen
Definition 2.7 (Offenes Workflownetz)
Ein offenes Workflownetz (oWFN) N = [P, T, F, W, m0 , ΩN ] ist eine Erweiterung des
Petrinetzes [P, T, F, W, m0 ], wobei
◦ P die disjunkte Vereinigung der Eingabepl¨atze PI , Ausgabepl¨atze PO und inneren
Pl¨atze PN darstellt,
◦ F ∩ (PO × T ) = ∅ und F ∩ (T × PI ) = ∅,
◦ die Anfangsmarkierung m0 sowie alle Endmarkierungen nur innere Pl¨atze beinhalten und
◦ in keiner Endmarkierungen mf ∈ ΩN eine Transition aktiviert ist.
Als Interface des Netzes bezeichnen wir die Nachrichtenkan¨ale, die durch PI und PO
repr¨asentiert sind. Die B¨ogen F k¨onnen von Eingabepl¨atzen nur ausgehend und bei
¨
Ausgabepl¨atzen nur eingehend sein. Ubertragen
in die reale Welt entspricht dies beispielsweise beim klassischem Briefverkehr dem Umstand, dass ein verschickter Brief vom
Absender nicht zur¨
uckgeholt werden kann. Der Postweg ist dabei f¨
ur den Absender ein
Ausgabekanal und f¨
ur den Empf¨anger ein Eingabekanal. In den Abbildungen sind die
Netze mit einem gestrichelten Rahmen versehen, welcher das Interface symbolisiert. Die
Eingabepl¨atze befinden sich stets links und die Ausgabepl¨atze rechts auf diesem Rahmen.
In Abbildung 2.1 sind zwei offene Workflownetze eines fiktiven Getr¨ankeautomaten dar¨
gestellt. Uber
Kn¨opfe am Automaten kann sich der Kunde beispielsweise zwischen Kaffee
(Eingabe K) und Tee (Eingabe T ) entscheiden. Im Startzustand wartet das dargestellte
Netz auf eine dieser beiden Eingaben. Anschließend wirft der Kunde Geld ein (Eingabe e) und der Automat entscheidet selbst¨andig, ob er nun das Getr¨ank ausgibt (Ausgabe BK bzw. BT ) oder mehr Geld verlangt (Ausgabe G). Nach der Ausgabe des Getr¨anks
endet die Interaktion. Der Kunde hat aber auch die M¨oglichkeit, w¨ahrend der iterativen
Geldeingabe vorzeitig abzubrechen (Eingabe A). In diesem Fall gibt der Automat die
erhaltenen M¨
unzen zur¨
uck (Ausgabe W ) und die Interaktion endet ebenfalls.
Jede Markierung eines offenen Workflownetzes N fassen wir als Summe der Markierungen der Eingabe-, Ausgabe- und inneren Pl¨atze auf (m = mI + mO + mN ). Die
Kurzschreibweise mN bezeichnet dabei die Markierung der inneren Pl¨atze von N, entsprechend stellen mI und mO die Markierungen der Eingabe- bzw. Ausgabepl¨atze dar.
Definition 2.8 (Inneres Netz)
Das innere Netz von N ist das Netz ohne die Interfacepl¨atze sowie ohne deren adjazente
B¨ogen. Die Anfangs- und Endmarkierungen bleiben erhalten.
16
2.1 Modelle
N1
N2
p0
v0
K
K
v3
T
p1
p2
p4
G
T
W
e
p5
e
v1
v5
G
W
v4
BK
A
BK
A
BT
p3
p6
BT
v2
v6
Endmarkierungen sind [p3 ], [p6 ] bzw. [v2 ], [v6 ]
Abbildung 2.1: oWFNs zweier Getr¨ankeautomaten
In dieser Arbeit betrachten wir nur solche offenen Workflownetze, deren inneres Netz
beschr¨ankt ist. Desweiteren schließen wir leere Transitionen im inneren Netz aus. Die
Begr¨
undung f¨
ur diese Einschr¨ankung folgt im Abschnitt 4.2.
¨
Definition 2.9 (Uberdeckung)
Eine Markierung m eines oWFN u
¨berdeckt eine andere Markierung m , falls f¨ur alle
inneren Pl¨atze p ∈ PN gilt: m(p) ≥ m (p). Gibt es sogar einen Platz mit m(p) > m (p)
¨
so sprechen wir von echter Uberdeckung.
Man beachte, dass es nur von den inneren Pl¨atzen eines Netzes abh¨angt, ob eine Markierung eine andere u
urde [p1 , p4 ] die Markierung [p1 , e]
¨ berdeckt. In Abbildung 2.1 w¨
echt u
¨berdecken. Auch [p1 ] u
¨ berdeckt [p1 , e], jedoch nicht echt.
2.1.3 Serviceautomaten
Nachdem wir als Modell f¨
ur die Gesch¨aftsprozesse offene Workflownetze betrachtet haben, wollen wir und nun ein Modell f¨
ur das Verhalten der Partner des Gesch¨aftsprozesses
anschauen. Im Gegensatz zu den offenen Workflownetzen, welche das interne Verhalten
der Gesch¨atsprozesse widerspiegeln, interessieren wir uns bei den Partnern lediglich f¨
ur
die Kommunikation nach außen.
17
2 Grundlagen
Als einfaches Modell, welches internes Verhalten vernachl¨assigt, bieten sich Serviceautomaten an. Eine Einf¨
uhrung in dieses Modell bieten beispielsweise [MS05]. Bei Serviceautomaten handelt es sich um Zustandsautomaten mit asynchronen Nachrichtenkan¨alen
als Interface. In [LMW07] ist eine M¨oglichkeit dargestellt, einen entsprechenden Serviceautomaten aus einem oWFN zu konstruieren. Dabei kann der erzeugte Automat als das
kommunikative Verhalten des urspr¨
unglichen Netzes betrachtet werden.
Definition 2.10 (Serviceautomat)
Ein Serviceautomat R = [Q, CI , CO , δ, q0 , ΩR ] mit Nachrichtenkan¨alen C ist ein endlicher Automat mit
◦ disjunkten Eingabekan¨alen CI und Ausgabekan¨alen CO , mit CI ∪ CO = C,
◦ einer endlichen Zustandsmenge Q,
◦ einer Zustands¨uberf¨uhrungsfunktion δ ⊆ Q × (CI ∪ CO ∪ {τ }) × Q und
◦ Endzust¨anden Ω ⊆ Q.
Von den Endzust¨anden aus werden keine Nachrichten versendet, d.h. wenn q ∈ Ω und
(q, x, q ) ∈ δ, dann ist x ∈ CI .
Wir verwenden die klassische Darstellung endlicher Zustandsautomaten, d.h. Zust¨ande
¨
sind Kreise, Uberf¨
uhrungen Pfeile, Anfangs- und Endzust¨ande sind mit eingehendem
Pfeil bzw. doppeltem Rand markiert. Zur grafischen Darstellung der Kommunikation
des Serviceautomaten wird an den Kanten bei eingehenden Nachrichten x ∈ CI ein
Fragezeichen vorangestellt, w¨ahrend ausgehende Nachrichten x ∈ CO mit einem Ausrufezeichen gekennzeichnet sind.
Der Serviceautomat in Abbildung 2.2 repr¨asentiert einen zu dem oben vorgestellten Getr¨ankeautomaten passenden Kunden. Dieser Kunde w¨ahlt entweder Kaffee (K) oder Tee
(T ) und wirft solange M¨
unzen ein (e) bis das Getr¨ank bezahlt ist. Anschließend nimmt
er das Getr¨ank entgegen (BK ). Wie man sieht, kann er aber auch den Bezahlvorgang
abbrechen und sein Wechselgeld annehmen (W ).
Definition 2.11 (Partnerautomat)
Seien N = [P, T, F, W, m0 , ΩN ] ein oWFN und R = [Q, CI , CO , δ, q0 , ΩR ] ein Serviceautomat. Wenn PI = CO und PO = CI , dann heißt R Partnerautomat f¨
ur N.
Dass die Interfaces zusammenpassen, garantiert noch nicht eine sinnvolle Interaktion
eines Partners mit einem bestimmten Gesch¨aftsprozess. Man kann sich leicht einen Kunden vorstellen, der zwar die Bedienelemente des Getr¨ankeautomaten kennt, diese jedoch
18
2.1 Modelle
R
q0
!K
!T
q1
!e
?G
q2
?BK
q3
q6
!A
!A
!e
q4
?G
q7
?BT
?W
q5
q8
Abbildung 2.2: Partnerautomat f¨
ur das Netz N1 aus Abb. 2.1
in falscher Reihenfolge benutzt. Daher f¨
uhren wir ein Kriterium ein, das zum Ausdruck
bringt, ob die Interaktion eines Partnerautomat mit einem bestimmten Gesch¨aftsprozess
sinnvoll verl¨auft oder nicht.
Definition 2.12 (Komposition)
Sei N = [P, T, F, W, m0 , ΩN ] ein oWFN und R = [Q, CI , CO , δR , q0 , ΩR ] ein Partnerautomat f¨ur N. Dann heißt der Automat N ⊕ R = [QN ⊕R , δN ⊕R , q0 N ⊕R , ΩN ⊕R ] mit
◦ Zust¨anden QN ⊕R (Paare aus einer Markierung von N und einem Zustand von R),
◦ einer Zustand¨uberf¨uhrungsfunktion δN ⊕R ⊆ QN ⊕R × QN ⊕R ,
◦ einem Startzustand q0 N ⊕R = (m0 , q0 ) und
◦ Endzust¨anden ΩN ⊕R = {(mf , qf ) | mf ∈ ΩN und qf ∈ ΩR }
¨
die Komposition aus N und R. Die Zust¨ande und Uberf¨
uhrungsfunktion sind induktiv
definiert: q0 N ⊕R ∈ QN ⊕R . F¨ur (m, q) ∈ QN ⊕R existiert – in den folgenden F¨allen – auch
(m , q ) ∈ QN ⊕R und (m, q) → (m , q ) ∈ δN ⊕R :
t
◦ q = q und es gibt eine Transition t ∈ T mit m −
→m,
◦ es gibt einen Eingabeplatz pI ∈ PI mit (q, pI , q ) ∈ δR und m = m + [pI ],
◦ es gibt einen Ausgabeplatz pO ∈ PO mit (q, pO , q ) ∈ δR und m = m − [pO ],
◦ (q, τ, q ) ∈ δR und m = m.
19
2 Grundlagen
Wir nennen Zust¨ande q ∈ QN ⊕R erreichbar, wenn es eine Zustandsfolge q0 , q1 , . . . , qn
ur je zwei aufeinanderfolgende Zust¨ande eine
gibt mit q0 = q0 N ⊕R und qn = q, wobei f¨
Kante in der Komposition existiert, (qi , qi+1 ) ∈ δN ⊕R .
Definition 2.13 (Deadlockfrei)
Die Komposition N ⊕ R aus dem oWFN N = [P, T, F, W, m0, ΩN ] und dem Serviceautomaten R = [Q, CI , CO , δ, q0 , ΩR ] heißt deadlockfrei, falls jeder erreichbare Zustand der
Komposition, der kein Endzustand ist, mindestens einen Nachfolger besitzt.
Definition 2.14 (Beschr¨
ankte Kommunikation)
Ein oWFN und ein Serviceautomat kommunizieren k-beschr¨ankt, falls in der Komposition auf keinem Nachrichtenkanal jemals mehr als k Nachrichten liegen. Ist der konkrete Wert dieser Schranke uninteressant, so spricht man auch einfach von beschr¨ankter
Kommunikation.
Definition 2.15 (Strategie)
Ein Partnerautomat R heißt k-Strategie f¨
ur ein oWFN N, wenn die Komposition N ⊕ R
deadlockfrei ist sowie k-beschr¨ankt kommuniziert. Die Menge aller k-Strategien f¨ur N
sei Strat k (N). Ihre Vereinigung Strat(N) :=
Strat k (N) enth¨alt dann alle Strategien
k∈N
f¨ur N.
Man sieht leicht, dass die Komposition aus Abbildung 2.3 deadlockfrei ist. Die beiden
Partner N1 und R kommunizieren zudem 1-beschr¨ankt. Somit ist R eine 1-Strategie f¨
ur
das Netz N1 .
[p0 ], q0
[p0 , K, e], q2
[p1 , e], q2
[p2 ], q2
[p0 , K], q1
[p1 ], q1
[p0 , K, A], q4
[p1 , A], q4
[p0 , T, A], q4
[p5 , A], q4
[p1 , G], q2
[p0 , T ], q1
[p5 ], q6
[p5 , G], q7
[p0 , T, e], q7
[p5 , e], q7
[p4 ], q7
[p3 , BK ], q2
[p3 , W ], q4
[p6 , W ], q4
[p6 , BT ], q7
[p3 ], q8
[p3 ], q5
[p6 ], q5
[p6 ], q3
Abbildung 2.3: Komposition von N1 aus Abb. 2.1 und R aus Abb. 2.2
20
2.2 Bedienungsanleitung
In dieser Arbeit werden nur Netze und Serviceautomaten betrachtet, die miteinander
beschr¨ankt kommunizieren.
2.2 Bedienungsanleitung
Eine kompakte Darstellung aller Strategien zu einem gegebenen Netz N bietet die sogenannte Bedienungsanleitung f¨ur N. In [MS05] wurde dieses Konzept erstmals eingef¨
uhrt
und in [LMW07] erweitert. In [SMB08] wurde zus¨atzlich eine -Relation f¨
ur Bedienungsanleitungen eingef¨
uhrt. Die nachfolgenden Definitionen sind angelehnt an [SMB08].
Ein Automat heißt deterministisch, wenn es keine τ -Transitionen gibt und f¨
ur jeden
Zustand und jedes Label h¨ochstens eine ausgehende Kante mit diesem Label existiert.
Definition 2.16 (Annotierter Automat)
Ein annotierter Automat Rφ = [Q, CI , CO , δ, q0 , Ω, φ] besteht aus einem deterministischen Automaten R = [Q, CI , CO , δ, q0 , ΩR ] und einer Annotationsfunktion φ : Q → BF .
Dabei ist BF die Menge der booleschen Funktionen u
¨ber CI ∪ CO ∪ {τ, final}.
Definition 2.17 (Assignment)
Ein Assignment eines Serviceautomaten R weist wie folgt jedem Zustand q von R eine
boolesche Belegung βR (q) mit den Werten true/false f¨ur die Kantenbeschriftungen der
von q ausgehenden Kanten zu:


true,
βR (q)(x) := true,


false,
x = final und ∃q : (q, x, q ) ∈ δ
x = final und q ∈ Ω
sonst
Definition 2.18 (Simulationsrelation)
Seien S = [QS , CI , CO , δS , q0S , ΩS ] und R = [QR , CI , CO , δR , q0R , ΩR ] zwei Serviceautomaten. Eine Simulationsrelation zwischen S und R ist wie folgt induktiv definiert:
◦ (q0S , q0R ) ∈ .
◦ Wenn (qS , qR ) ∈ und x ∈ CI ∪ CO sowie (qS , x, qS ) ∈ δS , dann ist (qR , x, qR ) ∈ δR
und (qS , qR ) ∈ .
◦ Wenn (qS , qR ) ∈
und (qS , τ, qS ) ∈ δS , dann ist (qS , qR ) ∈ .
21
2 Grundlagen
Die Beziehung von einem Serviceautomaten zu einem annotierten Automaten wird u
¨ ber
ein Matching hergestellt.
Definition 2.19 (Matching)
Sei S = [QS , CI , CO , δS , q0S , ΩS ] ein Serviceautomat, Rφ = [QR , CI , CO , δR , q0R , ΩR , φ]
ein annotierter Automat und eine Simulationsrelation zwischen S und R. Dann matcht
S mit Rφ , falls f¨ur alle (qS , qR ) ∈ gilt: βS (qS ) |= φ(qR ). Eine Belegung β erf¨ullt dabei
die Annotation φ (kurz β |= φ), wenn die durch φ gegebene Formel mit der Belegung β
eine wahre Aussage darstellt.
Match(Rφ ) ist die Menge aller Automaten, die mit Rφ matchen.
Definition 2.20 (Bedienungsanleitung)
Sei N ein oWFN und OG = Rφ ein annotierter Automat. OG heißt genau dann
k-Bedienungsanleitung (engl. Operating Guideline) zu N, wenn Match(OG) = Strat k (N).
Wir schreiben in dem Fall auch OG = OGN .
Bedienungsanleitungen bieten die M¨oglichkeit, alle Strategien eines Netzes kompakt darzustellen. Die Berechnung einer solchen Bedienungsanleitung ist in [LMW07] beschrieben. Zur Anschauung zeigt die Abbildung 2.4 eine 1-Bedienungsanleitung f¨
ur das Netz
N1 aus Abbildung 2.1.
OGN1
q0 :
!K∨!T ∨!e∨!A
!e
q2 :
?G∧?BK
?BK
q3 :
?G
!K∨!T
!T
q10 :
!e∨!A
!A
!K
!T
q4 :
?W
q5 :
q6 :
!K∨!T
!A
!e∨!A
!e
!T
?G
q7 :
?G∧?BT
?BT
?W
final
q9 :
!K
!A
!K
q1 :
!e
final
q8 :
final
Abbildung 2.4: Bedienungsanleitung f¨
ur das Netz N1 aus Abb. 2.1
22
2.2 Bedienungsanleitung
Wie eingangs gefordert, wollen wir Laufzeitersetzungen auch f¨
ur Teilmengen aller Kunden angeben k¨onnen. Dies bedeutet, wir ben¨otigen eine M¨oglichkeit, Mengen von Strategien, die als annotierte Automaten gegeben sind, zueinander in Beziehung zu setzen.
Definition 2.21 ( -Relation fu
¨r annotierte Automaten)
ψ
Seien S = [QS , CI , CO , δS , q0S , ΩS , ψ] und Rφ = [QR , CI , CO , δR , q0R , ΩR , φ] zwei annotierte Automaten. Sei eine Simulationsrelation zwischen S und R. Dann gelte die
Beziehung S ψ Rφ , falls f¨ur alle (qS , qR ) ∈ gilt: φ(qR ) =⇒ ψ(qS ) ist eine Tautologie.
Man kann sich die -Relation annotierter Automaten vorstellen als eine Art Mengenvergleich f¨
ur die repr¨asentierten Strategien. Werden n¨amlich alle Strategien, die S ψ repr¨asentiert, auch von Rφ repr¨asentiert, so ist S ψ Rφ .
In Abbildung 2.5 sieht man zwei annotierte Automaten OG (a) und OG (b), welche
bestimmte Strategien von Kunden beschreiben. Die Kunden gem¨aß OG w¨ahlen zuerst
ihr Getr¨ank (Tee T oder Kaffee K). Anschließend bezahlen sie (e) solange der Automat weiteres Geld verlangt (G), oder sie brechen den Vorgang ab und lassen sich ihr
eingeworfenes Geld zur¨
uckgeben. Die Kunden gem¨aß OG w¨ahlen hingegen als Getr¨ank
immer nur Kaffee. Ansonsten verhalten sie sich wie die Kunden mit der freien Getr¨ankewahl. Es gilt die Beziehung OG
OG OGN1 . Wie wir sehen werden, gibt es umso
mehr M¨oglichkeiten der Laufzeitersetzung von einem Ausgangsnetz in ein ZN, je weniger
Strategien dabei bewahrt werden sollen.
OG
q0 :
a
!e
?G
?G∧?BK
b
!A
q4 :
final
q5 :
!e
?W
q2 :
?G
?G∧?BK
?W
?BK
final
q3 :
!K∨!T
!T
!K
q1 :
!e∨!A
?BK
q3 :
q0 :
!K
!K
q1 :
q2 :
OG
q6 :
!e∨!A
!A
!A
q4 :
?W
!e∨!A
!e
?G
q7 :
?G∧?BT
?BT
?W
final
q5 :
final
q8 :
final
Abbildung 2.5: Teilmenge von Strategien ( -Relation)
23
2 Grundlagen
24
3 neue Definitionen
3.1 Wissensfunktionen
Zur Berechnung der Laufzeitersetzung f¨
uhren wir zwei Hilfsfunktionen, die Erreichbarkeitsfunktion und die Fortf¨
uhrbarkeitsfunktion, ein. Diese enthalten Informationen u
¨ ber
erreichbare bzw. fortf¨
uhrbare Markierungen. Betrachten wir einen Partnerautomaten
R, so wollen wir wissen, welche Markierungen eines Netzes N bei der Interaktion mit R
erreicht werden k¨onnen und von welchen Markierungen von N die Interaktion problemlos
fortgesetzt werden kann.
3.1.1 Erreichbarkeitsfunktion
Die Erreichbarkeitsfunktion ist angelehnt an das Knowledge, welches in [LMW07] bei der
Berechnung einer Bedienungsanleitung verwendet wird. Wir modifizieren die Definition
dahingehend, dass nicht zwei Serviceautomaten miteinander kommunizieren sondern ein
Serviceautomat mit einem offenen Workflownetz.
Definition 3.1 (Erreichbarkeitsfunktion)
Seien N = [P, T, F, W, m0 , ΩN ] ein oWFN, R = [Q, CI , CO , δ, q0 , ΩR ] ein Partnerautomat f¨ur N und q ein Zustand von R. Sei weiterhin QN ⊕R die Menge der erreichbaren
Zust¨ande der Komposition N ⊕R. Dann ist die Erreichbarkeitsfunktion K1 definiert ¨uber
den Zust¨anden des Automaten als K1 (q) := {m | (m, q) ∈ QN ⊕R }.
Die Erreichbarkeitsfunktion gibt f¨
ur jeden Zustand q des Serviceautomaten an, in welchen Markierungen sich das oWFN befinden kann, wenn bei korrekter Kommunikation
der beteiligten Partner der Automat in diesen Zustand gelangt ist. Die Bestimmung der
Erreichbarkeitsfunktion ist trivial, auch f¨
ur nichtdeterministische Automaten: Man kann
die Informationen direkt aus der Komposition des Netzes mit dem Serviceautomaten ablesen. Eine effiziente Implementation ist in dem Software-Tool Fiona gegeben.
25
3 neue Definitionen
Im folgenden betrachten wir den Algorithmus Erreichbarkeit(N1 ,R) als gegeben.
Dieser erh¨alt als Eingabe ein ofWN N1 sowie einen Serviceautomaten R und liefert als
R¨
uckgabe die Erreichbarkeitsfunktion.
Ein Beispiel f¨
ur eine Erreichbarkeitsfunktion zeigt Abbildung 3.1. Der beteiligte Auto¨
mat R ist hier und den folgenden Beispielen jener aus Abbildung 2.5(b). Der Ubersicht
halber schreiben wir die Funktionswerte in Tabellenform an die Zust¨ande des Automaten. Man u
¨berzeugt sich leicht von der Korrektheit im Vergleich mit der Komposition
aus Abbildung 2.3.
N1
R
p0
K
T
q0
!K
K1
[p0 , K]
[p1 ]
!T
q1
p1
p2
p4
p5
G
!e
W
e
q2
BK
A
?G
K1
[p0 , K, e]
[p1 , e]
[p2 ]
[p1 , G]
[p3 , BK ]
?BK
q6
!A
!A
q4
p6
q3
K1
[p0 , K, A]
[p0 , T, A]
[p1 , A]
[p5 , A]
[p3 , W ]
[p6 , W ]
K1
[p3 ]
q5
!e
?G
q7
K1
[p0 , T, e]
[p5 , e]
[p4 ]
[p5 , G]
[p6 , BT ]
?BT
?W
BT
p3
K1
[p0 , T ]
[p5 ]
K1
[p0 ]
K1
[p3 ]
[p6 ]
q8
K1
[p6 ]
Endmarkierungen sind [p3 ] und [p6 ]
Abbildung 3.1: oWFN mit Erreichbarkeitsfunktion
3.1.2 Fortf¨
uhrbarkeitsfunktion
Die Fortf¨
uhrbarkeitsfunktion stellt die Umkehrung der Erreichbarkeitsfunktion dar. Dabei werden nicht erreichbare sondern fortf¨uhrbare Markierungen betrachtet. Uns interessiert f¨
ur jeden Zustand des Partnerautomaten, in welchen Markierungen sich das Workflownetz befinden kann, damit die beiden ab diesem Zustand deadlockfrei interagieren.
Definition 3.2 (fortfu
¨hrbar in q)
Seien N = [P, T, F, W, m0 , ΩN ] ein oWFN und R = [Q, CI , CO , δ, q0 , ΩR ] ein Partnerautomat f¨ur N. Eine Markierung m von N heißt fortf¨
uhrbar im Zustand q ∈ Q, wenn
die Komposition N ⊕ R mit Startzustand (m, q) deadlockfrei ist und die beiden Partner
beschr¨ankt kommunizieren.
26
3.1 Wissensfunktionen
Definition 3.3 (Fortfu
¨hrbarkeitsfunktion)
Seien N = [P, T, F, W, m0 , ΩN ] ein oWFN, R = [Q, CI , CO , δ, q0 , ΩR ] ein Partnerautomat
f¨ur N und q ein Zustand von R. Dann ist die Fortf¨uhrbarkeitsfunktion K2 definiert ¨uber
den Zust¨anden des Automaten als K2 (q) := {m | m ist fortf¨uhrbar in q}.
F¨
ur die Berechnung der Fortf¨
uhrbarkeitsfunktion nutzen wir folgenden Ansatz: Wir lassen sowohl den Automaten R als auch das Netz N ab den Endzust¨anden r¨
uckw¨arts laufen und bestimmen dabei die r¨uckw¨arts erreichbaren Markierungen, analog zur vorher
betrachteten Erreichbarkeitsfunktion. Daf¨
ur ben¨otigen wir Umkehrungen von Serviceautomaten und offenen Workflownetzen.
Definition 3.4 (Umkehrung)
Bei der Umkehrung reverse(N) eines oWFN N werden die B¨ogen umgedreht und Einund Ausgabekan¨ale vertauscht. Endmarkierung ist die alte Startmarkierung, w¨ahrend
ein neu hinzugef¨ugter Platz v0 anfangsmarkiert ist und Transitionen zu allen bisherigen
Endmarkierungen erh¨alt.
Bei der Umkehrung reverse(R) eines Automaten R werden alle Kanten umgedreht und
die Ein- und Ausgabekan¨ale vertauscht. Endzustand ist der alte Startzustand, w¨ahrend
der neu hinzugef¨ugte Startzustand q0 τ -Kanten zu allen bisherigen Endzust¨anden erh¨alt.
Es folgt der Algorithmus Fortfuehrbarkeit(N2 ,R). Als Eingabe erh¨alt der Algorithmus ein oWFN sowie einen Serviceautomaten und berechnet die Fortf¨
uhrbarkeitsfunktion. Der Berechnung liegt folgende Idee zugrunde: Zun¨achst werden die r¨
uckw¨arts
erreichbaren Markierungen bestimmt und anschließend diejenigen wieder gel¨oscht, die
zu einem Deadlock in der Komposition f¨
uhren.
Fortfuehrbarkeit(N2 ,R)
(1)
K2 := Erreichbarkeit((reverse(N2 ), reverse(R)))
(2)
do
(3)
foreach q ∈ Q

(4)
while ∃m ∈ K2 (q) mit
m + [x], x ∈ CI

(4a)
∃q : (q, x, q ) ∈ δ mit K2 (q )
m − [x], x ∈ CO


m,
x=τ
(4b)
oder RN2 (m) ⊆ K2 (q) do
(5)
K2 (q) := K2 (q) \ {m}
(6)
while K2 ¨andert sich
(7)
return K2
Algorithmus 3.2: Berechnung der Fortf¨
uhrbarkeitsfunktion
27
3 neue Definitionen
Wir verdeutlichen die Arbeitsweise des Algorithmus anhand des Beispiels von Abbildung 3.4. Die Umkehrungen des gegebenen Netzes N2 und des Automaten R sind
in Abbildung 3.3 dargestellt. Desweiteren l¨asst sich an dem umgekehrten Automaten
die Erreichbarkeitsfunktion ablesen. Anhand der Zwischenergebnisse des Algorithmus
erl¨autern wir die Berechnung von K2 (q1 ).
reverse(N2)
reverse(R)
K1
[v1 , v3 ]
[v3 , v5 ]
[v0 , K]
[v0 , T ]
v0
q0
?K
K1
[v0 ]
q1
K
K1
[v1 v3 ]
[v3 , v5 ]
[v0 , K]
[v0 , T ]
?T
q6
v3
T
v1
v5
G
?e
W
e
q2
v4
BK
A
!BK
BT
v2
?A
!G
K1
[v, BK ]
[v2 , BK ]
[v6 , BK ]
[v1 , v4 ]
[v1 , v3 , e]
[v0 , K, e]
[v1 , v3 , G]
[v3 , v5 , G]
[v0 , K, G]
[v0 , T, G]
q3
v6
K1
[v]
[v2 ]
[v6 ]
v0
?A
q4
!G
K1
[vW ]
[v2 , W ]
[v6 , W ]
[v1 , v3 , A]
[v3 , v5 , A]
[v0 , K, A]
[v0 , T, A]
q7
!BT
!W
q5
?e
K1
[v]
[v2 ]
[v6 ]
τ
q8
τ
τ
q0
K1
[vBT ]
[v2 , BT ]
[v6 , BT ]
[v4 , v5 ]
[v3 , v5 , e]
[v0 , T, e]
[v1 , v3 , G]
[v3 , v5 , G]
[v0 , K, G]
[v0 , T, G]
K1
[v]
[v2 ]
[v6 ]
K1
[v]
[v2 ]
[v6 ]
Startmarkierung ist [v0 ], Endmarkierung ist [v0 ]
Abbildung 3.3: umgekehrtes Netz und umgekehrter Automat
Gem¨aß Zeile 1 des Algorithmus enth¨alt K2 (q1 ) zun¨achst {[v1 , v3 ], [v3 , v5 ], [v0 , K], [v0 , T ]}
(vgl. Abb. 3.3). In den Zeilen 2 ff. werden diejenigen Markierungen gel¨oscht, die in einem
Zustand von R nicht fortf¨
uhrbar sind. Aus K2 (q1 ) wird [v0 , T ] durch die Bedingung
in Zeile 4a gel¨oscht. Schließlich enth¨alt K2 (q2 ) nicht die Markierung [v0 eT ] und ist
somit nicht fortf¨
uhrbar. Die Markierung [v3 v5 ] wird aus dem gleichen Grund aus K2 (q1 )
entfernt. Das Ergebnis des Algorithmus ist in Abbildung 3.4 zu sehen.
Ein weiteres Beispiel verdeutlicht die Notwendigkeit der Bedingung in Zeile 4b. In Abbildung 3.5 sieht man ein Workflownetz, f¨
ur das der Automat R keine Strategie ist. Das
Netz besitzt in der Tat u
¨berhaupt keine Strategien. Der Zustand q1 des Automaten wird
zun¨achst mit den Markierungen [v0 ] und [v1 ] versehen (Zeile 1 des Algorithmus). Allerdings kann von der Markierung [v0 ] im Netz die Transition t schalten zu [v4 ], womit sich
das Netz in einem Deadlock befindet. Somit wird in Zeile 4b diese Markierung wieder
entfernt. Das Ergebnis der Berechnung ist in Abbildung 3.5 gegeben.
28
3.1 Wissensfunktionen
N2
R
v0
K
q0
!K
K2
[v0 , K]
[v1 , v3 ]
!T
K2
[v0 , T ]
[v3 , v5 ]
K2
[v0 ]
q1
q6
v3
T
v1
v5
G
!e
W
e
v4
q2
BK
A
!A
?G
K2
[v2 , BK ]
[v6 , BK ]
[v1 , v4 ]
[v1 , v3 , e]
[v0 , e, K]
[v1 , v3 , G]
[v0 , K, G]
?BK
BT
v2
v6
q3
!A
q4
!e
K2
[v2 , W ]
[v6 , W ]
[v1 , v3 , A]
[v3 , v5 , A]
[v0 , K, A]
[v0 , T, A]
q7
q5
K2
[v2 , BT ]
[v6 , BT ]
[v4 , v5 ]
[v3 , v5 , e]
[v0 , e, T ]
[v3 , v5 , G]
[v0 , T, G]
?BT
?W
K2
[v2 ]
[v6 ]
?G
K2
[v2 ]
[v6 ]
q8
K2
[v2 ]
[v6 ]
Endmarkierungen sind [v2 ] und [v6 ]
Abbildung 3.4: oWFN mit Fortf¨
uhrbarkeitsfunktion
R
v0
q0
!K
t
K
!T
K2
−
K2
[v1 ]
K2
−
q1
v4
q6
v1
T
G
e
W
!e
q2
BK
A
?G
K2
[v2 BK ]
[v3 , BK ]
[v1 , e]
?BK
BT
v2
v3
q3
!A
!A
q4
K2
[v2 W ]
[v3 , W ]
[v1 , A]
q5
?G
q7
K2
[v2 BT ]
[v3 , BT ]
?BT
?W
K2
[v2 ]
[v3 ]
!e
K2
[v2 ]
[v3 ]
q8
K2
[v2 ]
[v3 ]
Endmarkierungen sind [v2 ] und [v3 ]
Abbildung 3.5: Fortf¨
uhrbarkeitsfunktion f¨
ur nicht bedienbares oWFN
29
3 neue Definitionen
Trotz der eingangs geforderten k-Beschr¨anktheit der beteiligten Workflownetze kann es
passieren, dass das umgekehrte Netz unbeschr¨ankt ist. Abbildung 3.6 zeigt ein solches
Beispiel. Bei der Komposition des umgekehrten Netzes mit dem umgekehrten Automaten
ist der Platz v4 wegen der Transition t unbeschr¨ankt.
R
v0
K
v1
T
G
!e
W
e
q2
BK
A
?G
K2
∗
[v2 , v4
, BK ]
∗
[v3 , v4
, BK ]
∗ , e]
[v1 , v4
∗
[v0 , v4
, e, K]
?BK
BT
v2
!T
K2
−
K2
−
q1
v4
t
q0
!K
K2
∗
[v1 , v4
]
∗
[v0 , v4
, K]
v3
q3
q6
!A
!A
q4
K2
∗, W ]
[v2 , v4
∗
[v3 , v4
, W]
∗
[v1 , v4
, A]
∗
[v0 , v4
, A, K]
q5
?G
q7
K2
∗, B ]
[v2 , v4
T
∗
[v3 , v4
, BT ]
?BT
?W
K2
∗
[v2 , v4
]
∗
[v3 , v4
]
!e
K2
∗
[v2 , v4
]
∗
[v3 , v4
]
q8
K2
∗
[v2 , v4
]
∗
[v3 , v4
]
Endmarkierungen sind [v2 ], [v3 ]
ur [x], [x, v4 ], [x, v4 , v4 ], . . .
[x, v4∗ ] steht hier stellvertretend f¨
Abbildung 3.6: oWFN mit Fortf¨
uhrbarkeitsfunktion bei unbeschr¨ankter Umkehrung
In diesem Fall erzeugen wir die Komposition aus umgekehrtem Netz mit umgekehrtem
Automaten nicht vollst¨andig, sondern beschr¨anken uns auf solche Zust¨ande, bei denen
die Pl¨atze mit h¨ochstens k Marken belegt sind.
Mit dem folgenden Lemma beweisen wir die Korrektheit des vorgestellten Algorithmus
und schaffen damit die Grundlage f¨
ur den folgenden Abschnitt Laufzeitersetzung.
Lemma 3.5 Der Algorithmus Fortfuehrbarkeit(N2 , R) berechnet die Fortf¨uhrbarkeitsfunktion K2 f¨ur das oWFN N2 und den Serviceautomaten R korrekt.
Beweis:
Offensichtlich umfassen die r¨
uckw¨arts erreichbaren Markierungen (Zeile 1 des Algorithmus) mindestens alle deadlockfreien Markierungen.
Wir f¨
uhren nun die Annahme zum Widerspruch, f¨
ur einen Zustand q entspr¨ache die vom
Algorithmus berechnete Menge K2 (q) nicht der Fortf¨
uhrbarkeitsfunktion. Dann g¨abe es
eine Markierung m ∈ K2 (q), die nicht fortf¨
uhrbar in q ist. Mindestens einer der folgenden
drei Punkte tr¨afe dann zu:
30
3.2 Laufzeitersetzung
(i) Der Zustand (q, m) in der Komposition R ⊕ N2 hat keinen Nachfolger und ist nicht
Endzustand.
(ii) R kann in einen Zustand q wechseln, aber die entsprechend modifizierte Markierung des Netzes ist nicht fortf¨
uhrbar in q .
(iii) N2 kann schalten in eine Markierung m , aber m ist nicht fortf¨
uhrbar in q.
Punkt (i) ist unm¨oglich, da die Komposition als umgekehrte Komposition von den Endzust¨anden aus erstellt wurde und es somit Nachfolger von (q, m) geben muss. Punkt (ii)
¨
wird durch die Uberpr¨
ufung in Zeile 4a des Algorithmus ausgeschlossen. Zeile 4b garantiert, dass Punkt (iii) nicht auftritt.
Die in den Punkten (i)–(iii) beschriebenen Zust¨ande h¨atten in der Komposition stets
einen Deadlock zur Folge. Umgekehrt w¨
urde, wenn m in q nicht fortf¨
uhrbar w¨are, einer der drei Punkte auf (q, m) zutreffen. Daher werden durch den Algorithmus genau
alle nicht fortf¨
uhrbaren Markierungen von den r¨
uckw¨arts erreichbaren Markierungen
¨
entfernt. Ubrig bleiben genau die fortf¨
uhrbaren Markierungen.
3.2 Laufzeitersetzung
Im Folgenden seien als zugrundeliegende Netze stets zwei offene Workflownetze N1 =
[P1 ∪ PI ∪ PO , T1 , F1 , W1 , m01 , Ω1 ] und N2 = [P2 ∪ PI ∪ PO , T2 , F2 , W2 , m02 , Ω2 ] mit demselben Interface gegeben. Die Idee der Laufzeitersetzung ist, mithife zus¨atzlicher Transitionen Marken vom Ausgangs- in das Zielnetz zu verschieben. Die Interaktion beginnt
dann mit der Startmarkierung von N1 und endet bei einer Endmarkierung von N2 .
Definition 3.6 (Transitionsmenge zweier Netze)
Als Transitionsmenge von N1 nach N2 bezeichnen wir ein Tupel T = (TT , FT , WT ) aus
Transitionen, B¨ogen und Bogenvielfachheiten, wenn f¨ur alle t ∈ TT gilt: •t ∈ bags(P1 )
und t• ∈ bags(P2 ∪ PI ).
Die Transitionen in einer Transitionsmenge enthalten im Vorbereich nur innere Pl¨atze
des Ausgangsnetzes. Im Nachbereich sind innere Pl¨atze des Zielnetzes oder auch Eingabepl¨atze erlaubt. Es liegt nahe, die beteiligten Netze mit Hilfer einer solchen Transitionsmenge zu einem gr¨oßeren offenen Workflownetz zu verbinden.
31
3 neue Definitionen
Definition 3.7 (verbundenes Netz)
Sei T = (TT , FT , WT ) eine Transitionsmenge von N1 nach N2 . Das oWFN
N1 ⊕ T ⊕ N2 := (P1 ∪ P2 ∪ PI ∪ PO , T1 ∪ TT ∪ T2 , F1 ∪ FT ∪ F2 , W1 ∪ WT ∪ W2 , m01 , Ω2 )
heißt das verbundene Netz aus N1 , N2 und T .
N1 heißt in diesem Zusammenhang Ausgangsnetz, N2 heißt Zielnetz.
Das Interface des verbundenen Netzes ist hier die Verschmelzung der (identischen) Interfaces beider Workflownetze N1 und N2 . Dadurch k¨onnen die Transitionen der beiden
urspr¨
unglichen Netze gemeinsam die Ein- und Ausgabepl¨atze verwenden. Wie wir sehen
werden, ist dieses Verhalten bei der Laufzeitersetzung explizit erw¨
unscht.
Man beachte, dass die Anfangsmarkierung des verbundenen Netztes genau die Anfangsmarkierung des Ausgangsnetzes ist, w¨ahrend die Endmarkierungen des verbundenen
Netzes denen des Zielnetzes entsprechen. Die Marken auf den Pl¨atzen sollen dabei zur
Laufzeit von N1 nach N2 verschoben werden.
Definition 3.8 (Laufzeitersetzung)
Gegeben sei eine Bedienungsanleitung OG mit OG OGN1 . Dann heißt eine Transitionsmenge T von N1 nach N2 Laufzeitersetzung gem¨aß OG, falls gilt:
Jeder Serviceautomat R ∈ Match(OG) ist eine Strategie f¨ur N1 ⊕ T ⊕ N2 ,
also Match(OG) ⊆ Strat(N1 ⊕ T ⊕ N2 ).
Die Transitionen t ∈ TT nennen wir Laufzeitersetzungstransitionen und schreiben kurz
t•. Zur weiteren Vereinfachung der Schreibweise bezeichne im folgenden eine
•t
Laufzeitersetzungstransition t nicht nur eine Transition des verbundenen Workflownetzes
sondern zugleich die mit t verbundenen B¨ogen und Bogenvielfachheiten. Die Aussage
t ∈ T bedeutet dann, dass die Transition t zusammen mit den entsprechenden B¨ogen in
der Laufzeitersetzung enthalten ist.
Abbildung 3.7 zeigt eine Laufzeitersetzung f¨
ur die Netze zweier Getr¨ankeautomaten. Die
¨
beiden Netze teilen zwar die Interfacepl¨atze, zur besseren Ubersichtlichkeit
sind diese
jedoch doppelt – einmal f¨
ur jedes Netz – dargestellt. Die gestrichelten Rahmen markieren
optisch die urspr¨
unglichen Workflownetze. Als Konvention liegen Eingabepl¨atze stets
links auf dem Rahmen, Ausgabepl¨atze rechts.
In dem konkreten Beispiel besitzen die beiden Netze die gleiche Bedienungsanleitung.
Daher ist auch die Laufzeitersetzungstransition [p0 ]
[v0 ] enthalten – die Netze
k¨onnten also gleich zu Beginn der Interaktion ersetzt werden.
32
3.2 Laufzeitersetzung
T
N1
N2
p0
v0
K
K
v3
T
p1
p2
p4
G
T
W
e
p5
e
v1
v5
G
W
v4
BK
A
BK
A
BT
p3
p6
BT
v2
v6
Startmarkierung des verbundenen Netzes ist [p0 ], Endmarkierungen sind [v2 ] und [v6 ]
Abbildung 3.7: Laufzeitersetzung offener Workflownetze gem¨aß OG aus Abb. 2.5
In unserem Beispiel sind auch Laufzeitersetzungstransitionen enthalten, die eine Endmarkierung des Ausgangsnetzes in eine Endmarkierung des Zielnetzes u
uhrt. Solche
¨berf¨
Transitionen k¨onnen immer als Laufzeitersetzungstransitionen verwendet werden.
Definition 3.9 (triviale Laufzeitersetzung)
Die Transitionsmenge {mf
mf | mf ∈ Ω1 und mf ∈ Ω2 }, welche ausschließlich
¨
Uberf¨
uhrungen von Endmarkierungen enth¨alt, heißt triviale Laufzeitersetzung.
Die Bezeichnung der trivialen Laufzeitersetzung als Laufzeitersetzung impliziert, dass
die Bedingungen nach Definition 3.8 erf¨
ullt sind. Tats¨achlich k¨onnen wir dies an dieser
Stelle noch nicht beweisen. Erst im Abschnitt 4.2 gehen wir erneut auf die triviale Laufzeitersetzung ein und rechtfertigen somit im Nachhinein die Namensgebung.
3.2.1 Eingabepl¨
atze neu belegen
Wie aus der Definition der Transitionsmenge ersichtlich, d¨
urfen die Laufzeitersetzungstransitionen auch Marken auf die Eingabepl¨atze PI legen. Im u
¨bertragenen Sinne hieße
solch ein Verhalten, dass die Laufzeitersetzung dem Zielservice gegen¨
uber bestimmte
Nachrichten des Partners simuliert. Der Zielservice w¨
urde die Nachrichten intern verarbeiten, als w¨aren sie vom Partner (bzw. Kunden) pers¨onlich u
¨bermittelt worden.
33
3 neue Definitionen
Abbildung 3.8 verdeutlicht, was passieren kann, wenn man Eingabepl¨atze im Nachbereich von Laufzeitersetzungstransitionen verbietet. Man sieht leicht, dass es deutlich weniger Laufzeitersetzungstransitionen gibt, wenn der Eingabeplatz e nicht belegt werden
darf.
T
N1
N2
p0
e
v0
p1
p2
p4
p3
v1
v2
v3
e
G
pf
G
vf
Endmarkierungen sind [pf ] bzw. [vf ]
Abbildung 3.8: Laufzeitersetzung, die keinen Eingabeplatz belegt
Bei diesem Netz k¨onnen die Markierungen [p2 , p4 ] und [p3 , p4 ] nur u
uhrt werden,
¨berf¨
¨
indem auf den Platz e eine Marke gelegt wird. Ansonsten ist keine Uberf¨
uhrung dieser
beiden Markierungen m¨oglich. Befindet sich das Netz N1 in einer solchen Markierung,
¨
dann k¨onnte die n¨achstm¨ogliche Uberf¨
uhrung der Marken in das Zielnetz erst in der
Endmarkierung stattfinden.
34
4 Instantane Laufzeitersetzungen
Bei der Laufzeitersetzung von Serviceautomaten [Lis07] werden Zust¨ande des Ursprungsautomaten u
uhrt in Zust¨ande des Zielautomaten. Ein Serviceautomat befindet sich
¨berf¨
stets in genau einem Zustand. Somit ist der Ausgangsautomat nach dem Schalten der
¨
Laufzeitersetzungstransition inaktiv. Die Uberf¨
uhrung wurde durch sogenannte τ -Transitionen repr¨asentiert, also solche Transitionen, die keine Nachricht vom Nachrichtenkanal nehmen und keine neue hineingeben.
Analog zu dem Vorgehen bei Serviceautomaten untersuchen wir in diesem Kapitel zun¨achst die sogenannten instantanen Laufzeitersetzungen zweier offener Workflownetze.
Bei dieser Art von Laufzeitersetzung wird die Eigenschaft u
¨bernommen, das Ursprungsnetz durch eine einzige Laufzeitersetzungstransition komplett zu leeren. Das bedeutet,
dass alle Marken des Ausgangsnetzes gleichzeitig konsumiert und neue Marken im Ziel¨
netz porduziert werden. Damit u
uhrung
¨ bertragen wir grundlegend die Idee der Uberf¨
von Serviceautomaten auf offene Workflownetze.
Zu Beginn der Interaktion ist das Ausgangsnetz aktiviert, nach dem Schalten der Laufzeitersetzungstransition soll es deaktiviert sein. Umgekehrt soll das Zielnetz solange deaktiviert sein, bis eine der Laufzeitersetzungstransitionen geschaltet hat. Wie wir sp¨ater
sehen werden, ist die Deaktivierung des Ausgangsnetzes wegen der Identit¨at der Interfacepl¨atze nicht offensichtlich und wird erst durch strukturelle Bedingungen an die
beteiligten Netze sichergestellt.
Ein Ziel dieser Arbeit ist, die Laufzeitersetzung speziell f¨
ur eine vorgegebene Menge
von Partnerstrategien zu erzeugen. Diese Strategien seien im folgenden stets durch den
annotierten Automaten OG = Rφ gegeben. Wie schon in der Definition von Laufzeitersetzungen gefordert, handelt es sich dabei um Strategien f¨
ur das Ausgangsnetz N1 ,
d.h. OG OGN1 .
Im Abschnitt 3.1 haben wir bereits die Wissensfunktionen f¨
ur offene Workflownetze kennengelernt. In den folgenden Betrachtungen setzen wir die Erreichbarkeitsfunktion K1 ,
die den Zust¨anden von R die erreichbaren Markierungen des Ausgangsnetzes N1 zuordnet, sowie die Fortf¨
uhrbarkeitsfunktion K2 , f¨
ur die entsprechend fortf¨
uhrbaren Markierungen des Zielnetzes N2 , als gegeben voraus.
35
4 Instantane Laufzeitersetzungen
Definition 4.1 (instantane Laufzeitersetzung)
Sei T = (TT , FT , WT ) eine Laufzeitersetzung von N1 = [PI ∪ P1 ∪ PO , T1 , F1 , m01 , Ω1 ]
nach N2 = [PI ∪ P2 ∪ PO , T2 , F2 , m02 , Ω2 ] gem¨aß OG. T heißt instantan, wenn nach
Schalten einer beliebigen Transition t ∈ T gilt: m(p) = 0, ∀p ∈ P1 .
In diesem Kapitel meinen wir mit T – wenn nicht anders erw¨ahnt – eine Laufzeitersetzung vom Netz N1 nach N2 gem¨aß der Bedienungsanleitung OG = Rφ , wie in der
Definition 4.1 beschrieben. Zur einfachen Formulierung der nachstehenden Aussagen
und Beweise sprechen wir lediglich von einer erreichbaren Markierung m1 bzw. einer
fortf¨uhrbaren Markierung m2 , falls es einen Zustand q ∈ Q gibt, sodass mit m1 ∈ K1 (q)
bzw. m2 ∈ K2 (q).
Instantane Laufzeitersetzungen gibt es in jedem Fall, unabh¨angig davon, welche Workflownetze ersetzt und welche Partnerstrategien der Laufzeitersetzung zugrunde gelegt
werden sollen. Schließlich ist jede triviale Laufzeitersetzung, offensichtlich auch instantan. Interessanter ist nat¨
urlich die Frage, ob es auch nicht-triviale instantane Laufzeitersetzungen gibt.
Ein Beispiel f¨
ur eine nicht-triviale instantane Laufzeitersetzung zeigt Abbildung 4.1.
Dieser Laufzeitersetzung liegt als Strategiemenge OG die Bedienungsanleitung von Abbildung 2.4 zugrunde. Offensichtlich gibt es gem¨aß OG neben den dargestellten noch
weitere Laufzeitersetzungstransitionen – beispielsweise [p3 ]
[v2 ].
T
N1
N2
p0
v0
K
K
v3
T
p1
p2
p4
G
T
W
e
p5
e
v1
v5
G
W
v4
BK
A
BK
A
BT
p3
p6
BT
v2
v6
Endmarkierungen sind [p3 ], [p6 ] bzw. [v2 ], [v6 ]
Abbildung 4.1: instantane Laufzeitersetzung gem¨aß OG von Abb. 2.4
36
4.1 Algorithmus zur Bestimmung instantaner Laufzeitersetzungen
F¨
ur Laufzeitersetzungen von Serviceautomaten wurde das Kriterium der Maximalit¨at
definiert [Lis07]. Wir wollen dieses Kriterium nun ¨ahnlich f¨
ur instantane Laufzeitersetzungen offener Workflownetze formulieren.
Definition 4.2 (vollst¨
andige instantane Laufzeitersetzung)
Eine instantane Laufzeitersetzung T heißt vollst¨andig, falls sie alle instantanen Laufzeitersetzungstransitionen enth¨alt. Als instantane Laufzeitersetzungstransition bezeichnen wir dabei all jene Transitionen, deren Vorbereich eine erreichbare Markierung des
Ausgangsnetzes darstellt und die in einer beliebigen instantanen Laufzeitersetzung enthalten sind.
Gem¨aß dieser Definition ist die vollst¨andige instantane Laufzeitersetzung genau die Vereinigung aller instantanen Laufzeitersetzungen. Man u
¨berzeugt sich leicht davon, dass
diese eindeutig ist. Die in Abbildung 4.1 dargestellte instantane Laufzeitersetzung ist,
wie wir gesehen haben, nicht vollst¨andig. Unser Ziel ist daher, einen Algorithmus anzugeben, der stets die vollst¨andige instantane Laufzeitersetzung berechnet.
4.1 Algorithmus zur Bestimmung instantaner
Laufzeitersetzungen
Die im Abschnitt 3.1 kennengelernten Wissensfunktionen bilden die Grundlage des folgenden Algorithmus zur Bestimmung instantaner Laufzeitersetzungen. Gegeben seien
zwei Workflownetze N1 und N2 , welche keine leeren Transitionen im inneren Netz besitzen, sowie ein annotierter Automat OG = Rφ OGN1 zur Beschreibung aller Partnerstrategien.
Es folgt der Algorithmus InstantaneLE(N1 , N2 , R). Er bestimmt eine Menge instantaner Laufzeitersetzungstransitionen von N1 nach N2 . Der Algorithmus sucht dazu zu
jeder erreichbaren Markierung des Ausgangsnetzes passende fortf¨
uhrbare Markierungen
des Zielnetzes. Sein Vorgehen dabei l¨asst sich wie folgt zusammenfassen: Der Algorithmus bestimmt zuerst die Erreichbarkeitsfunktion f¨
ur das Netz N1 und die Fortf¨
uhrbarkeitsfunktion f¨
ur das Netz N2 . Dann beginnt er, die triviale Laufzeitersetzung nach und
nach zur vollst¨andigen Laufzeitersetzung zu erweitern. F¨
ur alle erreichbaren Markierungen des Ausgangsnetzes werden die potentiell fortf¨
uhrbaren Markierungen des Zielnetzes
untersucht (Zeile 5–6). Dabei fallen bestimmte Paarungen von Ausgangs- und Zielmarkierung, die bei der Laufzeitersetzung zu Deadlocks f¨
uhrten, aus der Betrachtung heraus
(Zeile 7–10). F¨
ur die anderen wird jeweils eine instantane Laufzeitersetzungstransition
erzeugt (Zeile 11–12).
37
4 Instantane Laufzeitersetzungen
InstantaneLE(N1 , N2 ,R)
(1)
K1 := Erreichbarkeit(N1,R)
(2)
K2 := Fortfuehrbarkeit(N2 ,R)
(3)
T := {mf
mf | mf ∈ Ω1 und mf ∈ Ω2 }
(4)
foreach q ∈ Q
(5)
foreach Markierung m1 ∈ K1 (q),
die von keiner erreichbaren Markierung echt u
¨berdeckt wird
I
I
(6)
M := {mN
+
(m
−
m
)
|
2
2
1
O
I
I
m2 ∈ K2 (q), mO
1 = m2 und m1 ≤ m2 }
(7)
foreach q ∈ Q
(8)
foreach m2 ∈ M
(9)
if ∃m mit (mN
/ K2 (q )
1 + m) ∈ K1 (q ) und (m2 + m) ∈
(10)
M := M \ {m2 }
(11)
foreach m2 ∈ M
(12)
T := T ∪ {mN
m2 }
1
(13) return T
Algorithmus 4.2: Berechnung der instantanen Laufzeitersetzung
Im Detail erl¨autern wir das Verhalten des Algorithmus beispielhaft anhand der Wissensfunktionen von Abbildung 4.3. Nach Initialisierung der Transitionsmenge T mit
der trivialen Laufzeitersetzung iteriert der Algorithmus in Zeilen 4 und 5 u
¨ ber alle erreichbaren Markierungen des ersten Netzes. Sagen wir, er w¨ahlt zuerst den Zustand q0 ,
dann findet er die initiale Markierung m1 = [p0 ] (Zeile 5). Als Menge M potentieller
Zielmarkierungen werden aus der Fortf¨
uhrbarkeitsfunktion K2 (q0 ) anschließend diejenigen Markierungen ausgew¨ahlt, die dieselben Ausgabepl¨atze wie m1 und mindestens alle
Eingabepl¨atze dieser Markierung haben (Zeile 6). Diese Bedingung erf¨
ullt hier nur [v0 ].
R
K1
[p0 , K]
[p1 ]
q0
!K
K2
[v0 , K]
[v1 , v3 ]
K1
[p0 ]
!T
K2
[v0 ]
q1
q2
!A
!e
?G
K1
[p0 , K, e]
[p1 , e]
[p2 ]
[p1 , G]
[p3 , BK ]
?BK
q3
K2
[v2 , BK ]
[v6 , BK ]
[v1 , v4 ]
[v1 , v3 , e]
[v0 , e, K]
[v1 , v3 , G]
[v0 , K, G]
q4
K1
[p0 , K, A]
[p0 , T, A]
[p1 , A]
[p5 , A]
[p3 , W ]
[p6 , W ]
K2
[v2 ]
[v6 ]
q5
K2
[v2 , W ]
[v6 , W ]
[v1 , v3 , A]
[v3 , v5 , A]
[v0 , K, A]
[v0 , T, A]
?G
q7
K1
[p0 , T, e]
[p5 , e]
[p4 ]
[p5 , G]
[p6 , BT ]
K2
[v2 , BT ]
[v6 , BT ]
[v4 , v5 ]
[v3 , v5 , e]
[v0 , e, T ]
[v3 , v5 , G]
[v0 , T, G]
?BT
?W
K1
[p3 ]
K2
[v0 , T ]
[v3 , v5 ]
q6
!A
!e
K1
[p0 T ]
[p5 ]
K1
[p3 ]
[p6 ]
K2
[v2 ]
[v6 ]
q8
K1
[p6 ]
K2
[v2 ]
[v6 ]
Abbildung 4.3: Wissensfunktionen K1 und K2 f¨
ur die Netze aus Abb. 4.1
38
4.1 Algorithmus zur Bestimmung instantaner Laufzeitersetzungen
Der Algorithmus u
uft weiter alle Zust¨ande, bei denen mN
¨berpr¨
1 = [p0 ] in K1 enthalten
ist. Dies sind die Zust¨ande q1 , q2 , q4 , q5 und q7 . Zum besseren Verst¨andnis zeigt listet
die Tabelle 4.4 die Wissensfunktionen f¨
ur diese Zust¨ande mit Unterscheidung zwischen
inneren und Interface-Pl¨atzen auf.
Zustand
q1
q2
q4
q6
q7
Markierung in K1 ()
[p0 ] + [K]
[p0 ] + [K, e]
[p0 ] + [K, A]
[p0 ] + [T, A]
[p0 ] + [T ]
[p0 ] + [T, e]
Markierungen in K2 ()
[v0 ] + [K]
[v0 ] + [K, e]
[v0 ] + [K, A]
[v0 ] + [T, A]
[v0 ] + [T ]
[v0 ] + [T, e]
Tabelle 4.4: Ausschnitt der Wissensfunktionen f¨
ur Abb. 4.3
Diejenigen dieser Zust¨ande, bei welchen [p0 ] als erreichbare Markierung des Ausgangsnet¨
zes vorkommt, enthalten als fortf¨
uhrbare Markierung im Zielnetz [v0 ]. Die Uberpr¨
ufung
in Zeile 9 des Algorithmus l¨asst diese Markierung zu, sodass wir die neue instantane
Laufzeitersetzungstransition [p0 ]
[v0 ] erhalten.
Als n¨achster Zustand sei in Zeile 4 q1 ausgew¨ahlt, die n¨achste betrachtete Markierung des Ausgangsnetzes ist dann m1 = [p1 ]. Die potentiellen Zielmarkierungen sind
hierf¨
ur M = {[v0 , K], [v1 , v3 ]}. Weil diese in Zeile 9 nicht verworfen werfen, f¨
ugt der
Algorithmus die zwei instantanen Laufzeitersetzungstransitionen [p1 ]
[v1 , v3 ] und
[p1 ]
[v0 , K] hinzu. Er f¨ahrt so fort, bis alle erreichbaren Markierungen des Ausgangsnetzes u
uft worden sind.
¨ berpr¨
Die vollst¨andige instantane Laufzeitersetzung ist in Tabelle 4.5 dargestellt. Dabei sind
die Transitionen optisch getrennt in solche, die nur innere Pl¨atze des Zielnetzes im Nachbereich enthalten (links), und solche, die zus¨atzlich Eingabepl¨atze belegen (rechts).
[p0 ]
[p1 ]
[p2 ]
[p3 ]
[p3 ]
[p4 ]
[p5 ]
[p6 ]
[p6 ]
[v0 ]
[v1 , v3 ]
[v1 , v4 ]
[v2 ]
[v6 ]
[v4 , v6 ]
[v3 , v5 ]
[v2 ]
[v6 ]
[p1 ]
[p1 ]
[p2 ]
[p2 ]
[p5 ]
[p6 ]
[p6 ]
[v0 , K]
[v1 , v4 , e]
[v1 , v3 , e]
[v0 , K, e]
[v0 , T ]
[v3 , v6 , e]
[v0 , T, e]
Tabelle 4.5: vollst¨andige instantane Laufzeitersetzung
39
4 Instantane Laufzeitersetzungen
¨
Ein weiteres Beispiel soll zeigen, wozu die Uberpr¨
ufung in Zeile 9 des Algorithmus
¨
ben¨otigt wird. Bei den Netzen zuvor wurde keine Transition durch diese Uberpr¨
ufung
verworfen.
¨
4.1.1 Notwendigkeit der Uberpr¨
ufung auf Fortf¨
uhrbarkeit
¨
In Abbildung 4.6 sind zwei Netze gegeben, bei denen ohne die Uberpr¨
ufung in Zeile 9
ein Deadlock in der Komposition aus dem verbundenen Netz und dem Partner entstehen
w¨
urde. Damit w¨are die Transitionsmenge keine Laufzeitersetzung.
Netz 1
T
Netz 2
p0
v0
A
A
C
C
p1
B
R
q0
!A
v1
v2
q1
B
D
K1
[p0 , A]
[p1 ]
vf
Endmarkierungen sind [pf ] bzw. [vf ]
K2
[v0 ]
!C
K2
[v0 , A]
[v1 ]
K1
[p0 , C]
[p1 ]
!B
D
pf
K1
[p0 ]
q3
K2
[v0 , C]
[v2 ]
q2
K1
[p0 , A, B]
[p1 , B]
[pf ]
K2
[v0 , A, B]
[v2 , B]
[vf ]
!D
q4
K1
[p0 , C, D]
[p1 , D]
[pf ]
K2
[v0 , C, D]
[v2 , D]
[vf ]
¨
Abbildung 4.6: Notwendigkeit der Uberpr¨
ufung in Zeile 9
Folgende Konstellation ist in diesem Beispiel gegeben: Die Markierung [p1 ] des Ausgangsnetzes ist in K1 (q1 ) sowie K1 (q3 ) enthalten. Die Markierung [v1 ] des Zielnetzes ist
analog in K2 (q1 ) jedoch nicht in K2 (q3 ) enthalten. Bei diesem Fall w¨
urde die Bedingung
[v1 ] als Laufzeiterin Zeile 9 des Algorithmus zutreffen und die Transition [p1 ]
¨
setzungstransition verwerfen. G¨abe es diese Uberpr¨
ufung nicht, und damit die Transition [p1 ]
[v1 ], so gelangt man nach dem Schalten in die Markierung [v1 ]. Wegen
[p1 ] ∈ K1 (q3 ) kann diese Transition mitunter dann schalten, wenn sich der Partner
gerade im Zustand q3 befindet. Jedoch ist die Markierung [v1 ] nicht fortf¨
uhrbar in q3
([v1 ] ∈
/ K2 (q3 )). Aus diesem Grund werden solche Transitionen bei der Erzeugung der
Laufzeitersetzung verworfen.
Ganz allgemein muss gew¨ahrleistet sein, dass wenn eine Laufzeitersetzungstransition
m1
m2 schaltet, die Markierung m2 in allen Zust¨anden fortf¨
uhrbar ist, bei denen
m1 erreichbar ist. Anderenfalls ergibt sich, wie wir gesehen haben, in der Komposition
aus dem verbunden Netz mit dem Partner ein Deadlock.
40
4.2 Einschr¨ankungen der Netze
Proposition 4.3 Wird f¨ur eine Ausgangsmarkierung m1 die potentielle Zielmarkierung
m2 in Zeile 9 des Algorithmus verworfen, so hat f¨ur ein R ∈ Match(OG) die Komposition
¨
mit dem verbundenen Netz mit der Uberf¨
uhrung m1
m2 einen Deadlock.
4.2 Einschr¨
ankungen der Netze
4.2.1 Leere Transitionen im inneren Netz
Abbildung 4.7 zeigt das oWFN N2 eines Kaffeeautomaten, der nach Einwurf von e einen
Kaffee ausgibt – unabh¨angig von der Wahl des Kunden. Auf den Abbruchwunsch (A)
des Partners reagiert der Automat ebenfalls. Das Netz enth¨alt zwei Transitionen, tK und
tT , die im inneren Netz leer sind.
T
N1
N2
p0
v0
tK
K
K
tT
v1
T
G
T
G
e
W
e
W
A
BK
A
BK
p1
p2
p4
p5
BT
p3
p6
BT
v2
v3
Endmarkierungen sind [p3 ], [p6 ] bzw. [v2 ], [v3 ]
Abbildung 4.7: leere Transitionen im inneren Netz
Intuitiv sollte das Netz N1 durch N2 zur Laufzeit ersetzt werden k¨onnen. Weil die
Interface-Pl¨atze beim verbundenen Netz verschmolzen werden, ergibt sich tats¨achlich
aber bereits bei der trivialen Laufzeitersetzung folgendes Problem: W¨ahlt n¨amlich ein
Partner Tee aus, so wird der Platz T markiert. Die Transition tT des zweiten Netzes ist
anschließend aktiviert und kann diese Marke vom Eingabeplatz wieder entfernen. Damit
ist aber keine Transition mehr aktiviert, weder im Ausgangs- noch im Zielnetz, obwohl
kein Endzustand erreicht wurde. Die Komposition enth¨alt also einen Deadlock.
41
4 Instantane Laufzeitersetzungen
Wir m¨ochten stattdessen, dass das Zielnetz tats¨achlich erst dann aktiviert ist, wenn eine
Laufzeitersetzungstransition geschaltet hat. Ebenso soll das Ausgangsnetz deaktiviert
sein, sobald eine Laufzeitersetzungstransition geschaltet hat. Also schließen wir leere
Transitionen im inneren Netz von vornherein explizit aus.
Durch diese Bedingung ist sichergestellt, dass das Ausgangsnetz nach dem Schalten
einer instantanen Laufzeitersetzungstransition auch tats¨achlich deaktiviert ist. Ebenso
ist aufgrund dieser strukturellen Einschr¨ankung das Zielnetz auch erst dann aktiviert,
wenn eine Laufzeitersetzungstransition geschaltet hat.
Lemma 4.4 Sei N ein oWFN mit beschr¨anktem inneren Netz. Sind alle inneren Pl¨atze
von N leer und gibt es im inneren Netz von N keine leeren Transitionen, dann sind alle
Transitionen in N deaktiviert.
Beweis:
Jede Transition in N besitzt mindestens einen inneren Platz im Vorbereich. W¨are dem
nicht so, dann g¨abe es eine Transition, welche nur Eingabepl¨atze im Vorbereich besitzt.
Diese Transition hat dann mindestens einen inneren Platz im Nachbereich, weil es nach
Voraussetzung keine leeren Transitionen im inneren Netz gibt. Dann w¨are das innere
Netz von N aber nicht beschr¨ankt, Widerspruch zur Annahme. Also besitzt jede Transition einen inneren Platz im Vorbereich, woraus die Aussage folgt.
¨
4.2.2 Uberdeckte
Endmarkierungen
Intuitiv erwarten wir von jeder Laufzeitersetzung, dass zumindest die Endmarkierungen
des ersten Netzes in eine Endmarkierung des zweiten Netzes u
uhrt werden k¨onnen.
¨berf¨
Schließlich sind die Endmarkierungen des zweiten Netzes gleichzeitig die Endmarkierungen des bei der Laufzeitersetzung verbundenen Netzes.
Wir werden nun zeigen, dass Endmarkierungen, die von beliebigen Markierungen echt
u
¨berdeckt werden, problematisch bei der Erzeugung von Laufzeitersetzungen sind. In
Abbildung 4.8 sind dazu zwei Netze dargestellt, f¨
ur die es keine instantane Laufzeitersetzung gibt.
Das erste Netz befindet sich nach Schalten der Transition t1 in der Endmarkierung
[p2 ], w¨ahrend t2 in die Endmarkierung [p1 , p2 ] schaltet. Offenbar u
¨berdeckt die zweite
Endmarkierung echt die Endmarkierung [p2 ]. Das zweite Netz besitzt nur eine Endmarkierung, [v1 ]. Betrachten wir die m¨oglichen Transitionsmengen von N1 nach N2 , so sehen
wir, dass es in der Komposition des verbundenen Netzes mit einem Partner stets zu
einem Deadlock kommt.
42
4.2 Einschr¨ankungen der Netze
T
Netz 1
Netz 2
p0
v0
e
e
t1
t2
t3
G
G
t>
p1
p2
v1
t<
Endmarkierungen sind [p2 ] und [p1 p2 ] bzw. [v1 ]
Abbildung 4.8: u
¨berdeckte Endmarkierung
¨
◦ Lassen wir als Uberf¨
uhrung die Transition t< = [p2 ]
dem Schalten von t2 und t< die Markierung [p1 ] u
¨brig.
[v1 ] zu, so bleibt nach
◦ Nehmen wir stattdessen t< nicht zur Laufzeitersetzung hinzu, daf¨
ur aber die Transition t> = [p1 , p2 ]
[v1 ], so erhalten wir nach Schalten von t1 die Markierung
[p2 ], welche nicht in das zweite Netz u
uhrt wird.
¨ berf¨
◦ Offensichtlich erhalten wir ebenfalls einen Deadlock in der Komposition, wenn gar
keine der genannten Laufzeitersetzungstransitionen verwendet wird.
Bei Workflownetzen kann der Modellierer u
¨berdeckte Endmarkierungen aufl¨osen, indem
er eindeutig macht, welche Transition als letzte geschaltet hat. F¨
ur das oben genannte
usste die TransiBeispiel k¨onnen die Pl¨atze pt1 und pt2 neu angelegt werden. Dann m¨
tion t1 im Nachbereich [p2 , pt1 ] belegen und t2 die Markierung [p1 , p2 , pt2 ]. Diese neuen
Endmarkierungen werden nicht u
¨ berdeckt.
Der Verbot echt u
ur die
¨ berdeckter Endmarkierungen stellt also keine Einschr¨ankung f¨
Ausdrucksm¨achtigkeit der gegebenen Netze dar. Daher gehen wir o.B.d.A. davon aus,
dass im Ausgangsnetz keine Endmarkierung von einer erreichbaren Markierung u
¨berdeckt wird.
¨
4.2.3 Uberdeckte
Markierungen
¨
Uberdeckte
Markierungen, die keine Endmarkierungen sind, f¨
uhren nicht automatisch
zu den zuvor beschriebenen Problemen. Allerdings gibt es auch f¨
ur u
¨berdeckte Markierungen ungewollte Effekte bei der Laufzeitersetzung.
43
4 Instantane Laufzeitersetzungen
Abbildung 4.9 zeigt eine leicht modifizierte Variante des Ausgangsnetzes f¨
ur das Beispiel
der zwei Getr¨ankeautomaten. Der einzige Unterschied gegen¨
uber N1 in N1 ist, dass
anfangs p7 belegt und irgendwann geleert wird.
T
N1
N2
p0
v0
p7
K
K
t
v3
T
p1
p2
p4
G
T
W
e
p5
e
v1
v5
G
W
v4
BK
A
BK
A
BT
p3
p6
BT
v2
v6
Endmarkierungen sind [p3 ], [p6 ] bzw. [v2 ], [v3 ]
Abbildung 4.9: u
¨berdeckte Markierung
Die vollst¨andige instantane Laufzeitersetzung von N1 als Ausgangsnetz zum Zielnetz N2
sieht ¨ahnlich zur Laufzeitersetzung von N1 nach N2 aus (vgl. Tabelle 4.5). Die Vorbereiche aller instantanen Laufzeitersetzungstransitionen enthalten – außer bei der Endmarkierung – zus¨atzlich den Platz p7 . Die Konsequenz f¨
ur das Verhalten des verbundenen
Netzes ist, dass – sobald die Transition t den Platz p7 geleert hat, keine Laufzeiterset¨
zungstransition außer jener zur Uberf¨
uhrung des Endzustandes schalten kann.
Die Existenz instantaner Laufzeitersetzungen ist unabh¨angig davon, ob es u
¨ berdeckte
erreichbare Markierungen im Ausgangsnetz gibt. M¨ochte man das zuvor beschriebene
Verhalten jedoch vermeiden, so sollten die u
¨berdeckten Markierungen analog zum Vorgehen bei den u
¨ berdeckten Endmarkierungen beim Entwurf des offenen Workflownetzes
beseitigt werden.
44
4.3 Korrektheit des Algorithmus InstantaneLE
4.3 Korrektheit des Algorithmus InstantaneLE
In den vorherigen beiden Abschnitten haben wir den Algorithmus 4.2 zur Bestimmung
instantaner Laufzeitersetzungen vorgestellt sowie strukturelle Bedingungen an die gegebenen offenen Workflownetze erl¨autert. In diesem Anschnitt beweisen wir formal die
korrekte Funktionsweise des Algorithmus.
Satz 4.5 Der Algorithmus InstantaneLE(N1 , N2 ,R) berechnet eine instantane Laufzeitersetzung von N1 nach N2 gem¨aß OG = Rφ .
Beweis:
Der Beweis orientiert sich an der Definition einer Laufzeitersetzung (s. Def. 3.8). Die
ersten beiden Punkte zeigen, dass es sich bei T um eine Transitionsmenge von N1 nach
N2 handelt. Der dritte Punkt beweist das deadlockfreie Verhalten sowie die beschr¨ankte
Kommunikation.
1. z.z. f¨
ur alle t ∈ T gilt: •t ∈ bags(P1 )
Dies folgt direkt aus der Konstruktion der Transitionsmenge in Zeile 3 und Zeile 12
des Algorithmus.
2. z.z. f¨
ur alle t ∈ T gilt: t• ∈ bags(P2 ∪ PI )
In Zeile 6 des Algorithmus werden die modifizierten Markierungen in der Menge
M so gew¨ahlt, dass sie keinen Ausgabeplatz besitzen. Damit folgt die geforderte
Bedingung ebenfalls aus Zeile 3 und Zeile 12.
3. z.z.: N1 ⊕ T ⊕ N2 ist deadlockfrei f¨
ur jedes R ∈ Match(OG)
Nach Lemma 4.4 kann im Netz N2 keine Transition schalten, solange keine Marken
durch eine Laufzeitersetzungstransition von N1 nach N2 u
uhrt wurden. Gem¨aß
¨berf¨
Zeile 3 des Algorithmus umfasst T zumindest die trivialen Laufzeitersetzungstransitionen [mf ]
[mf ], mf ∈ Ω1 , mf ∈ Ω2 . Da nach Voraussetzung der
Partnerautomat R mit dem Ausgangsnetz deadlockfrei interagiert, wird auf jeden
Fall irgendwann eine Laufzeitersetzungstransition schalten k¨onnen (sp¨atestens in
der urspr¨
unglichen Endmarkierung des Ausgangsnetzes).
Der Algorithmus w¨ahlt in Zeile 5 keine echt u
¨berdeckten Markierungen. Also sind
nach dem einmaligen Schalten einer Laufzeitersetzungstransition t die inneren
Pl¨atze von N1 komplett leer. Nach Lemma 4.4 kann nun in N1 und auch in T
keine Transition mehr schalten.
Damit ist nach dem Schalten von t nur noch das zweite Netz, N2 , aktiv. Nun ist
die Fortf¨
uhrbarkeit des verbundenen Netzes mit einem Partnerautomat R dadurch
gew¨ahrleistet, dass die als Nachbereich erzeugten Markierungen m2 der Wissens-
45
4 Instantane Laufzeitersetzungen
funktion K2 f¨
ur das zweite Netz entnommen sind. Diese enth¨alt schließlich genau
die im Netz N2 fortf¨
uhrbaren Markierungen. Also ist die Komposition deadlockfrei
und kommuniziert beschr¨ankt.
Wie bereits oben gezeigt, entfernt jede Transition in T alle Marken der inneren Pl¨atze
von N1 . Damit ist bewiesen, dass die erzeugte Laufzeitersetzung auch eine instantane
Laufzeitersetzung ist.
Wir haben bewiesen, dass die vom Algorithmus erzeugte Transitionsmenge tats¨achlich
eine instantane Laufzeitersetzung darstellt. Dies sagt aber nichts aus u
¨ ber den Nutzen
¨
der Laufzeitersetzung. Wie wir gesehen haben, ist bereits allein die Uberf¨
uhrung der
Endmarkierungen des ersten Netzes in die Endmarkierungen des zweiten Netzes eine
instantane Laufzeitersetzung. Daher wollen wir noch die Vollst¨andigkeit der vom Algorithmus gefundenen L¨osung beweisen.
Satz 4.6 Der Algorithmus InstantaneLE(N1 , N2 ,R) berechnet die vollst¨andige instantane Laufzeitersetzung von N1 nach N2 gem¨aß OG = Rφ .
Beweis:
Angenommen, T w¨are nicht vollst¨andig. Dann g¨abe es mindestens eine instantane Laufzeitersetzungstransition t = m
m , die nicht in T enthalten ist. Nach der Definition Laufzeitersetzungen ist dieses m eine erreichbare, innere Markierung des ersten
Netzes und steht somit in der Erreichbarkeitsfunktion mindestens eines Zustandes q.
I
O
Daher h¨atte der Algorithmus auch mindestens eine Markierung m1 = mN
1 + m1 + m1
N
angeschaut mit m = m1 . Zudem w¨are die Markierung des zweiten Netzes, m2 = m +
mI1 + mO
uhrbar in q und damit in K2 (q) enthalten.
1 , fortf¨
In Zeile 5 wird keine Markierung ausgew¨ahlt, die von einer anderen echt u
¨berdeckt
wird. Anderenfalls w¨are t nicht instantan (N1 w¨
urde nicht komplett geleert). Die einzige
andere M¨oglichkeit, warum der Algorithmus die Transition t verworfen hat, ist somit
die Bedingung in Zeile 9. Nach Proposition 4.3 kann t keine Laufzeitersetzungstransition sein. Dies f¨
uhrt zum Widerspruch, also erzeugt der Algorithmus eine vollst¨andige
instantane Laufzeitersetzung.
Wir haben in diesem Kapitel die instantanen Laufzeitersetzungen kennengelernt und
konnten einen Algorithmus angeben, der f¨
ur zwei gegebene offene Workflownetze und
eine vorgegebene Menge von Strategien als Partner die vollst¨andige instantane Laufzeitersetzung erzeugt. Im n¨achsten Schritt sollen auch nicht-instantane Laufzeitersetzungen
untersucht und erzeugt werden.
46
5 Nebenl¨
aufige Laufzeitersetzungen
Die bisher betrachteten instantanen Laufzeitersetzungen haben die Eigenschaft, dass alle
Marken des Ausgangsnetzes auf einmal in das Zielnetz u
uhrt werden. Petrinetze –
¨berf¨
und damit Worflownetze – arbeiten jedoch per Definition nebenl¨aufig. Das bedeutet, die
Reihenfolge, in der aktivierte Transitionen schalten, ist nicht festgelegt. Die Nebenl¨aufigkeit – also dass verschiedene Aktionen unabh¨angig voneinander stattfinden – ist bei
Gesch¨aftsprozessen explizit erw¨
unscht. In diesem Kapitel soll nun die Nebenl¨aufigkeit
auch f¨
ur Laufzeitersetzungen genutzt werden. Dadurch werden voneinander unabh¨angige
Teile des Ausgangsnetzes auch voneinander unabh¨angig in das Zielnetz u
uhrt.
¨berf¨
Laufzeitersetzungstransitionen sind Teil des verbundenen offenen Worklownetzes und
k¨onnen theoretisch ebenfalls unabh¨angig voneinander schalten. Erst die Beschr¨ankung
im vorherigen Kapitels auf instantane Laufzeitersetzungen erzwingt, dass die komplette
¨
Uberf¨
uhrung des Ausgangs- in das Zielnetz in einem einzigen Schritt erfolgt. Unser folgender Ansatz ist, die in einer instantanen Laufzeitersetzung enthaltenen Nebenl¨aufigkeiten zu finden und zu separieren. Das bedeutet, wir zerteilen instantane Laufzeitersetzungstransitionen in kleinere Transitionen, um so das Ausgangsnetz in mehreren
Schritten nebenl¨aufig in das Zielnetz u
uhren zu k¨onnen.
¨berf¨
Es gibt eine kanonische aber aufw¨andige Methode, nebenl¨aufige Laufzeitersetzungen zu
finden: Man teilt die Transitionen einer instantanen Laufzeitersetzung beliebig in kleinere
Transitionen und pr¨
uft jedesmal durch eine vollst¨andige Zustandsraumanalyse, ob die
entstehende Komposition deadlockfrei bleibt. Dieser Brute-Force-Ansatz ist wegen der
Gr¨oße der Komposition allerdings unpraktisch f¨
ur reale Gesch¨aftsprozesse.
Wir pr¨asentieren im folgenden Abschnitt einen neuen Algorithmus, der Transitionen
einer instantanen Laufzeitersetzung in kleinere Transitionen zerteilt. Dadurch entsteht
eine neue, nebenl¨aufige Laufzeitersetzung. Die einzelnen Arbeitschritte des Algorithmus
werden anhand verschiedener Beispiele detailliert erkl¨art. In den weiteren Abschnitten
folgen ein formaler Korrektheitsbeweis sowie einige heuristische Modifikationen zur Verbesserung des Ergebnisses. Abschließend verdeutlichen wir den Vorteil von nebenl¨aufigen
Laufzeitersetzungen gegen¨
uber instantanen Laufzeitersetzungen. Die zwei folgenden Definitionen erkl¨aren die f¨
ur dieses Kapitel notwendigen Begriffe.
47
5 Nebenl¨aufige Laufzeitersetzungen
Definition 5.1 (Rechenoperationen auf Transitionen)
Als Summe mehrerer Transitionen t1 , . . . , tn bezeichnen wir die Transition
•ti
ti :=
i
ti • .
i
i
Analog ist die Differenz zweier Transition t1 , t2 definiert als
t1 • −t2 • .
t1 − t2 := •t1 − •t2
Voraussetzung zur Bildung der Differenz-Transition ist nat¨urlich, dass die Vor- bzw.
Nachbereiche voneinander subtrahiert werden k¨onnen, also •t2 ≤ •t1 und t2 • ≤ t1 •.
Der Schnitt mehrerer Transitionen t1 , . . . , tn sei
•ti
ti :=
i
ti • .
i
i
Diese Schnitttransition u
¨berf¨uhrt den Schnitt der Vorbereiche auf den Schnitt der Nachbereiche, wobei als Schnitt von Markierungen m1 , . . . , mn das platzweise Minimum der
Marken gemeint sei:
mi (p) := min mi (p).
i
i
Definition 5.2 (u
¨berfu
¨hrte, nicht u
¨berfu
¨hrbare Markierung)
Sei T = (TT , FT , WT ) eine instantane Laufzeitersetzung von N1 nach N2 gem¨aß Rφ .
Eine Markierung heißt u
uhrt in T , wenn eine Transition t ∈ T mit mN = •t
¨berf¨
existiert.
Eine Markierung heißt nicht u
uhrbar, wenn sie in der vollst¨andigen instantanen
¨berf¨
Laufzeitersetzung nicht u
¨berf¨uhrt wird.
5.1 Algorithmus zum Erzeugen nebenl¨
aufiger
Laufzeitersetzungen
Der Algorithmus Zerteilung zum Finden nebenl¨aufiger Laufzeitersetzungstransitionen
basiert auf einer schrittweisen Aufspaltung der Transitionen einer instantanen Laufzeitersetzung. Anfangs sei eine instantane Laufzeitersetzung von N1 nach N2 gem¨aß OG gegeben, bei der die Vorbereiche der Laufzeitersetzungstransitionen paarweise verschieden
sind. Eine solche Transitionsmenge kann aus der vollst¨andigen instantanen Laufzeitersetzung gewonnen werden, indem Transitionen mit doppelt auftretenden Vorbereichen
gel¨oscht werden.
48
5.1 Algorithmus zum Erzeugen nebenl¨aufiger Laufzeitersetzungen
Der unten dargestellte Algorithmus Zerteilung bestimmt die Menge der nicht u
uhr¨berf¨
ten Markierungen (Zeile 1) sowie die Menge aller Teilmarkierungen, die in den u
uhr¨berf¨
ten Markierungen enthalten sind (Zeile 2). Die Zerteilung der Laufzeitersetzungstransitionen findet in den Zeilen 3–8 statt. Dabei wird tempor¨ar mit einer Kopie der aktuellen Laufzeitersetzung gearbeitet, welche der Subalgorithmus ZerteilungsSchritt
ver¨andert. Treten bei einem Zerteilungsschritt Konflikte auf, wird die aktuelle Arbeitskopie der Laufzeitersetzung verworfen. Im Erfolgsfall hingegen wird die Arbeitskopie als
neue Laufzeitersetzung u
¨bernommen. Zum Schluss werden alle Transitionen entfernt, die
Summe anderer Laufzeitersetzungstransitionen sind (Zeilen 9–10).
Zerteilung(N1 , N2 , R, T )
(1)
B := {mb | mb wird nicht u
uhrt in T }
¨berf¨
(2)
M := {m | ∃t ∈ T mit m < •t}
(3)
foreach Markierung m ∈ M
(4)
T := T
(5)
B := B
(6)
if ZerteilungsSchritt(m)
(7)
T := T
(8)
B := B
(9)
foreach t = Σti mit t ∈ T und ti ∈ T
(10)
T := T \ {t}
(11) return T
Algorithmus 5.1: Berechnung nebenl¨aufiger Laufzeitersetzungen
ZerteilungsSchritt(m)
(1)
T := {t | m ≤ •t, t ∈ T }
(2)
m := {t• | t ∈ T }
m}
(3)
T := T ∪ {m
(4)
foreach t ∈ T : m ≤ •t
(5)
if •t − m = ∅ and t • −m = ∅
(6)
return false
(7)
T := T ∪ {(•t − m)
(t • −m )}
(8)
if ∃mb ∈ B mit m ≤ mb
(9)
return false
(10) foreach t ∈ T
(11)
if not ZerteilungsSchritt(•t − m)
(12)
return false
(13) return true
Algorithmus 5.2: Zerteilung von Laufzeitersetzungstransitionen
49
5 Nebenl¨aufige Laufzeitersetzungen
Der Subalgorithmus ZerteilungsSchritt erh¨alt als Eingabe eine Markierung m des
Ausgangsnetzes. Zuerst bildet er den Schnitt aller Nachbereiche der Transitionen, welche
m im Vorbereich enthalten (Zeilen 1–2). Nach der Erzeugung einer neuen Laufzeitersetzungstransition (Zeile 3) wird der Schnitt mit den bestehenden Transitionen gebildet.
Es folgt eine mehrschrittige Pr¨
ufung auf Deadlocks. Bei Transitionen mit leerem Vorbereich wird die Zerteilung abgebrochen (Zeilen 4–7). Falls eine der nicht u
uhrten
¨berf¨
Markierungen den Vorbereich u
¨berdeckt, wird ebenfalls abgebrochen (Zeilen 8–9). Alle
neu entstandenen Transitionen werden zuletzt rekursiv auf Deadlocks u
uft (Zei¨ berpr¨
len 10–12).
Die genaue Vorgehensweise erl¨autern wir am Beispiel von Abbildung 5.3. Der Getr¨ankeautomat mit dem Workflownetz N1 erwartet zuerst die Eingabe von Geld (e) und verarbeitet dann nebenl¨aufig die Wahl eines Getr¨anks (Kaffee C oder Tee T ) und die Wahl
eines S¨
ußungsmittels (Zucker Z oder S¨
ußstoff S). Zuletzt wird das gew¨
unschte Getr¨ank
ausgegeben (G). Der Getr¨ankeautomat gem¨aß N2 verh¨alt sich ganz ¨ahnlich. Im Unterschied zu N1 ist hier die Verarbeitung des Geldes nebenl¨aufig zur Getr¨anke- und
S¨
ußungsmittelwahl.
N1
N2
p0
v0
e
e
p1
p2
v1
T
T
K
K
S
pT
pK
pS
S
pZ
Z
vT
v3
v2
vK
vS
vZ
Z
vE
pf
BKZ
BKZ
BT S
BT S
BKS
BKS
BT Z
vf
Endmarkierungen sind [pf ] bzw. [vf ]
Abbildung 5.3: zwei offene Worfklownetze
50
BT Z
5.1 Algorithmus zum Erzeugen nebenl¨aufiger Laufzeitersetzungen
F¨
ur die betrachteten Beispielnetze verwenden wir folgende instantane Laufzeitersetzung
Tinst als Grundlage f¨
ur die Zerteilung:
t1
t2
t3
t4
t5
t6
:
[p0 ]
: [p1 , p2 ]
: [p1 , pS ]
: [p1 , pZ ]
: [p2 , pT ]
: [p2 , pK ]
[v0 ]
t7
[v1 , vE , v3 ] t8
[v1 , vE , vS ] t9
[v1 , vE , vZ ] t10
[v3 , vE , vT ] t11
[v3 , vE , vK ]
: [pT , pS ]
: [pT , pZ ]
: [pK , pS ]
: [pK , pZ ]
:
[pf ]
[vE , vT , vS ]
[vE , vT , vZ ]
[vE , vK , vS ]
[vE , vK , vZ ]
[vf ]
Tabelle 5.4: instantane Laufzeitersetzung zu Abb. 5.3
Beim Aufruf Zerteilung(N1 , N2 , R, Tinst ) bestimmt unser Algorithmus als erstes die
Menge B aller nicht u
uhrten Markierungen (Zeile 2). In unserem Beispiel werden
¨berf¨
alle erreichbaren Markierungen u
uhrt, somit ist B = ∅. Sp¨ater in Abschnitt 5.2.2
¨ berf¨
behandeln wir ein Beispiel, bei dem B nicht-leer ist.
In Zeile 4 bis 7 iteriert der Algorithmus u
¨ber alle Teilmarkierungen der Vorbereiche von
T . Sei eine betrachtete solche Markierung m = [p1 ]. Der Aufruf von ZerteilungsSchritt([p1 ]) bestimmt als erstes alle Laufzeitersetzungstransitionen, in deren Vorbereich m enthalten ist. In unserem Beispiel sind es die drei Transitionen t2 , t3 und t4 von
Tabelle 5.4, in deren Vorbereich sich [p1 ] befindet.
Die Schnittmenge der Nachbereiche dieser drei Transitionen ist m = [v1 , vE ] (Zeile 2),
[v1 , vE ] eingef¨
ugt (Zeile 3). Die
somit wird die Laufzeitersetzungstransition [p1 ]
anderen Transitionen werden gem¨aß Zeile 7 des Algorithmus folgendermaßen ver¨andert:
([p1 , p2 ]
([p1 , pS ]
([p1 , pZ ]
[v1 , vE , v3 ]) − ([p1 ]
[v1 , vE , vS ]) − ([p1 ]
[v1 , vE , vZ ]) − ([p1 ]
[v1 , vE ]) = [p2 ]
[v1 , vE ]) = [pS ]
[v1 , vE ]) = [pZ ]
[v3 ]
[vS ]
[vZ ]
Die Zeilen 8 bis 9 des Subalgorithmus ZerteilungsSchritt sind hier unbedeutend,
weil es keine nicht u
uhrten Markierungen gibt. In Zeile 11 wird nun die ver¨ander¨berf¨
te Transitionsmenge rekursiv weiter zerteilt. Es erfolgt also beispielsweise der Aufruf
ZerteilungsSchritt([p2 ]). Dabei wird wiederum [p2 ]
[v3 ] als neue Transition
[vE , vT ] und [pK ]
[vE , vK ] zum weitehinzugef¨
ugt. Rekursiv bleiben [pT ]
ren Zerteilen u
¨brig. In unserem Beispiel liefern diese Aufrufe jeweils true als Ergebnis
¨
zur¨
uck, sodass alle lokalen Anderungen
in die Transitionsmenge T u
¨bernommen werden.
Zuletzt werden alle diejenigen Transitionen wieder entfernt, die sich als Summe anderer
Transitionen darstellen lassen. Abbildung 5.5 zeigt das Ergebnis von Zerteilung(N1 ,
N2 , R, Tinst ).
51
5 Nebenl¨aufige Laufzeitersetzungen
T
N1
N2
p0
v0
e
e
p1
p2
v1
T
T
K
K
S
pT
pK
pS
S
pZ
Z
vT
v3
v2
vK
vS
vZ
Z
vE
pf
BKZ
BKZ
BT S
BT S
BKS
BKS
vf
BT Z
BT Z
Anfangsmarkierung des verbundenen Netzes ist [p0 ], Endmarkierung ist [vf ]
Abbildung 5.5: berechnete nebenl¨aufige Laufzeitersetzung
Man u
¨berzeugt sich leicht davon, dass das Ergebnis des Algorithmus Zerteilung nicht
eindeutig festgelegt ist. Die zuvor erhaltenen Laufzeitersetzungstransitionen sind zum
Vergleich in Tabelle 5.6 aufgelistet. W¨ahlt der Algorithmus in Zeile 3 statt [p1 ] zuerst
die Markierung [p2 ], dann enth¨alt die erzeugte Laufzeitersetzung die Transitionen laut
Tabelle 5.7.
[p0 ]
[p1 ]
[p2 ]
[pf ]
[v0 ]
[pT ]
[v1 , vE ] [pK ]
[v3 ]
[pZ ]
[vf ]
[pS ]
[vE , vT ]
[vE , vK ]
[vZ ]
[vS ]
Tabelle 5.6: zerteilte Laufzeitersetzungstransitionen zur Tab. 5.4
[p0 ]
[p1 ]
[p2 ]
[pf ]
[v0 ]
[pT ]
[v1 ]
[pK ]
[v3 , vE ] [pZ ]
[vf ]
[pS ]
[vT ]
[vK ]
[vE , vZ ]
[vE , vS ]
Tabelle 5.7: anders zerteilte Laufzeitersetzungstransitionen zur Tab. 5.4
52
5.2 Korrektheit
5.2 Korrektheit
Die Korrektheit des im vorherigen Abschnitt vorgestellten Algorithmus Zerteilung
wollen wir nun formal beweisen. Zun¨achst beweisen wir dazu zwei Lemmata f¨
ur die beiden Abbruchbedingungen des Subalgorithmus ZerteilungsSchritt. Diese Aussagen
sind f¨
ur den anschließenden Korrektheitsbeweis notwendig.
5.2.1 Leerer Vorbereich
Transitionen mit leerem Vorbereich k¨onnen beliebig oft schalten und damit in ihrem
Nachbereich beliebig viele Marken erzeugen. Wir fordern jedoch beschr¨ankte Netze
f¨
ur die Interaktion. Dass beim Zerteilen von Transitionen leere Vorbereiche entstehen
k¨onnen, zeigt das folgende Beispiel in Abbildung 5.8. F¨
ur dieses Netz erh¨alt man durch
den Aufruf ZerteilungsSchritt([p1]) zerteilte Transitionen mit leerem Vorbereich.
Netz 1
Netz 2
p0
v0
e
e
p1
p2
p3
v1
G
pf
G
vf
Endmarkierungen sind [pf ] bzw. [vf ]
Abbildung 5.8: Test auf leeren Vorbereich
¨
Zun¨achst wird die Uberf¨
uhrung [p1 ]
[v1 ] der Menge T hinzugef¨
ugt. Bei der Subtraktion dieser Transition von den anderen Transitionen aus T entstehen die Differen[] und [p3 ]
[]. Infolge dessen werden diese neuen Transitionen auch
zen [p2 ]
von der Transition [p2 , p3 ]
[v1 ] subtrahiert. Damit bleibt als Ergebnis []
[v1 ]
u
¨brig. Mit dieser Transition w¨are das verbundene Netz allerdings nicht mehr beschr¨ankt.
Deswegen verwirft der Subalgorithmus ZerteilungsSchritt in Zeile 5 und 6 diese Modifikation.
53
5 Nebenl¨aufige Laufzeitersetzungen
¨
Die Uberpr¨
ufung in Zeile 5 ist wesentlich f¨
ur das folgende Lemma.
Lemma 5.3 Sei Tinst eine instantane Laufzeitersetzung von N1 nach N2 gem¨aß OG =
Rφ , bei der die Vorbereiche der Laufzeitersetzungstransitionen paarweise verschieden
sind. Sei T die Transitionsmenge die von Zerteilung(N1 , N2 , R, Tinst ) bestimmte
Transitionsmenge vor dem L¨oschen der Summentransitionen, also vor Zeile 9 des Algorithmus. Wann immer mehrere Transitionen t1 , . . . , tn ∈ T in der Summe im Vorbereich
genau den Vorbereich einer Transition t von T ergeben, ist
ti = t.
i
Beweis:
Wir zeigen dies induktiv u
¨ber n.
Induktionsanfang: F¨
ur n = 1 ist •t = •t1 .
Ist t1 eine instantane Laufzeitersetzungstransition, dann gilt t = t1 offensichtlich.
Schließlich enth¨alt Tinst keine zwei Transitionen mit demselben Vorbereich. Sei also
m2 eine zerteilte Transition. Wir wollen die umgekehrte Annahme,
t1 = m1
t• = m2 , zum Widerspruch f¨
uhren.
In einem Rekursionsschritt des Algorithmus Zerteilung wird auch ZerteilungsSchritt(m1 ) aufgerufen, da sonst t1 nicht in T h¨atte aufgenommen werden k¨onnen.
In Zeile 2 wird dabei der Schnitt m der Nachbereiche aller Transitionen, die m1
im Vorbereich enthalten, gebildet. Zu diesen Nachbereichen geh¨oren auch m2 und
t•. Wegen t• = m2 ist der Schnitt m echt kleiner als m2 .
Der Algorithmus erzeugt eine neue Transition m1
m , die anschließend unter
anderem von t1 subtrahiert wird. Wegen t1 − m1
m = []
[m2 − m ]
hat diese Differenz einen leeren Vorbereich und einen nicht-leeren Nachbereich.
Der Algorithmus liefert dann false zur¨
uck (Zeile 6) und verwirft somit den entsprechenden Zerteilungsschritt. Dies ist ein Widerspruch zur Existenz von t und
t1 in T , womit die urspr¨
ungliche Behauptung t1 = t bewiesen ist.
Induktionsbehauptung: Wenn die Aussage f¨
ur je n Transitionen gilt, gilt sie auch f¨
ur
n + 1 Transitionen.
Induktionsbeweis: Seien Transitionen t1 , . . . , tn+1 ∈ T gegeben, sodass der summierte
n+1
•ti auch Vorbereich einer einzelnen Transition t aus T ist.
Vorbereich
i=1
m . Innerhalb des Aufrufes ZerteilungsSchritt(m) ist auch
Sei t1 = m
die Differenz d := t − t1 bestimmt worden (Zeile 7). Weil der Vorbereich der Trann+1
sitionen t2 , . . . , tn+1 in der Summe •d ergibt, gilt induktiv d =
ti .
i=2
54
5.2 Korrektheit
Ebenfalls muss ZerteilungsSchritt(•d) aufgerufen worden sein, womit t − d
erzeugt worden ist. Es gilt nach Induktionsvoraussetzung t − d = t1 . Insgesamt gilt
n+1
also t = t1 + d =
ti .
i=1
Als Spezialfall aus dem Lemma 5.3 ergibt sich die folgende Proposition.
Proposition 5.4 Sei T die von Zerteilung(N1 , N2 , R, Tinst ) erzeugte Transitionsmenge. Wann immer t1 , . . . , tn ∈ T zusammen im Vorbereich eine erreichbare innere
Markierung von N1 ergeben, ist ihre Summe eine instantane Laufzeitersetzungstransition aus Tinst .
5.2.2 Nicht ¨
uberf¨
uhrbare Markierungen
Im Allgemeinen sind nicht alle Markierungen, die im Ausgangsnetz erreicht werden
k¨onnen, durch eine instantane Laufzeitersetzungstransition in das Zielnetz u
uhrbar.
¨berf¨
Entst¨
unden bei der Zerteilung instantaner Laufzeitersetzungstransitionen solche Transitionen, deren summierte Vorbereiche eine nicht u
uhrbare Markierung mb ergeben, so
¨ berf¨
w¨are das verbundene Netz mitunter nicht mehr bedienbar. Die Transitionen stellen dann
¨
n¨amlich zusammen eine instantane Uberf¨
uhrung dieser Markierung mb dar. Nach Voraussetzung gibt es keine solche Laufzeitersetzungstransition, daher erhielten wir einen
Deadlock in der Komposition. Wir zeigen, dass ist es problematisch ist, nur einen Teil
einer nicht u
uhrbaren Markierung als Vorbereich einer Transition zu haben.
¨berf¨
In Abbildung 5.9 sind dazu zwei Getr¨ankeautomaten dargestellt, die neben dem Getr¨ank
G auch eine Zettel Z ausgeben. Das Netz 1 gibt den Zettel im Falle von Kaffee K dabei
unabh¨angig von der Bezahlung e. Im Falle von Tee T erh¨alt man den Zettel ebenso
wie in Netz 2 erst nach dem Bezahlen. Die Strategien der Benutzer sind durch den
Automaten R festgelegt. Er ist hier mit den Wissensfunktionen K1 und K2 abgebildet.
Bei diesem Beispiel k¨onnen einige erreichbare Markierungen des Ausgangsnetzes nicht
u
uhrt werden. Als instantane Laufzeitersetzung sei folgendes Tinst gegeben:
¨berf¨
[p0 ]
[p1 , p2 ]
[p1 , p4 ]
[v0 ]
[pf ]
[v1 , v2 ] [p2 , p3 ]
[v1 , e] [p3 , p4 ]
[vf ]
[v2 , v3 ]
[v2 , e]
55
5 Nebenl¨aufige Laufzeitersetzungen
R
K1
[p0 , T ]
[p1 , p2 ]
Netz 1
q1
Netz 2
p0
!e
v0
q2
p2
p3
p1
v1
e
v2
v3
e
p4
q3
p5
Z
Z
G
pf
K1
[p0 , K]
[p2 , p3 ]
[p2 , p5 , Z]
K1
[pf , B]
?G
G
q4
vf
K1
[pf ]
K2
[v0 , K]
[v2 , v3 ]
q5
K2
[v0 , T, e]
[v1 , v2 , e]
[vf , Z, G]
K1
[p0 , K, e]
[p2 , p3 , e]
[p2 , p5 , Z, e]
[p3 , p4 ]
[p4 , p5 , Z]
[pf , Z, G]
?Z
K
K
K2
[v0 ]
!K
K1
[p0 , T, e]
[p1 , p2 , e]
[p1 , p4 ]
[pf , Z, G]
T
T
q0
!T
K2
[v0 , T ]
[v1 , v2 ]
K1
[p0 ]
!e
K2
[v0 , K, e]
[v2 , v3 , e]
[vf , Z, G]
q6
?Z
K2
[vf , B]
K1
[p2 , p5 , e]
[p4 , p5 ]
[pf , G]
?G
K2
[vf ]
Endmarkierungen sind [pf ] bzw. [vf ]
q7
K2
[vf , B]
q8
K1
[pf ]
K2
[vf ]
Abbildung 5.9: Test auf nicht-¨
uberf¨
uhrbare Markierungen
Die Menge B des Algorithmus Zerteilung enth¨alt die Markierungen
[p2 , p5 , Z], [p2 , p5 , e], [p2 , p5 , Z, e], [p4 , p5 ] und [p4 , p5 , Z].
Bliebe diese Menge B unber¨
ucksichtigt, so entst¨
unden beim Zerteilen die Transitionen
[p1 ]
[v1 ], [p2 ]
[v2 ], [p3 ]
[v3 ] sowie [p4 ]
[e]. Damit k¨onnte bei[e]
spielsweise von der Markierung [p4 , p5 ] aus die Laufzeitersetzungstransition [p4 ]
schalten, sodass die Markierung [p5 ] im Ausgangsnetz u
¨ brig bliebe. Dies ist ein Deadlock
in der Komposition aus dem verbundenen Netz und seinem Partner.
Um diesen Deadlock auszuschließen, u
uft ZerteilungsSchritt([p4]) in Zeile 8,
¨ berpr¨
ob [p4 ] als Teil einer der Markierung aus B vorkommt. Wegen [p4 , p5 ] ∈ B ist dies der
Fall und der Aufruf liefert den Wert false, wodurch die oben beschriebene, fehlerhafte
Teilung verworfen wird.
F¨
ur beliebige Netze funktioniert diese Deadlockpr¨
ufung ebenfalls, wie das folgende Lemma zeigt.
56
5.2 Korrektheit
Lemma 5.5 Sei Tinst eine instantane Laufzeitersetzung von N1 nach N2 gem¨aß OG =
Rφ , bei der die Vorbereiche der Laufzeitersetzungstransitionen paarweise verschieden
sind. Sei T die Transitionsmenge, die von Zerteilung(N1 , N2 , R, Tinst ) berechnet
wurde. Wenn in der Komposition aus verbundenem Netz N1 ⊕ T ⊕ N2 und R keine
Transition aus T schalten kann, obwohl N1 noch nicht leer ist, dann kann eine Transition aus N1 schalten.
Beweis:
Angenommen, N1 ist nicht leer und keine Transition aus N1 oder T kann schalten.
Solange u
¨berhaupt keine Laufzeitersetzungstransition geschaltet hat, kann kein Deadlock
erreicht worden sein. Die bereits ausgef¨
uhrten Transitionen aus T seien t1 , . . . , tn und
makt sei die aktuelle Markierung von N1 . Dann ist m := makt + •ti eine erreichbare
i
Markierung von N1 . G¨abe es eine instantane Laufzeitersetzungstransition mit mN als
Vorbereich, dann h¨atte der Subalgorithmus ZerteilungsSchritt auch die Differenz
aus dieser Transition und t1 , . . . , tn zu T hinzugef¨
ugt. Somit k¨onnte jetzt eine Transition
aus T schalten, im Widerspruch zur Voraussetzung.
So ist mN nicht Vorbereich einer instantanen Laufzeitersetzungstransition, also eine nicht
u
¨berf¨uhrte Markierung (m ∈ B). Wegen der Bedingung in Zeile 8 von ZerteilungsSchritt(m) w¨are dann keines der ti zu T hinzugef¨
ugt worden, Widerspruch. Wenn N1
nicht leer ist und keine Transition aus T aktiviert ist, kann somit eine Transition aus
N1 schalten.
5.2.3 Korrektheit des Algorithmus Zerteilung
Mithilfe der verherigen Lemmata f¨
uhren wir nun den formalen Korrektheitsbeweis f¨
ur
den Algorithmus Zerteilung.
Satz 5.6 Sei Tinst eine instantane Laufzeitersetzung, bei welcher die Vorbereiche der
Transitionen paarweise verschieden sind. Die von Zerteilung(N1 , N2 , R, Tinst ) erzeugte Transitionsmenge T stellt eine korrekte Laufzeitersetzung von N1 nach N2 gem¨aß
OG = Rφ dar.
Beweis:
Die erzeugte Menge T ist offensichtlich eine Transitionsmenge von N1 nach N2 . Es gen¨
ugt
somit zu zeigen, dass die Komposition des verbundenen Netzes N1 ⊕ T ⊕ N2 mit Interaktionspartnern gem¨aß OG keine Deadlocks enth¨alt. Wir unterscheiden dazu zwei F¨alle
– je nachdem, ob in der aktuellen Markierung noch innere Pl¨atze des Ausgangsnetzes
markiert sind oder nicht.
57
5 Nebenl¨aufige Laufzeitersetzungen
Fall 1: P1 ist nicht leer.
Sollte noch keine Laufzeitersetzungstransition geschaltet haben, dann hat die bisherige Interaktion nur zwischen dem Partner und N1 stattgefunden. Dabei werden
keine Deadlocks erreicht, weil OG OGN1 .
Haben hingegen bereits Transitionen t1 , . . . , tn ∈ T geschaltet, dann ist ebenfalls
kein Deadlock erreicht. Schließlich kann gem¨aß Lemma 5.5 eine weitere Laufzeitersetzungstransition, eine Transition des Ausgangsnetzes oder der Interaktionspartner schalten.
Fall 2: P1 ist leer.
Dann haben bereits die Laufzeitersetzungstransitionen t1 , . . . tn ∈ T geschaltet
n
•ti = m1 , wobei m1 eine erreichbare Markierung von N1 ist. Gem¨aß
mit tΣ :=
i=1
Proposition 5.4 ist tΣ eine instantane Laufzeitersetzungstransition, weswegen der
Nachbereich eine in N2 fortf¨
uhrbare Marierung ist. Demnach kann in der Komposition kein Deadlock erreicht werden.
In beiden F¨allen ist die Komposition deadlockfrei, T ist also eine Laufzeitersetzung von
N1 nach N2 gem¨aß OG.
5.3 Heuristik
Der vorangegange Korrektheitsbeweis hat gezeigt, das der Algorithmus Zerteilung in
der Lage ist, aus einer instantanen Laufzeitersetzung eine nebenl¨aufige Laufzeitersetzung zu erzeugen. Wir werden sehen, dass der Algorithmus – so wie er beschrieben ist
– nicht immer die sch¨onste“ L¨osung findet. Begr¨
undet ist dies in der Pr¨
ufung in Zei”
le 8 des Subalgorithmus ZerteilungsSchritt auf potentiell deadlock-verursachende
Transitionen. Offensichtlich werden umso h¨aufiger Zerteilungsschritte verworfen, je mehr
Markierungen in der Menge B enthalten sind.
In diesem Abschnitt diskutieren wir verschiedene M¨oglichkeiten, seltener Zerteilungsschritte zu verwerfen, unter Bewahrung der Deadlockfreiheit der Komposition aus verbundenem Netz und Interaktionspartner. Einige Ans¨atze, dies zu erreichen, sind:
◦ alle u
uhrbaren Markierungen in der Transitionsmenge T auch tats¨achlich zu
¨ berf¨
u
uhren – damit enth¨alt B nur nicht ¨uberf¨uhrbare Markierungen,
¨ berf¨
◦ differenzierte Deadlockpr¨
ufung – f¨
ur manche nicht u
uhrbaren Markierungen
¨ berf¨
kann das Netz auch dann schalten, wenn ein Teil bereits u
uhrt wurde,
¨berf¨
58
5.3 Heuristik
◦ die Menge B verkleinern – bei manchen nicht u
uhrbaren Markierungen kann
¨berf¨
in der Komposition stets der Partner R agieren.
Der erste Ansatz bezieht sich auf die Menge Tinst , die beim Aufruf von Zerteilung(N1 ,
N2 , R, Tinst ) als Eingabe gegeben ist. Die anderen beiden Ans¨atze sollen mithilfe geeigneter Modifikationen des Algorithmus umgesetzt werden. Wir pr¨asentieren jeweils eine
Heuristik mit erkl¨arendem Beispiel. Zus¨atzlich beweisen wir formal die Korrektheit der
vorgestellten Algorithmusvarianten.
5.3.1 differenzierte Deadlockpr¨
ufung
Motiviert ist die folgende heuristische Analyse durch das Beispiel in Abbildung 5.10. Die
beiden Netze sind fast identisch mit denen aus Abbildung 5.9. Der einzige Unterschied
ist, dass nebenl¨aufig zu dem oben beschriebenen Verhalten noch eine weitere Eingabe A
verarbeitet und die Nachricht S ausgegeben wird. Der Automat R in Abbildung 5.11
beschreibt die betrachtete Strategie.
p0
v0
Netz 1
pα
Netz 2
p0
v0
vα
T
T
p2
p3
K
K
p1
v1
e
p4
A
v2
v3
S
e
S
Z
A
Z
p5
G
pβ
pf
G
vf
pf
vβ
vf
Anfangsmarkierungen sind [p0 ] bzw. [v0 ], Endmarkierungen sind [pf ] bzw. [vf ]
Abbildung 5.10: Beispielnetze f¨
ur Heuristiken
59
5 Nebenl¨aufige Laufzeitersetzungen
K1
[p0 ]
q0
R
K1
[p0 , K]
[pα , p2 , p3 ]
[pα , p2 , p5 , Z]
K2
[v0 ]
!K
q1
K1
[p0 , K, e]
[pα , p2 , p3 , e]
[pα , p2 , p5 , Z, e]
[pα , p3 , p4 ]
[pα , p4 , p5 , Z]
[pα , pf , Z, G]
K2
[v0 , K]
[vα , v2 , v3 ]
K1
[pα , p2 , p5 , e]
[pα , p4 , p5 ]
[pα , pf , G]
!e
q2
?Z
K2
[v0 , K, e]
[vα , v2 , v3 , e]
[vα , vf , Z, G]
q3
?G
q4
K2
[vα , vf , B]
K1
[pα , pf ]
K2
[vα , vf ]
!A
q5
K1
[pα , pf , A]
[pβ , pf , S]
[pf , S]
K2
[vα , vf , A]
[vβ , vf , S]
[vf , S]
?S
q6
K1
[pf ]
K2
[vf ]
Abbildung 5.11: Serviceautomat mit Wissensfunktion f¨
ur die Netze aus Abb. 5.10
Man erkennt leicht, dass die Transitionen der Laufzeitersetzung f¨
ur das Beispiel aus
Abbildung 5.9 zusammen mit den Transitionen [pα ]
[vα ] und [pβ ]
[vβ ] eine
nebenl¨aufige Laufzeitersetzung f¨
ur die zwei Netze aus Abbildung 5.10 sind. Die Menge
B enth¨alt in diesem Beispiel nur nicht u
uhrbare Markierungen von N1 , siehe Tabel¨berf¨
le 5.12. Erreicht das verbundene Netz N1 ⊕T ⊕N2 bei der Interaktion mit einem Service[pα , p2 , p5 , Z]
[pα , p2 , p5 , Z, e]
[pα , p2 , p5 , e]
[pα , p4 , p5 , Z]
[pα , p4 , p5 ]
Tabelle 5.12: nicht u
uhrbare Markierungen
¨berf¨
automaten R die Markierung [pα , p2 , p5 , e], so kann N1 weiterschalten, auch wenn die
¨
Uberf¨
uhrung [pα ]
[vα ] bereits stattgefunden hat. Das Ausgangsnetz kann von der
Markierung [p2 , p5 , e] schalten nach [pf , G]. Damit hat das Netz wieder eine u
uhrba¨berf¨
re Markierung erreicht. Die Markierung [pα , p2 , p5 , e] soll daher im folgenden nicht mehr
zum Abbruch beim Zerteilen der Transition f¨
uhren.
Verallgemeinert soll kein Abbruch der Zerteilung erfolgen, wenn N1 schalten kann nachdem bereits ein Teil der Marken einer nicht u
uhrbaren Markierung durch Laufzeit¨berf¨
ersetzungstransitionen in das Zielnetz u
berf¨
u
hrt
worden
sind. Daf¨
ur ist sicherzustellen,
¨
dass die von N1 ben¨otigten Eingabepl¨atze nicht von den Transitionen aus N2 verarbeitet
werden.
Mit einer Modifikation des Zerteilungsalgorithmus l¨asst sich dieses Ziel erreichen: Falls
der Vorbereich einer zerteilten Transition in einer Markierung mb in B enthalten ist,
bricht der Algorithmus nicht notwendigerweise ab, sondern subtrahiert zun¨achst den
Vorbereich der Transition von mb . Dann pr¨
uft er, ob es f¨
ur die Differenzmarkierung
noch aktivierte Transitionen in N1 gibt. Ben¨otigen diese aktivierten Transitionen zum
Schalten auch Eingabepl¨atze, so muss sichergestellt sein, dass N2 keine Marken von
60
5.3 Heuristik
diesen Pl¨atzen entfernt. Dazu wird bestimmt, welche Transitionen in N2 potentiell durch
den Nachbereich der neu erzeugten Laufzeitersetzungstransition aktiviert werden. Sobald
eine der potentiell aktivierten Transitionen einen f¨
ur N1 notwendigen Eingabeplatz im
Vorbereich hat, wird die aktuelle Zerteilung verworfen.
Wir definieren eine Abbildung V von den Eingabepl¨atzen PI auf Mengen von Pl¨atzen
in N2 , die folgende Eigenschaft besitzt: Wenn q ∈ V (pi ), dann gibt es entlang der B¨ogen
in N2 einen Pfad von q zu einer Transition, die auch pi im Vorbereich hat. Formal sei
S(pi ) := {t | ∃ • t(pi ) > 0}
die Menge der Transitionen, die die Eingabe l verwenden, und
V (pi ) := {p | ∃t ∈ S(pi ) : es gibt einen Pfad von p nach t}
die entsprechend gesuchte Platzmenge des Zielnetzes.
Nachstehend zeigen wir zum Vergleich den originalen Ausschnitt des Subalgorithmus
und die modifizierte Algorithmusvariante.
ZerteilungsSchritt(m)
..
.
(7)
(8)
(9)
(10)
..
.
...
if ∃mb ∈ B mit m ≤ mb
return false
...
ZerteilungsSchritt*(m)
..
.
(7)
...
(8)
foreach mb ∈ B : m ≤ mb
(9a)
mb := mb − m
(9b)
if mb aktiviert keine Transition in T1
(9c)
return false
(9d)
L := {pi ∈ PI | ∃t ∈ T1 : t ist aktiviert in mb und [pi ] ≤ •t}
(9e)
foreach pi ∈ L
(9f)
if m ∩ V (pi ) = ∅
(9g)
return false
(9h)
B := B ∪ {(mb − m)}
(10) . . .
..
.
Algorithmus 5.13: modifizierter Ausschnitt aus ZerteilungsSchritt
61
5 Nebenl¨aufige Laufzeitersetzungen
Wir erl¨autern die Rechenschritte beispielhaft am Aufruf ZerteilungsSchritt*([pα]).
Der Algorithmus pr¨
uft in einem Zerteilungsschritt die m¨ogliche Laufzeitersetzungstransition [pα ]
[vα ]. In Zeile 8 wird dabei die Markierung mb = [pα , p2 , p5 , e] ∈ B
ausgew¨ahlt. Als Differenz aus mb und m = [pα ] erhalten wir in Zeile 9a mb = mb − m =
[p2 , p5 , e]. Genau eine Transition von N1 ist aktiviert in mb (Zeile 9b). Damit bestimmt
der Algorithmus als n¨achstes die Menge L der verwendeten Eingabepl¨atze zu L = {e}
(Zeile 9d).
V (e) = {v0 , v0 , v1 , v2 , v3 } sind diejenigen Pl¨atze, welche zur Aktivierung der e-verarbeitenden Transition in N2 beitragen k¨onnten (Zeile 9e). Man sieht, dass in Zeile 9f die
Schnittmenge {vα } ∩ {v0 , v0 , v1 , v2 , v3 } leer ist, daher wird die Laufzeitersetzungstransition [pα ]
[vα ] an dieser Stelle nicht verworfen (Zeile 9g).
Wir zeigen nun, dass f¨
ur diesen erweiterten Algorithmus das Lemma 5.5 in ¨ahnlicher
Form zutrifft.
Lemma 5.7 Sei Tinst eine instantane Laufzeitersetzung von N1 nach N2 gem¨aß OG =
Rφ , bei der die Vorbereiche der Laufzeitersetzungstransitionen paarweise verschieden
sind. Sei T die Transitionsmenge, die von Zerteilung(N1 , N2 , R, Tinst ) mit dem
modifiziertem Subalgorithmus ZerteilungsSchritt* berechnet wurde. Wenn in der
Komposition aus verbundenem Netz N1 ⊕ T ⊕ N2 und R keine Transition aus T schalten
kann, obwohl N1 noch nicht leer ist, dann kann eine Transition aus N1 schalten.
Beweis:
Angenommen, N1 ist nicht leer und keine Transition aus N1 oder T kann schalten.
Wir k¨onnen die Argumentation aus dem Beweis zu Lemma 5.5 an dieser Stelle zum
großen Teil u
¨bernehmen. So ist nur noch der Fall zu betrachten, dass bereits die Laufzeitersetzungstransitionen t1 , . . . , tn geschaltet haben und die aktuelle Markierung makt
von N1 nicht Vorbereich einer instantanen Transition aus Tinst ist.
•ti eine nicht u
uhrte Markierung. Nach der Initia¨berf¨
In diesem Fall ist m := makt +
i
lisierung der Menge B im Algorithmus Zerteilung gilt m ∈ B. Bei der Erzeugung der
Transitionen ti ist jeweils die Differenz aus den Markierungen von B und dem Vorbereich
•ti zu B hinzugenommen worden (Zeile 9h). Somit gilt makt ∈ B.
Gem¨aß Zeile 9b und 9c des Algorithmus, gibt es aktivierte Transitionen in makt . Wegen
¨
der Uberpr¨
ufung in den Zeilen 9d bis 9g ist im Zielnetz keine Transition aktiviert, die
den Vorbereich mit den im Ausgangsnetz aktivierten Transitionen teilt. Somit kann eine
der aktivierten Transitionen von N1 schalten.
62
5.3 Heuristik
Die angegebenen Modifikationen des Zerteilungsalgorithmus arbeiten, wie wir gesehen
haben, korrekt, sind jedoch nicht vollst¨andig. So kann es ebenso wie im urspr¨
unglichen
Subalgorithmus ZerteilungsSchritt passieren, dass Laufzeitersetzungstransitionen
ausgeschlossen werden, welche in der Komposition tats¨achlich gar keinen Deadlock verursachen.
Ein derartiges Szenario zeigt die Abbildung 5.14. Hier gibt es eine Transition t, in deren
Vorbereich ein niemals markierter Platz liegt. Bei der heuristischen Vorgehensweise wird
¨
durch die Uberpr¨
ufung in Zeile 9f der Subalgorithmus ZerteilungsSchritt* abbrechen, obwohl die Transition t tats¨achlich nie eine Marke vom Eingabeplatz e entfernt.
p0
v0
Netz 1
pα
Netz 2
p0
v0
vα
v
T
T
p2
t
p3
K
K
p1
v1
e
p4
A
v2
v3
S
e
S
Z
A
Z
p5
G
pβ
pf
G
vf
pf
vβ
vf
Anfangsmarkierungen sind [p0 ] bzw. [v0 ], Endmarkierungen sind [pf ] bzw. [vf ]
Abbildung 5.14: Problembeispiel f¨
ur Heuristiken
Dieses Beispiel zeigt, dass der vorgeschlagene Algorithmus lediglich heuristischen Charakter hat. Als Daumenregel l¨asst sich aber festhalten, dass f¨
ur Transitionspfade, die
nebenl¨aufig im Zielnetz sind, der modifizierte Algorithmus diese Nebenl¨aufigkeiten auch
findet.
63
5 Nebenl¨aufige Laufzeitersetzungen
5.3.2 Verkleinung der Menge B
Im oben beschriebenen Beispiel von Abbildung 5.10 (Seite 59) wird die Zerteilung der instantanen Laufzeitersetzungstransitionen in die Teiltransition [pα ]
[vα ] beim Aufruf von ZerteilungsSchritt([pα ]) abgebrochen. Der Grund ist, dass N1 in der nicht
u
uhrbaren Markierung [pα , p2 , p5 , Z] nicht schalten kann. Allerdings kann der Auto¨berf¨
mat R aus Abbildung 5.11 bei dieser Markierung des Ausgangsnetzes noch die Nachricht
e senden und anschließend N1 kann durchaus weiterschalten.
Die genannte Markierung soll daher im folgenden nicht mehr Abbruchgrund beim Zerteilen der Transition sein. Ein Nachfolgezustand von ([pα , p2 , p5 , Z], q1 ) in der Komposition
ist ([pα , p2 , p5 , Z, e], q2 ), d.h. der Partner hat die Eingabe e vorgenommen. Verarbeitet
er noch die Ausgabe Z, so erhalten wir die Markierung m = [pα , p2 , p5 , e]. Im Aufruf
ZerteilungsSchritt([pα]) wurde [pα , p2 , p5 , Z], [pα , p2 , p5 , Z, e] und [pα , p2 , p5 , e] gepr¨
uft. Stattdessen soll nur noch f¨
ur [pα , p2 , p5 , e] gepr¨
uft werden, ob diese Markierung
einen Deadlock in der Komposition ergibt.
Allgemein ist in der Komposition kein Deadlock erreicht, solange der Partner schalten
kann. Wir erg¨anzen den Zerteilungsalgorithmus dahingehend, dass entsprechende Markierungen aus B entfernt werden. Ob der Partner R bei einer bestimmten Markierung
mb des Ausgangsnetzes schalten kann, wird anhand der Nachfolger derjenigen Zust¨ande
entschieden, f¨
ur die diese Markierung erreichbar ist (mb ∈ K1 (q)). Damit R u
¨ ber eine
Kante (q, l, q ) nach q wechseln kann, muss – falls l ein Ausgabeplatz des Netzes ist – l
auch markiert sein in mb .
Nachstehend zeigen wir zum Vergleich den originalen Ausschnitt des Algorithmus Zerteilung. Die Erweiterung dieser Initialisierung der Menge B ist auf der folgenden Seite
algorithmisch dargestellt.
Zerteilung(N1 , N2 , R, T )
(1)
B := {mb | mb wird nicht u
uhrt in T }
¨berf¨
(2)
...
..
.
Anhand einiger Beispielaufrufe von PartnerKannSchalten(mb ) f¨
ur verschiedene Markierungen mb verdeutlichen wir die Vorgehensweise des modifzierten Algorithmus. Beim
Aufruf PartnerKannSchalten([pα , p2 , p5 , Z]) existiert in Zeile i nur einen Zustand,
n¨amlich q1 , f¨
ur den die Markierung mb erreichbar ist. Im Automaten R gibt es einen
Nachfolger von q1 , die Kante ist mit dem Eingabeplatz e beschriftet. Somit liefert dieser Aufruf als R¨
uckgabewert true und die Markierung [pα , p2 , p5 , Z] wird aus der Menge
B gel¨oscht.
64
5.3 Heuristik
Zerteilung*(N1 , N2 , R, T )
(1a) B := {mb | mb wird nicht u
uhrt in T }
¨berf¨
(1b) foreach mb ∈ B
(1c)
if PartnerKannSchalten(mb )
(1d)
B := B \ {mb }
(2)
...
..
.
PartnerKannSchalten(mb )
(i)
foreach q ∈ Q mit mb ∈ K1 (q)
(ii)
if q ∈ Q mit (q, l, q ) ∈ δ
(iii)
return false
(iv)
foreach q ∈ Q mit (q, l, q ) ∈ δ
(v)
if l ∈ PO und mb (l) = 0
(vi)
return false
(vii) return true
Algorithmus 5.15: modifizierter Ausschnitt aus Zerteilung
Beim Aufruf PartnerKannSchalten([pα , p2 , p5 , Z, e]) gibt es ebenfalls genau einen
Zustand, q = q2 , auf den die Bedingung mb ∈ K1 (q) zutrifft. Der Nachfolger von q2 ist
u
¨ber eine Kante mit der Beschriftung Z erreichbar. Diese Nachricht geh¨ort zu den Ausgabekan¨alen PO . Wegen mb (Z) = 1 kann die Komposition im Zustand ([pα , p2 , p5 , Z, e], q2 )
weiterschalten. Der Algorithmus liefert daher true, sodass [pα , p2 , p5 , Z, e] ebenfalls aus
B entfernt wird.
Beim dritten Beispielaufruf, PartnerKannSchalten([pα , p2 , p5 , e]), enth¨alt die Erreichbarkeitsfunktion von Zustand q3 die Markierung mb . Allerdings ist der Ausgabeplatz
G, mit der die Kante zum einzigen Nachfolger von q3 beschriftet ist, in mb nicht markiert.
Der Algorithmus liefert false zur¨
uck und [pα , p2 , p5 , e] bleibt in der Menge B enthalten.
Mit dem modifizierten Algorithmus erreichen wir die angestrebte L¨osung f¨
ur das Beispiel
aus Abbildung 5.10 (Seite 59). Verwendet man f¨
ur den Zerteilungsalgorithmus sowohl
die ver¨anderte Menge B als auch die angepasste Deadlockpr¨
ufung, so erh¨alt man eine
¨
sch¨one“ nebenl¨aufige Laufzeitersetzung, welche die Uberf¨
uhrungen [pα ]
[vα ] und
”
[pβ ]
[vβ ] einschließt.
Die Korrektheit des Zerteilungsalgorithmus bei dieser Modifikation der Menge B ist
durch folgendes Lemma gegeben.
65
5 Nebenl¨aufige Laufzeitersetzungen
Lemma 5.8 Sei Tinst eine instantane Laufzeitersetzung von N1 nach N2 gem¨aß OG =
Rφ , bei der die Vorbereiche der Laufzeitersetzungstransitionen paarweise verschieden
sind. Sei T die Transitionsmenge, die vom modifiziertem Algorithmus Zerteilung*(N1 ,
N2 , R, Tinst ) mit dem modifiziertem Subalgorithmus ZerteilungsSchritt* berechnet
wurde. Wenn in der Komposition aus verbundenen Netz N1 ⊕ T ⊕ N2 und R keine Transition aus T schalten kann, obwohl N1 noch nicht leer ist, dann kann eine Transition
aus N1 schalten oder R kann Nachrichten empfangen/senden.
Beweis:
Angenommen, N1 ist nicht leer und keine Transition aus N1 oder T kann schalten.
Wir k¨onnen die Argumentation aus dem Beweis zu Lemma 5.7 an dieser Stelle zum
großen Teil u
¨bernehmen. So ist nur noch der Fall zu betrachten, dass bereits die Laufzeitersetzungstransitionen t1 , . . . , tn geschaltet haben und die aktuelle Markierung makt
von N1 nicht Vorbereich einer instantanen Transition aus Tinst ist.
•ti eine nicht u
uhrte Markierung. Ist nun makt ∈ B
¨ berf¨
In diesem Fall ist m := makt +
i
so gilt die gesuchte Aussage analog zu Lemma 5.7.
Anderenfalls hat der Aufruf PartnerKannSchalten(m) true zur¨
uckgegeben, sodass
die Markierung m aus B entfernt worden ist. Der Partner R besitzt also von seinem ak¨
tuellen Zustand aus Nachfolgezust¨ande (Zeilen i–iii). Die Uberf¨
uhrung zu den Nachfolgezust¨anden ist sichergesellt, weil die ben¨otigten Nachrichten (Ausgabekan¨ale des offenen
¨
Workflownetzes) vorhanden sind. Dies ist durch die Uberpr¨
ufung in den Zeilen iv–vii
sichergestellt.
Wenn N1 nicht leer ist und keine Transition aus T aktiviert ist, kann somit eine Transition aus N1 schalten oder R kann Nachrichten empfangen/senden.
Der Korrektheitsbeweis des Gesamtalgorithmus, Satz 5.6, beh¨alt f¨
ur die beiden vorgestellten Heuristiken seine G¨
ultigkeit. In der Argumentation des Beweises kann das
Lemma 5.5 durch das Lemma 5.7 und Lemma 5.8 ersetzt werden.
5.4 Gr¨
oßenreduktion durch nebenl¨
aufige
Laufzeitersetzungen
Im diesem Kapitel haben wir einen Algorithmus angegeben, der die Laufzeitersetzungstransitionen einer instantanen Laufzeitersetzung durch iteratives Zerteilen in kleinere,
nebenl¨aufige Transitionen trennt. Zwei heuristische Ans¨atze helfen, die Transitionen
66
5.4 Gr¨oßenreduktion durch nebenl¨aufige Laufzeitersetzungen
noch besser aufteilen zu k¨onnen. Im letzten Abschnitt erl¨autern wir nun den Vorteil,
der sich aus der Anwendung dieser Algorithmen ergibt.
Wir zeigen, dass die die erzeugte nebenl¨aufige Laufzeitersetzung T wesentlich kleiner
ist als die instantane Laufzeitersetzung Tinst , die der Zerteilungsalgorithmus als Eingabe
erh¨alt. Die m¨oglichen Ersetzungsschritte gehen dabei nicht verloren – jede Laufzeitersetzungstransition von Tinst l¨asst sich als Summe von Transitionen aus T darstellen.
Abbildung 5.16 zeigt ein offenes Workflownetz, bei dem die Laufzeitersetzung mit einer Kopie von sich durch exponentiell viele instantane Laufzeitersetzungstransitionen
m¨oglich ist, in Bezug auf die Gr¨oße des Netzes. Als Strategien sind alle Strategien des
Netzes zugelassen.
N1 = N2
p0
a1
...
a2
an
...
b1
...
b2
bn
pf
Endmarkierung ist [pf ]
Abbildung 5.16: exponentiell viele instantane Laufzeitersetzungstransitionen
Dieses Netz enth¨alt 2n + 2 innere Pl¨atze und n + 2 Transitionen. Die gestrichelten Pfeile
in der Abbildung deuten an, dass n nebenl¨aufigen Transitionen verschiedene Eingaben
verarbeiten und Ausgaben erzeugen. Es gibt offenbar mindestens 2n + 2 erreichbare
Markierungen. Jede dieser Markierungen von N1 kann zur Laufzeit instantan in die
gleiche Markierung in N2 u
uhrt werden. Damit enth¨alt die vollst¨andige instantane
¨berf¨
Laufzeitersetzung Tinst mindestens 2n + 2 Transitionen.
Es gibt f¨
ur dieses Beispiel eine offensichtlich viel kleinere nebenl¨aufige Laufzeitersetzung
T . Sie entspricht der Identit¨at der inneren Pl¨atze, das bedeutet, f¨
ur jeden inneren Platz
von N1 gibt es eine Transition in den gleichen Platz des Zielnetzes. Alle instantanen Lauf-
67
5 Nebenl¨aufige Laufzeitersetzungen
zeitersetzungstransitionen k¨onnen als Summe der entsprechenden nebenl¨aufigen Transitionen dargestellt werden. Die Gr¨oße von T ist so mit 2n + 2 Transitionen exponentiell
kleiner als Tinst .
Wesentlich f¨
ur die Gr¨oßenreduktion ist am Ende des Zerteilungsalgorithmus das L¨oschen
all jener Laufzeitersetzungstransitionen, die als Summe anderer dargestellt werden k¨onnen.
Anderenfalls w¨are das Ergebnis noch gr¨oßer als die urspr¨
ungliche instantane Laufzeitersetzung.
Gr¨oßenreduktion tritt nicht nur bei der Ersetzung identischer Netze auf. Im Abschnitt 5.1
(Seite 48ff) haben wir die Laufzeitersetzung der Netze zweier Getr¨ankeautomaten (Abbildung 5.3) betrachtet. Als zu bearbeitende, instantane Laufzeitersetzung wurde eine
Transitionsmenge mit 11 Transitionen festgelegt (Tabelle 5.4). Durch die Anwendung
unseres Algorithmus konnte die Zahl auf 8 nebenl¨aufige Transitionen reduziert werden
(Tabelle 5.6).
68
6 Fazit
In dieser Arbeit wurde ein theoretisches Konzept f¨
ur die Laufzeitersetzung von Gesch¨afts¨
prozessen in Form offener Workflownetze eingef¨
uhrt. Ubertragen
auf reale Anwendungen
lassen sich mithilfe der Laufzeitersetzungen aktive Gesch¨aftsprozesse in andere (neue)
Gesch¨aftsprozesse u
uhren. Auf diese Weise k¨onnten zum Beispiel laufende Vertr¨age
¨berf¨
einer Firma verkauft werden an eine andere Firma, wobei die Interaktion mit den Kunden
schrittweise u
¨ bergeben wird.
Unser Konzept sieht die freie Wahl der zugrundliegenden Strategien f¨
ur die beteiligten
Kommunikationspartner vor. Damit lassen sich f¨
ur verschiedene Kundengruppen individuelle Laufzeitersetzungen berechnen.
Auf der Modellebene erweitert die Laufzeitersetzung den Begriff der Austauschbarkeit
von Gesch¨aftsprozessen, welcher in verschiedenen Arbeiten bereits untersucht worden
ist. Die Laufzeitersetzung zweier offener Workflownetze ist definiert als eine Menge von
Transitionen, die zur Laufzeit Marken vom Ausgangs- in das Zielnetz u
uhren. Ziel
¨ berf¨
dieser Ersetzung ist, dass ein Serviceautomat, welcher als Interaktionspartner f¨
ur das
Ausgangsnetz dient, ebenso mit dem verbundenen Netz aus Ausgangsnetz, Zielnetz und
Laufzeitersetzung kommunizieren kann. Die Startmarkierung des verbundenen Netzes
liegt im Ausgangsnetz, w¨ahrend die Endmarkierung nur Pl¨atze des Zielnetzes belegt.
Bei der Laufzeitersetzung ist garantiert, dass das verbundene Netz mit dem Partner
deadlockfrei interagieren kann. Auf diese Weise wird der durch das Ausgangsnetz beschriebene Gesch¨aftsprozess zur Laufzeit durch den Gesch¨aftsprozess des Zielnetzes ersetzt.
Voraussetzung f¨
ur die Erzeugung von Laufzeitersetzungen ist, dass es sich um beschr¨ankte Netze handelt sowie dass die Interaktion mit den Partnern eine beschr¨ankte Kommunikation darstellt. Zus¨atzlich wird gefordert, dass die Netze keine leeren Transitionen im
inneren Netz enthalten. Als Menge der zu ber¨
ucksichtigenden Strategien der Interaktionspartner darf eine beliebige Untermenge der Strategien des Ausgangsnetzes angegeben
werden. Diese Strategiemenge wird dabei als annotierter Serviceautomat gegeben.
Wie in dieser Arbeit gezeigt, kann die Laufzeitersetzung instantan, also in einem einzigen Schritt, oder aber nebenl¨aufig, in mehreren Teilschritten, erfolgen. Die grundlegende
Idee der instantanen Laufzeitersetzungen f¨
ur offene Workflownetze basiert auf der Lauf-
69
6 Fazit
zeitersetzung von Serviceautomaten, welche in einer vorausgegangenen Studienarbeit
vorgestellt worden ist. Es konnte in der vorliegenden Arbeit ein Algorithmus angegeben und in seiner Korrektheit formal bewiesen werden, welcher die eindeutig definierte,
vollst¨andige instantane Laufzeitersetzung zweier offener Workflownetze gem¨aß einer vorgebenenen Menge von Strategien berechnet.
Der Schwerpunkt der Arbeit liegt auf der Berechnung nebenl¨aufiger Laufzeitersetzungen.
Es wurde der Algorithmus Zerteilung angegeben, welcher die Transitionen einer gegebenen instantanen Laufzeitersetzung in m¨oglichst kleine Teiltransitionen zerteilt. Wir
konnten zeigen, dass die Gr¨oße einer nebenl¨aufigen Laufzeitersetzung exponentiell kleiner sein kann als eine instantane Laufzeitersetzung, wenngleich sich alle Transitionen der
instantanen Laufzeitersetzung als Summe nebenl¨aufiger Laufzeitersetzungstransitionen
darstellen lassen. Dieser Zerteilungsalgorithmus sowie zwei modifzierte Varianten davon
wurden formal in ihrer Korrektheit bewiesen. Die Modifikationen beschreiben heuristische Ans¨atze, welche der Berechnung noch sch¨onerer“ Ergebnisse dienen.
”
Mit dem in Kapitel 4 vorgestellten Algorithmus InstantaneLE l¨asst sich stets die
vollst¨andige instantane Laufzeitersetzung finden. Dabei kann, wie wir gesehen haben, die
Anzahl der Laufzeitersetzungstransitionen exponentiell groß in Bezug auf die beteiligten
Netze sein. Es ist durchaus denkbar, dass ganz ein anderer Ansatz – der nicht auf den
¨
instantanen Uberf¨
uhrungen basiert – zur Erzeugung von Laufzeitersetzungen verwendet
werden kann.
Die heuristischen Ans¨atze in Abschnitt 5.3 zur Verbesserung der nebenl¨aufigen Laufzeitersetzungen bieten Raum f¨
ur weitere Untersuchungen. Die Frage, inwiefern sich die
Reihenfolge der Zerteilungsschritte im Algorithmus Zerteilung auf die Gr¨oße der erzeugten, nebenl¨aufigen Laufzeitersetzung auswirkt, kann ebenfalls Gegenstand weiterer
Arbeiten auf diesem Gebiet sein.
70
Literaturverzeichnis
[AAA+ 06]
Alexandre Alves, Assaf Arkin, Sid Askary, Ben Bloch, Francisco Curbera, Yaron Goland, Neelakantan Kartha, Sterling, Dieter K¨onig, Vinkesh
Mehta, Satish Thatte, Danny van der Rijn, Prasad Yendluri, and Alex
Yiu. Web services business process execution language version 2.0. OASIS
Committee Draft, May 2006.
[Aal98]
W.M.P. van der Aalst. The Application of Petri Nets to Workflow Management. The Journal of Circuits, Systems and Computers, 8(1):21–66,
1998.
[BK06]
F. Breugel and M. Koshkina.
Models and verification of BPEL.
http://www.cse.yorku.ca/ franck/research/drafts/tutorial.pdf, 2006.
[GGKS02]
Karl D. Gottschalk, Stephen Graham, Heather Kreger, and James
Snell. Introduction to web services architecture. IBM Systems Journal,
41(2):170–177, 2002.
[Gla01]
R. van Glabbeek. The linear time – branching time spectrum i: The semantics of concrete, 2001.
[HDvdA+ 05] Jan Hidders, Marlon Dumas, Wil M. P. van der Aalst, Arthur H. M. ter
Hofstede, and Jan Verelst. When are two workflows the same? In CATS
’05: Proceedings of the 2005 Australasian symposium on Theory of computing, pages 3–11, Darlinghurst, Australia, Australia, 2005. Australian
Computer Society, Inc.
[HSS05]
Sebastian Hinz, Karsten Schmidt, and Christian Stahl. Transforming
BPEL to Petri Nets. In Wil M. P. van der Aalst, B. Benatallah, F. Casati,
and F. Curbera, editors, Proceedings of the Third International Conference
on Business Process Management (BPM 2005), volume 3649 of Lecture Notes in Computer Science, pages 220–235, Nancy, France, September 2005.
Springer-Verlag.
71
Literaturverzeichnis
[Lis07]
Nannette Liske. Laufzeitersetzbarkeit von Services.
Humboldt-Universit¨at zu Berlin, April 2007.
[LMSW06]
Niels Lohmann, Peter Massuthe, Christian Stahl, and Daniela Weinberg.
Analyzing interacting BPEL processes. In Business Process Management,
pages 17–32, 2006.
[LMW07]
Niels Lohmann, Peter Massuthe, and Karsten Wolf. Operating guidelines
for finite-state services. In Jetty Kleijn and Alex Yakovlev, editors, 28th
International Conference on Applications and Theory of Petri Nets and
Other Models of Concurrency, ICATPN 2007, Siedlce, Poland, June 2529, 2007, Proceedings, volume 4546 of Lecture Notes in Computer Science,
pages 321–341. Springer-Verlag, 2007.
[Loh08]
Niels Lohmann. A feature-complete Petri net semantics for WS-BPEL 2.0.
In Marlon Dumas and Reiko Heckel, editors, Web Services and Formal
Methods, Forth International Workshop, WS-FM 2007 Brisbane, Australia, September 28-29, 2007, Proceedings, volume 4937 of Lecture Notes in
Computer Science, pages 77–91. Springer-Verlag, 2008.
[Mar03]
Axel Martens. Verteilte Gesch¨aftsprozesse - Modellierung und Verifikation
mit Hilfe von Web Services. Dissertation, Humboldt-Universit¨at zu Berlin, Mathematisch-Naturwissenschaftliche Fakult¨at II, 2003. erschienen in
WiKi: Stuttgart, Berlin & Paris.
[Mil71]
Robin Milner. An algebraic definition of simulation between programs.
Technical report, Stanford, CA, USA, 1971.
[Mil89]
Robin Milner. Communication and Concurrency. Prentice–Hall, 1989.
[MRS05]
Peter Massuthe, Wolfgang Reisig, and Karsten Schmidt. An Operating
Guideline Approach to the SOA. Annals of Mathematics, Computing &
Teleinformatics, 1(3):35–43, 2005.
[MS05]
Peter Massuthe and Karsten Schmidt. Operating Guidelines - an
Automata-Theoretic Foundation for the Service-Oriented Architecture. In
Kai-Yuan Cai, Atsushi Ohnishi, and M.F. Lau, editors, Proceedings of the
Fifth International Conference on Quality Software (QSIC 2005), pages
452–457, Melbourne, Australia, September 2005. IEEE Computer Society.
[Pap01]
Mike P. Papazoglou. Agent-oriented technology in support of e-business.
Commun. ACM, 44(4):71–77, 2001.
72
Studienarbeit,
Literaturverzeichnis
[RCS+ 08]
Seung Hwan Ryu, Fabio Casati, Halvard Skogsrud, Boualem Benatallah,
and R´egis Saint-Paul. Supporting the dynamic evolution of web service
protocols in service-oriented architectures. TWEB, 2(2), 2008.
[Rei82]
Wolfgang Reisig. Petrinetze, Eine Einf¨uhrung. Springer, 1982.
[Ric02]
Wolf Richter. Spezifikation und Implementation organisations¨
ubergreifender Gesch¨aftsprozesse mit Petrinetzen. Diplomarbeit, HumboldtUniversit¨at zu Berlin, 2002.
[Sch00]
Karsten Schmidt. LoLA: A Low Level Analyser. In Mogens Nielsen and
Dan Simpson, editors, Application and Theory of Petri Nets, 21st International Conference (ICATPN 2000), volume 1825 of Lecture Notes in
Computer Science, pages 465–474. Springer-Verlag, June 2000.
[Sch05]
Karsten Schmidt. Controllability of Open Workflow Nets. In J¨org Desel
and Ulrich Frank, editors, Enterprise Modelling and Information Systems
Architectures, volume P-75 of Lecture Notes in Informatics (LNI), pages 236–249, Bonn, 2005. Entwicklungsmethoden f¨
ur Informationssysteme
und deren Anwendung (EMISA, RWTH Aachen), K¨ollen Druck+Verlag
GmbH.
[SMB08]
Christian Stahl, Peter Massuthe, and Jan Bretschneider. Deciding substitutability of services with operating guidelines. Informatik-Berichte 222,
Humboldt-Universit¨at zu Berlin, April 2008.
73
Document
Kategorie
Seele and Geist
Seitenansichten
1
Dateigröße
676 KB
Tags
1/--Seiten
melden