close

Anmelden

Neues Passwort anfordern?

Anmeldung mit OpenID

Abstract-State-Machines 1 Motivation 2 Was ist eine Abstract State

EinbettenHerunterladen
Abstract-State-Machines
1
Motivation
2
Was ist eine Abstract State Machine
3
Semantik
4
Turbo-ASMs
5
Multi-Agent ASMs
Was ist eine ASM?
Eine Abstract State Machine besteht aus einem Universum - einer
Menge von Objekten, einer Menge von Funktionen innerhalb
dieses Universum und einer endlichen Menge von Regeln, die
angeben, wie Funktionen zu modifizieren sind.
Dabei werden die Funktionen unterschieden, in
◮
◮
static functions: ändern sich während der Ausführung der
ASM nicht
dynamic functions: ändern sich während der Ausführung der
ASM
◮
◮
◮
◮
2
controlled functions: werden nur durch die ASM selbst
geändert und nur von ihr gelesen
in functions: werden nicht durch die ASM, sondern durch die
Umgebung geändert
shared functions: werden sowohl durch die ASM als auch
durch die Umgebung geändert
out functions: werden nur von der ASM geändert und nur von
der Umgebung gelesen
Ausführung
Die Ausführung einer ASM beginnt bei einem Startzustand, in dem
alle statischen Funktionen festgelegt sind, und in dem alle
dynamischen Funktionen irgendwelche Anfangswerte haben.
Danach arbeitet die ASM schrittweise. In jedem Schritt werden alle
Regeln der ASM gleichzeitig angewandt, wodurch der Zustand
sich verändert. Auf dem dann neuen Zustand werden dann wieder
alle Regeln angewandt, usw...
Was die einzelnen Regeln bewirken, und wie sie den Zustand
verändern, wird weiter unten beschrieben.
Eine Termination ist in der formalen Semantik nicht vorgesehen,
meistens wird sie durch einen sich nicht mehr ändernden Zustand
dargestellt.
3
Updates
Die dynamischen Funktionen können, wie bereits erwähnt, durch
die Ausführung einer ASM geändert werden. Die Funktionen
arbeiten dann ähnlich wie Arrays in Programmiersprachen und
speichern für jede Argumentbelegung ein Objekt.
Die Updates, die in einem Schritt erfolgen, dürfen sich nicht
widersprechen, also eine Funktion an der gleichen Stelle mit
verschiedenen Werten updaten.
Ein Update wird durch eine Regel der Form
f (t1 , . . . , tn ):=t
beschrieben. t , t1 , . . . , tn sind dabei Terme.
4
Das Universum
Das Universum, genannt U , besteht bei einer ASM immer
mindestens aus den Elementen true , false und undef .
undef ist das undefinierte Element und wird implizit für alle nicht
vorgegebenen Funktionsbelegungen angenommen.
Im Universum befindet sich außerdem die sogenannte Reserve die
beliebig viele Elemente enthält, die nirgends sonst vorkommen.
5
Signatur
Zu jeder ASM gehört eine Signatur, die eine Menge von
Funktionssymbolen f1 , . . . , fn definiert. Jedem Funktionssymbol
wird ausserdem eine Stelligkeit zugeordnet. Die Stelligkeit 0 ist
dabei durchaus erlaubt, die Funktionen haben dann keine
Argumente.
Da bei einer ASM alle Funktionen aus dem Universum in das
Universum abbilden, muss nicht angegeben werden, aus welchen
Mengen Argumente und Funktionswerte stammen.
Die Signatur legt fest welche Funktionen statisch, welche
controlled, in, out oder shared sind, indem die Funktionssymbole in
vier disjunkte Mengen aufgeteilt werden.
6
Signatur
Die Signatur legt aber nicht fest, wie die statischen Funktionen
vorbelegt sind, wodurch sich die gleiche ASM auf verschiedene
Datenrepräsentationen anwenden lässt.
In jeder ASM sind die beiden Funktionen ¬ und ∧ als statische
Funktionen vorhanden, die für die Elemente true und false das
Offensichtliche tun, und für alle anderen Elemente undef
zurückgeben. Diese beiden Funktionen werden in der Signatur
üblicherweise nicht mit aufgeführt.
7
Algebren
Es sei eine Signatur Σ gegeben. Eine Algebra AΣ zur Signatur Σ
besteht aus
◮
der Trägermenge A , d.h. allen Elementen, die im Universum
vorkommen, und
◮
für jedes Funktionssymbol f eine konkrete Funktion
fA : A × . . . × A → A
Dabei muss die Anzahl der Argumente der konkreten Funktion
immer mit der in der Signatur festgelegten Stelligkeit des
Funktionssymboles übereinstimmen.
8
Terme
Terme sind induktiv definiert:
◮
Jedes 0-stellige Funktionssymbol ist ein Term
◮
f (t1 , . . . , tn ) ist ein Term, wenn f ein Funktionssymbol der
Stelligkeit n ist.
◮
Einige Regelkonstrukte definieren lokale Variablen, die jeweils
ein Element aus U enthalten. Diese Variablen sind ebenfalls
Terme.
◮
Sonst ist nichts ein Term.
Terme lassen sich innerhalb einer konkreten Algebra auswerten.
Dazu werden, von innen nach aussen, die konkreten Funktionen
der Algebra ausgewertet.
Da die Funktionssymbole des Terms je nach Algebra mit
verschiedenen Funktionen belegt sind, ist der Wert eines Term je
nach Algebra verschieden. Der Wert des Terms t in der Algebra A
wird mit tA bezeichnet.
9
Trägermenge der Algebren
Wie bereits erwähnt, arbeitet die ASM indem ihr Zustand durch
Updates verändert wird. Jeder Zustand wird dabei durch eine
Algebra repräsentiert.
Durch die Anwendung von Updates wird diese Algebra dann
verändert, so dass sich eine neue Algebra ergibt, die dann zum
neuen Zustand wird. Die Updates sind dabei so gestaltet, dass die
Trägermengen der neuen und der alten Algebra gleich sind.
Diese Trägermenge, die von allen Algebren benutzt wird, ist das
Universum der ASM.
10
Regeln
Die Regeln einer ASM werden üblicherweise als Code angegeben.
◮
◮
f (t1 , t2 , . . . , tn ):=t0 : Zuweisung, die Funktion wird geändert.
◮
if t1 = t2 then R1 : Bedingung, Regel R1 wird nur
ausgeführt, falls die Terme t1 und t2 im aktuellen Zustand zum
gleichen u ∈ U ausgewertet werden.
◮
···
11
skip : tut einfach nichts
R1 par R2 : Parallele Ausführung, Regeln R1 und R2 werden
gleichzeitig angewandt.
Regeln (Fortsetzung)
···
◮
···
12
forall x with φ do R1 : Führt Regel R1 für alle x ∈ U aus, für
die im akuellen Zustand φ(x ) = true .
Ist das Universum endlich, so ist dies äquivalent zu
if φ(u1 ) then R1 x =u
1
par
···
par
if φ(un ) then R1 x =u
n
mit je einer Zeile für jedes ui ∈ U , das dann in R1 die Variable
x ersetzt.
Regeln (Fortsetzung)
···
◮
◮
choose x with φ do R1 : Führt Regel R1 für ein zufälliges
x ∈ U aus, für das im aktuellen Zustand φ(x ) = true .
import x do R1 : führt Regel R1 aus, während die Variable x
auf ein neues Objekt zeigt.
Die Menge der gültigen Regeln ist also ebenfalls induktiv definiert.
Falls sich aus der Anwendung der Regeln wiedersprüchliche
Updates ergeben, werden alle Updates ignoriert, was
gleichbedeutend mit der Ausführung der skip Regel ist.
13
Mini-Beispiel
Eine ASM, die die Wurzelfunktion berechnet, könnte zum Beispiel
so aussehen:
ergebnis
:= sqrt(eingabe)
eingabe wäre hier eine in-Funktion, die jeweils die
Benutzereingaben enthält. ergebnis entsprechend eine
out-Funktion, durch die das Ergebnis der Berechnung dem
Benutzer dargestellt wird.
Bei geeigneter Belegung der sqrt Funktion zu Beginn der
Ausführung erfüllt diese ASM die Aufgabe.
14
Mini-Beispiel 2
Die folgende ASM leistet das selbe, wenn die mul Funktion die
Multplikation auf ist.
choose x with mul(x, x) = eingabe do
ergebnis := x
Da das choose nur x wählt, die die Bedingung erfüllen, wird die
Wurzel von eingabe korrekt ausgegeben. Wie man hier allerdings
schon sieht, sind ASMs nicht im Allgemeinen ausführbar.
15
Semantik: Algebren als Stati
Jeder Status S einer ASM ist eine Algebra mit der Signatur Σ der
ASM.
Jeder Schritt einer ASM erzeugt eine Menge von Updates der
Form f (u1 , . . . , un ):=u0 ( .u0 , u1 , . . . un ∈ U ) Dieses Update wird auf
der Funktion f im Zustand S ausgeführt, die im folgenden fS
genannt wird.
Nach diesem Update der Funktion fS ergibt sich eine neue
Funktion fS ′ gemäß
fS ′ (x1 , . . . , xn ) =
16
u0
fS (x1 , . . . , xn )
falls x1 = u1 ∧ · · · ∧ xn = un
sonst
Semantik: Algebren als Stati (fort.)
Der Status S geht dadurch in einen neuen Status S ′ über, der
wieder eine Algebra der selben Signatur Σ sein muss, da ein
Update nur Funktionswerte ändert, aber keine neuen Funktionen
erzeugt, noch die Anzahl der Argumente verändern kann. Die
Trägermengen der beiden Algebren bleiben dabei gleich, da ein
Update keine neuen Elemente erzeugen kann.
17
Semantik: Ausführung einer ASM
Eine ASM M wird ausgeführt, indem zuerst ein Anfangszustand S
angenommen wird. In jedem Schritt werden dann durch die Regeln
die Menge der Updates ∆(M , S ) bestimmt, die dann auf die
Funktionen des Status S angewendet werden, wodurch ein neuer
Status S ′ erzeugt wird, der dann im nächsten Schritt genutzt wird.
Wie aus den Regeln die Update-Menge bestimmt wird, ist im
folgenden für die einzelnen Regelelemente dargestellt.
Falls in der Update-Menge mehrere Updates auf die gleiche
Position vorkommen, die sich widersprechen, so wird der ganze
Schritt verworfen und der Zustand ändert sich nicht. Man nennt
solche Update-Mengen inkonsistent.
Je nachdem, in welcher Umgebung die ASM eingebettet ist,
werden zwischen den Schritten auf S ′ noch Updates aus der
Umgebung durchgeführt, die shared- und in-Funktionen ändern
können.
18
Widersprüchliche Updates
Eine Updatemenge ist genau dann inkonsistent, wenn ein Paar
von Updates (Up1 , Up2 ) der Form
Up1 = f (u1 , . . . , un ):=x
Up2 = f (u1 , . . . , un ):=y
und
x
y
in der Updatemenge existiert.
Dies ist der Fall, wenn auf die selbe Position der gleichen Funktion
zwei verschieden Elemente des Universums zugewiesen werden.
19
if
Eine bedingte Regel der Form
if t1 = t2 then R1
hat in einem Status S die Bedeutung R1 , falls t1 S = t2 S , oder
skip falls t1 S t2 S .
Die Gleichheitsrelation bezieht sich hierbei auf den Wert der Terme
und ist keine Funktion innerhalb des Universums. Zwei Terme sind
genau dann gleich, wenn sie das selbe Element bezeichnen.
20
Regelvariablen
In den Konstrukten forall und choose werden Regelvariablen
verwendet. Sie sind nicht Bestandteil des Status’ und gelten
jeweils nur für eine einzige Regel.
Je nach verwendetem Konstrukt, ergeben sich kein, einer oder
mehrere Werte für die Regelvariable. Diese Werte werden nun in
die Regel eingesetzt und die dann resultierende Regel(n)
ausgeführt.
Auf den folgenden Folien wird das Konzept für die beiden
fraglichen Konstrukte noch einmal detailliert erläutert.
21
forall
Eine Regel der Form
forall x with φ do R1
hat die selbe Bedeutung, wie die Regel
if φ(x ) = true then R1
für jede Belegung der Regelvariablen x mit Elementen des
Universums ohne die Reserve einmal angewandt.
22
choose
Eine Regel der Form
choose x with φ do R1
hat die selbe Bedeutung, wie die Regel R1 für eine Belegung der
Regelvariablen x angewandt, für die φ(x ) = true gilt.
Gibt es keine solche Belegung, dann ist die Regel
gleichbedeutend mit skip .
23
Beispiel: Quersumme
ergebnis := ergebnis + mod (zahl , 10)
zahl := div (zahl , 10)
Die Funktionen mod und div sind dabei so zu wählen, dass sie die
ganzzahlige Division mit dem 2. Argument durchführen.
24
Beispiel: Faktorisierung
choose f with divisor (f , zahl ) ∧ prime (f )
ergebnis := append (ergebnis , f )
zahl := zahl /f
Dieser Algorithmus ist so noch nicht direkt in eine
Programmiersprache umsetzbar, da z. B. die Funktion prime nicht
trivial zu implementieren ist. append sollte die entsprechende
Listenoperation durchführen.
Statt choose kann hier nicht forall genutzt werden, da sonst
die Zuweisung auf zahl zu einer inkonsistenten Updatemenge
führt. Die Konstruktion mit choose ist außerdem recht abstrakt,
da sie den Programmierer des Algorithmus’ nicht darauf festlegt,
welcher Primfaktor zuerst betrachtet werden soll.
25
Beispiel: Primzahltest
forall p with p < zahl
if divisor (p , zahl ) then
isPrime := false
Sinnigerweise sollte isPrime am Anfang auf true stehen.
Der Algorithmus funktioniert zwar, ist allerdings scheinbar
ineffizient. Dies könnte man (unintuitiverweise) durch eine
geschickte Wahl der Funktion < ändern. Gibt z. B. < nur dann true
zurück, wenn ihr erstes Argument eine Primzahl ist und kleiner als
die Wurzel des zweiten Arguments, so werden weniger
Möglichkeiten untersucht.
Die Funktionsnamen in einer ASM sollten allerdings ihrer intuitiven
Funktionalität entsprechen.
26
Beispiel: Matrizenmultiplikation
Gegeben seien zwei quadratische Matrizen A und B , jeweils der
Größe n. Eine Multiplikation C = A · B ist dann:
forall col with 0 < col ≤ n
forall row with 0 < row ≤ n
C (row , col ) = extractRow (A , row ) · extractCol (B , col )
Diese ASM sagt nichts über die Representation der Matrizen aus,
noch über die Implementierung des Vektorprodukts. Allerdings
schließt sie effizientere Algorithmen aus, die Teile des Produktes
wiederverwenden.
27
Beispiel: Labyrinth
28
Beispiel: Labyrinth
Gegeben sei ein Labyrinth, das freie Felder, Mauern, Ausgänge
und ein Wesen enthält, das den Ausgang erreichen will. Die
folgende ASM ermittelt, ob diese Aufgabe lösbar ist:
forall position with ¬wall (position)∧
(∃x . adjacent (position, x ) ∧ reachable (x )) ∧
¬reachable (position)
reachable (position) := true
if exit (position) then
possible := true
Je nachdem, wie die Funktionen wall und adjacent gewählt
werden, löst dieser Algorithmus nicht nur die „normalen“
Labyrinthe im 2-Dimensionalen, sondern in beliebig irrwitzigen
Graphen.
Diese Möglichkeit Algorithmen abstrakt zu definieren, ohne sie auf
eine konkrete Datenstruktur zu beschränken ist eine
herausragende Stärke von ASMs.
29
Turbo-ASMs
Turbo-ASMs können benutzt werden, um ASMs hierarchisch zu
strukturieren. Hierarchisch in so fern, als dass innerhalb eines
ASM-Schritts eine Unter-ASM ausgeführt wird, deren
Mikro-Schritte alle innerhalb des einen Makro-Schrittes der
umgebenden ASM ausgeführt werden.
Dazu werden zwei neue Konstrukte eingeführt:
30
◮
R1 seq R2 : Sequentielle Ausführung, erst wird R1 und danach
R2 angewandt.
◮
iterate R1 : Wiederholte Ausführung, es wird solange R1
angewandt, bis der Status sich nicht mehr ändert.
seq
Eine Regel der Form
R1 seq R2
hat den gleichen Effekt, wie zuerst Regel R1 und dann Regel R2
angewandt, es sei denn, R1 liefert eine inkonsistente
Update-Menge.
Falls R1 eine inkonsistente Update-Menge liefert, wird die
Ausführung nach R1 abgebrochen und der Zustand ändert sich
dementsprechend nicht.
Gerade bei mehr als zwei Regeln wird oft eine auf Einrückung
basierende Syntax verwendet:
seq
R1
R2
31
iterate
Eine Regel der Form
iterate R1
hat den gleichen Effekt, wie die Regel R1 unendlich oft angewandt.
Das bedeutet, falls die Regel R1 irgendwann einmal keine
Statusänderung mehr hervorruft, kann die Ausführung
abgebrochen werden.
Falls jedoch R1 in irgendeinem Schritt eine inkonsistente
Update-Menge liefert, gilt dies für die ganze Regel, und der Status
wird nicht geändert.
32
Auswertung von Turbo-ASMs
Eine Turbo-ASM Regel auszuführen, braucht nur einen
Makro-Schritt. Innerhalb dieses Makro-Schrittes werden die durch
die Regeln festgelegten Mikro-Schritte ausgeführt.
Das bedeutet insbesondere, dass sich während der Ausführung
die Werte von Funktionen nicht aufgrund der Umgebung ändern.
33
Multi-Agent ASMs
Eine asynchrone Multi-Agent ASM ist durch eine Menge Agents
von Paaren (a , ASM (a )) definiert. Jeder Agent a führt dabei die
ihm zugeordnete ASM ASM (a ) aus. Sowohl die Menge Agents als
auch die Funktion ASM (a ) sind dynamisch, können sich also
während der Ausführung ändern.
Es wird eine spezielle Funktion self eingeführt, die jeweils den
ausführenden Agenten zurückgibt. Durch sie lässt sich einfach ein
Agent-lokaler Status realisieren, indem allen lokalen Funktionen
self als erstes Argument mitübergeben wird. Meist wird dieses
Argument allerdings nicht explizit angegeben.
34
Ausführung
Eine Ausführung einer solchen ASM lässt sich durch eine Menge
M von Schritten beschreiben. Diese Menge muss den folgenden
Bedingungen genügen:
◮
Ordnung: Die Schritte eines einzelnen Agenten laufen
hintereinander ab und sind durch < geordnet
◮
endliche Vergangenheit: Jeder Schritt hat nur endlich viele
Vorgänger {m′ |m′ < m} ist endlich für alle m ∈ M
◮
kohärent: Jedes endliche Startsegment X von Schritten (also
Mengen für die gilt: m ∈ X , m′ < m ⇒ m′ ∈ X ) entspricht
eindeutig einem Status σ(X ), der für jedes maximale Element
m ∈ X gleich dem Ergebnis der Anwendung von m auf
σ(X \{m}) ist.
Jede konkrete Linearisierung eines endlichen Startsegments X
führt zum selben Ergebnis.
35
Kohärenz
A und B seien zwei unterschiedliche Elemente des Universums:
ASM A :
v := A
ASM B :
v := B
Es gibt zwei gültige Schrittfolgen für diese Kombination: A , A , A , . . .
und B , B , B , . . .. Andere Schrittfolgen sind nicht möglich, da sonst
die Kohärenzbedingung verletzt wäre.
Es ist also nicht festgelegt, welcher Agent wann ausgeführt wird,
aber es wird verhindert, dass die vereinigte Updatemenge zweier
möglicherweise parallel laufender Schritte durch die Parallelität
inkonsistent wird.
36
Document
Kategorie
Gesundheitswesen
Seitenansichten
4
Dateigröße
91 KB
Tags
1/--Seiten
melden