Formale Beschreibung von Auktionstypen zum … · B A C H E L O R A R B E I T Formale Beschreibung...

B A C H E L O R A R B E I T

Formale Beschreibung von Auktionstypen zum automatisierten Reasoning durch Agenten

von Benjamin Brandmüller

eingereicht am 30.09.2011 beim Institut für Angewandte Informatik

und Formale Beschreibungsverfahren des Karlsruher Instituts für Technologie

Referent: Prof. Dr. Rudi Studer Betreuer: Sebastian Rudolph

Heimatanschrift: Studienanschrift: Kastanienring 34 Neisser Str. 12 55286 Wörrstadt 76139 Karlsruhe

Ich versichere hiermit wahrheitsgemäß, die Arbeit bis auf die dem Aufgabensteller

bereits bekannte Hilfe selbstständig angefertigt, alle benutzten Hilfsmittel vollständig

und genau angegeben und alles kenntlich gemacht zu haben, was aus Arbeiten anderer

unverändert oder mit Abänderungen entnommen wurde.

XBenjamin Brandmüller

Autor

Inhaltsverzeichnis 1. Einleitung ..................................................................................................................................... 5

2. Grundlagen ................................................................................................................................... 5

2.1. General Game Playing (GGP) ................................................................................................. 5

2.2. Game Description Language (GDL) ....................................................................................... 6

2.2.1. Relationen ...................................................................................................................... 6

2.2.2. Definitionen ................................................................................................................... 8

2.2.3. Erweiterung der Definitionen ...................................................................................... 10

2.3. Erweiterungen der GDL ....................................................................................................... 11

2.3.1. Stochastische Spiele in GDL ......................................................................................... 11

2.3.2. Market Specification Language (MSL) ......................................................................... 12

2.3.3. Gala .............................................................................................................................. 12

2.3.4. GDL for Incomplete Information (GDL II) ..................................................................... 13

2.4. Auktionstypen ..................................................................................................................... 15

2.4.1. Höchstpreisauktion ...................................................................................................... 16

2.4.2. Vickrey-Auktion ............................................................................................................ 16

2.4.3. Holländische Auktion ................................................................................................... 16

2.4.4. Englische Auktion ......................................................................................................... 17

2.4.5. Call Auction .................................................................................................................. 17

2.4.6. Continuous Double Auction (CDA) ............................................................................... 17

3. Modellierung in GDL II ............................................................................................................... 18

3.1. Einseitige Auktionen ............................................................................................................ 19

3.1.1. Höchstpreisauktion ...................................................................................................... 19

3.1.2. Vickrey-Auktion ............................................................................................................ 20

3.1.3. Holländische Auktion ................................................................................................... 22

3.1.4. Englische Auktion ......................................................................................................... 24

3.2. Zweiseitige Auktionen ......................................................................................................... 26

3.2.1. Call Auction .................................................................................................................. 26

3.2.2. Continuous Double Auction (CDA) ............................................................................... 28

4. Korrektheitsprüfung der Modelle .............................................................................................. 30

4.1. Höchstpreisauktion ............................................................................................................. 30

4.1.1. Verifikation ................................................................................................................... 30

4.1.2. Validierung ................................................................................................................... 32

4.2. Vickrey-Auktion ................................................................................................................... 33

4.2.1. Verifikation ................................................................................................................... 33

4.2.2. Validierung ................................................................................................................... 34

4.3. Holländische Auktion........................................................................................................... 35

4.3.1. Verifikation ................................................................................................................... 35

4.3.2. Validierung ................................................................................................................... 36

4.4. Englische Auktion ................................................................................................................ 37

4.4.1. Verifikation ................................................................................................................... 37

4.4.2. Validierung ................................................................................................................... 39

4.5. Call Auction .......................................................................................................................... 40

4.5.1. Verifikation ................................................................................................................... 40

4.5.2. Validierung ................................................................................................................... 41

4.6. Continuous Double Auction ................................................................................................ 45

4.6.1. Verifikation ................................................................................................................... 45

4.6.2. Validierung ................................................................................................................... 46

5. Zusammenfassung und Ausblick ................................................................................................ 49

5.1. Umsetzung im Börsenhandel .............................................................................................. 50

5.2. Umsetzung in Internetauktionen ........................................................................................ 50

5.3. Umsetzung bei auktionsähnlichen Methoden .................................................................... 51

5.3.1. Mengentender ............................................................................................................. 51

5.3.2. Zinstender .................................................................................................................... 51

Abbildungsverzeichnis ....................................................................................................................... 51

Literaturverzeichnis............................................................................................................................ 52

1. Einleitung Ziel dieser Bachelorthesis ist es, gängige Auktionstypen in einer formalen Beschreibungssprache zu modellieren, um so die automatisierte Interpretation durch Agenten ohne jegliche menschliche Interaktion zu ermöglichen. Die Korrektheit der Modelle wird anschließend theoretisch geprüft. Die Modellierung erfolgt dabei in der formalen Beschreibungssprache GDL-II, die im Rahmen der Einführung erläutert wird. Insbesondere wird ausführlich auf die GDL eingegangen, die die Basis für die GDL-II ist. Aber auch andere vergleichbare Sprachen werden kurz erläutert. Im Rahmen der Einführung wird zudem Basiswissen zur Auktionstheorie vermittelt, welches für die spätere Validierung der Modelle benötigt wird. Die Bachelorarbeit zeigt, dass alle gängigen Auktionstypen durch die GDL-II beschrieben werden können. Insbesondere der Aspekt asymmetrischer und unvollständiger Information stellte bisher aufgrund der mangelnden Ausdrucksmächtigkeit der GDL ein Hindernis dar, welches nun jedoch mit der GDL-II überwunden werden kann. Abschließend werden die Potenziale der formalen Beschreibung aufgedeckt und mögliche Anwendungsbereiche identifiziert und bewertet. Hier wird deutlich, dass die formale Beschreibung auf Basis der GDL-II bereits in einfachem Umfeld Anwendung finden kann, aber auch Potenziale für komplexe Märkte, wie die Börse, bietet.

2. Grundlagen

2.1. General Game Playing (GGP)

Das General Game Playing ist ein vergleichsweise junges Forschungsgebiet der künstlichen Intelligenz, welches sich mit automatisierten Playern beschäftigt, die vorab unbekannte Spiele spielen. Diese Player entwickeln zur Laufzeit, gegeben eine hinreichende Spezifikation eines Spiels, ad-hoc Strategien, die es ihnen ermöglichen ein beliebiges Spiel ohne jegliche menschliche Interaktion zu spielen [Gen05] . Hierzu nutzen sie diverse AI-Technologien wie knowledge representation, reasoning, learning und rational decision making [Gen05] . Die Einsatzmöglichkeiten sind hierbei lediglich durch die Ausdrucksmächtigkeit der Sprache beschränkt. Dies unterscheidet sie wesentlich von bisher bekannten, hochspezialisierten Bots (z.B. „Deep Blue“), die nur in der Lage sind ein einziges Spiel zu spielen und dementsprechend eine anwendungsbezogene Strategie besitzen. General Game Player agieren hingegen auf einer Meta-Ebene, die erstmalig 1992 vom Wissenschaftler Barney Pell in seiner Publikation „METAGAME in Symmetric Chess-Like Games“ [Pel92] thematisiert wurde. Pell legte damit den Grundstein für das GGP und gründete damit einen neuen Forschungszweig, der seit 2005 im Rahmen der AAAI Conference [Gen05] durch jährliche Wettbewerbe angetrieben wird. Eine standardisierte Spezifikation, die „Game Description Language“ (kurz: GDL), der Spiele unterstützt diese Entwicklung und ermöglicht den Entwurf von vergleichbaren Playern [Lov06] . Da die Modellierbarkeit von Spielen abhängig von der Ausdrucksmächtigkeit der verwendeten Spielbeschreibung ist, wird diese kontinuierlich ergänzt und verbessert, um so zunehmend komplexere Mechanismen modellieren zu können. Bisher ist das GGP ein rein wissenschaftliches Forschungsgebiet, welches keine praxisrelevanten Anwendungsbereiche besitzt. Durch die rasante Entwicklung und stetige Verbesserung der Agenten und der dazu benötigten Infrastruktur, ist es jedoch vorstellbar, dass diese Technologien mittelfristig auch im wirtschaftlichen Umfeld eingesetzt werden. Hierzu ist es erforderlich relevante Parameter eines realen Systems, als Spiel zu modellieren. Die in dieser Arbeit vorgestellten Modelle von börsennahen Auktionstypen sind ein Beispiel dafür und ermöglichen z.B. den Einsatz von automatisierten Agenten in Börsen oder börsenähnlichen Märkten.

2.2. Game Description Language (GDL)1

Die Spezifikation der Game Description Language (GDL) stellt einen Standard zur formalen Beschreibung von Spielen dar. Die aktuelle Version beschränkt sich insbesondere auf diskrete, deterministische Multiplayer-Spiele mit vollständiger Information. Dies schränkt die Vielfalt an beschreibbaren Spielen stark ein, da sämtliche Spiele, die z.B. eine zufällige Komponente2 enthalten, nicht modelliert werden können. Trotz dieser Einschränkung wäre es äußerst impraktikabel ein Spiel als einen Graphen mit sämtlichen möglichen Zuständen zu modellieren, da die Anzahl der Zustände u.U. enorm hoch sein kann3. Stattdessen versucht die GDL ein Spiel durch eine kompakte Menge an Transitionen zu beschreiben, die auf eine beschränkte Menge von initialen Fakten angewendet werden kann und so zu neuen Fakten führt. Die Umsetzung der GDL erfolgt in der Sprache KIF, dessen Syntax für das weitere Verständnis kurz genannt wird:

wird zu ?x

wird zu (f a ?x (g (h c ?y) e))

wird zu (true (cell 1 1 ?x))

wird zu (not (true (cell 1 1 ?x)))

wird zu (<= (p ?x) (q ?x) (not (r ?x)))

wird zu

(<= (p ?x) (q ?x) (or (r ?x) (s ?x))) Die GDL Spezifikation basiert wesentlich auf der datalog¬ Syntax und erweitert diese um Funktionen als Konstanten, sowie Rekursionsrestriktionen, die dafür sorgen, dass die Semantik dennoch endlich bleibt. Diese Konzepte gliedern sich in Relationen und Definition und sollen im Folgenden erläutert werden:

2.2.1. Relationen4

Relationen sind elementare Konzepte der GDL. Sie sind die Instrumente mittels derer ein Spiel und seine Regeln beschrieben wird. Die GDL unterscheidet folgende Relationen:

Role Relation

Die role Relation definiert die Namen und Zugleich die Anzahl der Spieler. Für das gewählte Beispiel wäre es also:

(role xplayer)

(role oplayer)

True Relation

Die true Relation beschreibt Fakten, die in Form eines ground Terms dargestellt werden. Die Syntax einer true Relation ist true(fact). Sei control eine Funktion, die beschreibt welcher Spieler an der Reihe ist. Dann bezeichnet der atomare Satz

(true (control xplayer))

einen Status in dem der ground Term (control xplayer) wahr ist. D.h. xplayer ist an der Reihe.

1 Vgl. [Lov06]

2 Dazu gehören z.B. alle Spiele mit einem Würfel.

3 Beim Schach gibt es 10

28 Zustände

4 Zum besseren Verständnis werden vereinzelte Relationen anhand des Beispiels „Tic-Tac-Toe“ erklärt.

Init Relation

Analog zur true Relation bezeichnet auch die init Relation Fakten, die in Form eines ground Terms dargestellt werden. Allerdings sind Ausdrücke dieser Relation nur im Startzustand gültig und beschreiben somit die Ausgangssituation eines Spiels. Bei Tic-Tac-Toe bedeutet das, dass alle Zellen leer („b“ wie „blank“) sind und einer der Spieler an der Reihe ist:

(init (cell 1 1 b))

(init (cell 1 2 b))

(init (cell 1 3 b))

…

(init (control xplayer))

Next Relation

Genauso bezeichnet auch die next Relation wahre Fakten. Allerdings beschreibt sie Fakten die im nächsten Zustand nach dem aktuellen Zustand wahr sind. So wechseln sich die Spieler z.B. bei Tic-Tac-Toe ab:

(<= (next (control xplayer))

(true (control oplayer)))

(<= (next (control oplayer))

(true (control xplayer)))

Legal Relation

Die legal Relation beschreibt erlaubte Spielzüge eines Spielers. Sie allokiert Spielzüge und Player unter Berücksichtigung des aktuellen Zustands, der durch die true Relationen beschrieben wird. Bei Tic-Tac-Toe z.B. darf ein Spieler nur leere Zellen markieren, sofern er an der Reihe ist. Der andere Spieler darf keinen Zug ausführen (noop):

(<= (legal ?w (mark ?x ?y))

(true (cell ?x ?y b))

(true (control ?w)))

(<= (legal xplayer noop)

(true (control oplayer)))

(<= (legal oplayer noop)

(true (control xplayer)))

Does Relation

Die does Relation ist der Syntax in der legal Relation sehr ähnlich. Allerdings beschreibt sie tatsächliche gewählte Spielzüge eines Spielers. Sie wird benötigt, um den Folgezustand in Abhängigkeit des gewählten Spielzuges zu modellieren. Im Beispiel bedeutet es, dass eine Zelle markiert wird, sobald ein Spieler diese auswählt:

(<= (next (cell ?m ?n x))

(does xplayer (mark ?m ?n))

(true (cell ?m ?n b)))

Der Vollständigkeit wegen müsste zudem beschrieben werden, dass alle anderen Zellen unverändert bleiben.

Goal Relation

Die goal Relation definiert das Ziel des Spiels. Hierbei können ganzzahlige Punkte von 0 bis 100 auf die jeweiligen Spieler verteilt werden. Beim Tic-Tac-Toe bekommt entweder ein Spieler alle Punkte und gewinnt das Spiel (100:0) oder es gibt ein Unentschieden (50:50). Das Ziel der Spieler ist es

jedoch, durch eine markierte Reihe zu gewinnen. Demnach lautet die goal Relation für den Spieler xplayer:

(<= (goal xplayer 100)

(line x))

Terminal Relation

Terminal Relationen beschreiben wann ein Spiel beendet ist und definieren so die Endzustände. Im gewählten Beispiel ist dies der Fall, sobald ein Spieler eine Reihe markiert, oder keine Spielzüge mehr möglich sind:

(<= terminal

(line x))

(<= terminal

(line o))

(<= terminal

(not open))

Die terminal Relation gibt nicht an, welcher Spieler gewonnen hat und welche Auszahlung bekommt!

2.2.2. Definitionen

Neben den Relationen geben die Definitionen Rahmenbedingungen vor, wie die Relationen eingesetzt werden dürfen. Diese Bedingungen werden im folgenden Abschnitt vorgestellt:

Vokabular

Das Vokabular besteht aus einer Menge von Termen und atomaren Sätzen.

Term

Ein Term ist eine Variable oder eine Konstante. Kleinbuchstaben repräsentieren hierbei Konstanten. Variablen hingegen, werden als Großbuchstaben dargestellt.

Atomarer Satz

Ein atomarer Satz der Arität n ist die Komposition einer Konstanten mit einem Tupel aus Termen der Form p(1, 1,X).

Literale

Ein Literal ist ein atomarer Satz oder dessen Negation.

Ground Expressions

Ein Ausdruck heißt „ground“, wenn dieser keine Variablen enthält.

Datalog Regeln

Eine Datalog Regel ist eine Implikation der Form: ⏟

⏟

wobei der head h ein atomarer Satz und jedes im body ein Literal oder eine Disjunktion von Literalen5 ist. Zudem muss die Safety erfüllt sein. Dies bedeutet, dass eine Variable, die im head

5 Die Disjunktion wurde in der GDL ergänzt, um Berechnungen von Spielbeschreibungen durch General Game Player zu

beschleunigen. Sie hat keine zusätzliche Bedeutung für die Definition (Anm. d. Her.).

oder in einem negativen Literal auftaucht außerdem in einem positiven Literal im body stehen muss. Der Ausdruck distinct wird dabei als negatives Literal behandelt. Durch diese Anforderung wird sichergestellt, dass ein Modell nur endlich groß ist und eine Regel stets eindeutig interpretierbar ist. Außerdem müssen die Regeln so gewählt werden, dass die Rekursionsrestriktion erfüllbar ist6.

Abhängigkeitsgraph

Sei eine Menge von Datalog Regeln. Dann sind die Knoten des Abhängigkeitsgraphen für die atomaren Sätze des Vokabulars. Sofern es eine Regel mit im head und im body gibt, so existiert im Abhängigkeitsgraphen eine Kante von nach . Wenn ein negatives Literal ist, so wird diese Kante mit gekennzeichnet.

Stratifizierbare Datalog Regeln

Eine Menge von Datalog Regeln heißt stratifizierbar, wenn es im dazugehörigen Abhängigkeitsgraphen keinen Zyklus mit einer Kante gibt, die mit gekennzeichnet ist. Diese Definition ist von besonderer Bedeutung, da sie logische Inkonsistenzen und Mehrdeutigkeiten vermeidet und somit eine wesentliche Anforderung an jede Datalog Regel ist.

Modell

Ein Modell der Sprache L besteht aus einer Menge von ground atomaren Sätzen aus L.

Erfüllbarkeit

Folgende Ausdrücke eines Modells M sind erfüllbar, sofern deren dahinterstehende Bedingung wahr ist:

genau dann, wenn und syntaktisch nicht der selbe Term sind

genau dann, wenn der Ausdruck in M nicht erfüllbar ist

genau dann, wenn ist in M erfüllbar

genau dann, wenn ist in M erfüllbar

genau dann, wenn entweder oder oder beides in M erfüllbar ist

genau dann, wenn erfüllbar in für jeden ground Term

Entailment

Eine Menge an Datalog Regeln, die keine Negation enthält, heißt „Horn“. Für diese Menge gibt es genau ein minimales, erfüllbares Modell, wobei ein Modell M kleiner als N ist, wenn . Dieses minimale Modell ist der Sinngehalt der Menge. Entailment7 bedeutet, dass genau dann einen Ausdruck impliziert, sofern dieser in M erfüllbar ist.

Stratum

Sei a ein atomarer Satz in einer Menge an stratifizierbaren Datalog Regeln. Dann ist a in Stratum i, wenn die maximale Anzahl von -Kanten, in jedem Pfad vom Knoten a im Abhängigkeitsgraphen zu , gleich i ist. Eine Regel ist in Stratum i sofern der head einen atomaren Satz in Stratum i beinhaltet.

6 Siehe Abschnitt „Rekursionsrestriktion“ in Kapitel „‎2.2.3 Erweiterung der Definitionen“

7 Im deutschen Sprachgebrauch auch als „semantische Implikation“ bezeichnet

Stratifizierbare Datalog Semantik8

Jede Regel in eine Menge von stratifizierbaren Datalog Regeln hat ein endliches Stratum9. Zudem gibt es mindestens eine Regel mit Stratum 0. Diese Regeln sind Horn und haben somit ein minimales Modell . Dieses Modell wird durch die Fakten, die durch Regeln mit Stratum 1 geschaffen werden, zum Modell erweitert. Durch Wiederholung dieses Prozesses mit den Regeln in Stratum 2 wird dieses zum Modell erweitert usw. Die Stratifizierbare Datalog Semantik von ist das Modell mit maximalem Stratum k für jede Regel in .

Stratifizierbares Entailment

Genauso gilt auch für die stratifizierbare Datalog Semantik die semantische Implikation, die als stratifizierbares Entailment bezeichnet wird.

2.2.3. Erweiterung der Definitionen

Um die beschriebene Semantik der Relationen sicherzustellen müssen zusätzliche Restriktionen eingeführt werden, die syntaktisch korrekte, aber ungewollte Ausdrücke vermeiden. So besagt folgende Regel

(<= (role p) (true q)),

dass p ein (neuer) Player ist, sofern q erfüllt ist. Allerdings fordert die Spezifikation, dass die Anzahl der Spieler fix und nicht abhängig von den Zuständen zur Laufzeit sind. Die oben beschriebenen Definitionen werden daher wie folgt ergänzt:

Rekursionsrestriktion

In einer Datalog Regel sei im Abhängigkeitsgraphen in einem Kreis mit . Dann gilt { } entweder ist ground oder

{ } mit , wobei nicht in einem Kreis mit auftritt.

GDL Restriktionen

Wenn eine GDL Beschreibung und dessen Abhängigkeitsgraph ist, muss folgendes für gelten: Die role Relation darf nur in ground atomaren Sätzen auftauchen (z.B. im head ohne body). Eine Veränderung der Spieler, wie im oben genannten Beispiel wird somit verhindert.

Die init Relation darf nur im head einer Datalog Regel auftauchen. Der init Knoten in enthält zudem keine der folgenden Komponenten: true, does, next, legal, goal oder terminal.

Dies kapselt den Startzustand als reine Beschreibung ab und verhindert Kanten, die dorthin zurückführen.

Die true Relation taucht nur im body einer Datalog Regel auf Fakten werden nicht durch die true Relation geschaffen, sondern nur durch diese beschrieben.

Die next Relation taucht nur im head einer Datalog Regel auf Die next Relation beschreibt Fakten im nächsten Zustand und ist kein Ersatz für die true Relation

8 Vgl. auch [Apt88]

9 Dies wird durch die Safety sichergestellt (siehe Definition „Datalog Regeln“)

Die does Relation taucht nur im body einer Datalog Regel auf. In G gibt es zudem keinen Pfad zwischen dem does Knoten und einem legal, goal oder terminal Knoten.

Die does Relation ist kein Fakt der durch andere Fakten geschaffen wird, sondern dient der Beschreibung von Zustandsveränderungen. Sie ist eine dynamische Komponente und ist daher ungeeignet zur Verwendung in legal, goal oder terminal Koten All diese Definitionen gewährleisten nun eindeutige Interpretationen mittels derer ein General Game Player seine Züge wählen und Zustände berechnen kann. Allerdings stellt die GDL zusätzliche Anforderungen an eine Beschreibung, da sie möglicherweise nie endet oder nicht zu gewinnen ist:

Terminiertheit

Eine Beschreibung in GDL terminiert, wenn alle Sequenzen von legalen Spielzügen im Startzustand nach einer endlichen Anzahl von Schritten zu einem Endzustand führen

Spielbarkeit

Eine Beschreibung in GDL ist spielbar, wenn jede Rolle in jedem Zustand, der kein Endzustand ist, mind. einen legalen Spielzug hat.

Gewinnbarkeit

Eine Beschreibung in GDL ist stark gewinnbar, wenn es für eine Rolle eine Sequenz gibt, die zu einem Endzustand führt, indem die Punktzahl für diesen Spieler maximal ist. Eine Beschreibung in GDL ist schwach gewinnbar, wenn es für jede Rolle eine Sequenz von gemeinsamen Spielzügen von allen Rollen gibt, die zu einem Endzustand führt, indem die Punktzahl für diese Rolle maximal ist.

Wohldefinierte Spiele

Eine Beschreibung in GDL ist wohl definiert, wenn sie die Anforderungen an die Terminiertheit, Spielbarkeit und Gewinnbarkeit erfüllt.

2.3. Erweiterungen der GDL

Die soeben vorgestellte Beschreibungssprache liefert uns ein solides Grundgerüst zur Modellierung von Spielen. Aufgrund der mangelnden Beschreibungsmöglichkeit von Kommunikation zwischen den Playern, partieller Information und zufälliger Ereignisse, bedarf es jedoch einer Weiterentwicklung. So wurden mehrere Ansätze entwickelt, um die Ausdrucksmächtigkeit zu erhöhen, von denen einige im Folgenden erläutert werden sollen.

2.3.1. Stochastische Spiele in GDL

In [Kul09] wird ein Ansatz beschrieben, um die GDL um Zufallsereignisse zu erweitern. Hierfür schlagen die Autoren folgende neue Relation vor:

random <name> <value> <expression>

Der erste Parameter bezeichnet hierbei den Namen der Zufallsvariablen, der für Ereignisse desselben Zufallsexperiments gleich sein muss. Dieser Ausdruck ist bewusst atomar und keine Variable, da sie nicht von den Spielern, sondern von einer zentralen Instanz (dem Game Manager) unifiziert werden. Der zweite Parameter ist eine ganzzahlige Zahl , die die Wahrscheinlichkeit für das Ereignis (dritter Parameter) angibt. Das Ereignis ist ein beliebiger GDL-Ausdruck, dessen Wahrscheinlichkeit

aus

∑

ergibt.

Die Zufallsvariable darf aufgrund der Kommunikationsstruktur bei einer Competition lediglich in der legal-Relation auftauchen. So wird sichergestellt, dass dem Player das Ergebnis des Zufallsexperiments tatsächlich übermittelt wird. Allerdings ist die Verwendung der Zufallsvariablen auch in Implikationen erlaubt, um Abhängigkeiten der Wahrscheinlichkeiten im Spielverlauf modellieren zu können.10

2.3.2. Market Specification Language (MSL)11

Die Market Specification Language ist weniger eine Erweiterung, sondern vielmehr eine neue Beschreibungssprache, die auf der GDL basiert. Im Wesentlichen lassen sich vier Unterschiede identifizieren:

Market Maker

Die MSL spezifiziert die Rolle eines Market Makers12, der als Gegenpart zu einem Trader auf Basis bestimmter Regeln handelt. Neben den Quotes, die an alle Trader geschickt werden, versendet der Market Maker Nachrichten an einzelne Trader, um einen akzeptierten oder abgelehnten Trade zu signalisieren.

Trader

Neben dem Market Maker ist zudem die Rolle des Traders spezifiziert, der Nachrichten versenden und empfangen kann. Im Marktumfeld sind dies z.B. die Bid/Ask-Quotes. Somit gibt es also nur noch einen Akteur (Market Maker) der Aktionen durchführen kann und mehrere Akteure (Trader), die miteinander kommunizieren können.

Partielle Information

Anders als bei einem Spiel in GDL ist es nun möglich, dass unterschiedliche Trader unterschiedliche Informationen besitzen. So kann z.B. ein Markt modelliert werden, bei dem nur die Vertragspartner eines Trades von diesem Trade erfahren. Alle anderen Trader haben diese Information nicht. Ebenso können Quotes nur an bestimmte Trader versendet werden.

Umgebungsparameter

In der MSL wurde die Zeit als Parameter eingeführt um asynchrone Kommunikation zu ermöglichen. Ebenso wurden grundlegende Funktionen (Grundrechenarten) sowie die Relationen von reellen Zahlen definiert. Es muss somit also z.B. nicht mehr vorab spezifiziert werden, dass die Zahl „2“ eine höhere Wertigkeit besitzt als die Zahl „1“. Alle anderen Relationen und Definitionen der GDL wurden analog übernommen. Somit wurde es insbesondere ermöglicht partielle Informationen zu modellieren, um so einen Marktmechanismus zu beschreiben.

2.3.3. Gala13

Gala (GAme LAnguage) ist ein ganz anderer Ansatz zur Beschreibung von Spielen, der noch vor der ersten Version der GDL bereits im Jahre 1997 von Koller und Pfeffer entwickelt wurde. Er verfolgt ebenfalls das Ziel eine formale Repräsentation von Spielen auf einer Meta-Ebene zu ermöglichen, so wie sie ursprünglich von Barney Pell thematisiert wurde. Gala ermöglichte bereits die 10

Zum Beispiel kann in einem Kartendeck jede Karte in der Regel nur einmal gezogen werden. Die Wahrscheinlichkeit eine gezogene Karte ein weiteres Mal zu ziehen, sinkt damit auf 0. 11

Vgl. [Thi09] 12

Eine detaillierte Beschreibung verschiedener Akteure auf Märkten findet sich in [Har02] 13

Vgl. [Kol97]

Beschreibung von Multi-Player Spielen und die Beschreibung unvollständiger Information, sowie zufälliger Ereignisse. Ein Gala Programm besteht dabei aus zwei Kategorien: Im ersten Abschnitt werden Entitäten, also z.B. Player, beschrieben. Im zweiten Abschnitt werden mögliche Ereignisse modelliert. Spielzüge werden in der zweiten Kategorie modelliert und können durch folgende Gala Statements beschrieben werden:

Choose definiert die möglichen Optionen einer Entität und gibt an ob diese zufällig gewählt wird

Reveal beschreibt den Informationsfluss zwischen den Entitäten

Payoff gibt schließlich an wie die Auszahlungen sind Ein Spielzug beim Poker in Gala modelliert könnte demnach wie folgt aussehen:

Abbildung 1: Gala Spielzug Quelle: [Kol97]

Neben diesen Statements gibt es weitere Statements, die die Sprache vervollständigen. Die komplette Spezifikation der Sprache kann in [Kol97] nachgelesen werden.

2.3.4. GDL for Incomplete Information (GDL II)14

Die GDL II ist eine Beschreibungssprache, die im Wesentlichen auf den bereits bekannten Konzepten der GDL 15 basiert. Ein großer Nachteil der GDL war die beschränkte Ausdrucksmächtigkeit, die es nicht ermöglichte Spiele mit unvollständiger Information oder stochastischen Ereignissen zu beschreiben. Dies wird durch diese Variante nun ermöglicht. Anders als der Name vermuten lässt werden nicht nur unvollständige Informationen, sondern zugleich auch stochastische Ereignisse ermöglicht. Hierzu wird die bereits bekannte GDL lediglich um zwei weitere Relationen erweitert. Diese neuen Relationen sollen im Folgenden erläutert werden. Hierbei wird die Kenntnis der GDL vorausgesetzt:

Sees Relation

Abgeleitet von dem englischen Begriff für das Verb „sehen“ (to see) beschreibt der Term sees(R,P) eine Information P die ein Player R (definiert durch role(R)) erhält. Dies impliziert auch, dass nicht mehr alle Spieler alle Informationen erhalten, sondern jeder Informationsfluss explizit modelliert werden muss. Hierdurch wird es ermöglicht bestimmte Informationen nur bestimmten Playern bekannt zu geben. So ist es also zum Beispiel möglich einzelnen Spielern ihre Spielkarten mitzuteilen:

sees(Anna,Ace)

sees(Ben,King)

Man beachte, dass in diesem einfachen Beispiel bereits unvollständige Information modelliert wurde. Spielerin Anna hat keinerlei Kenntnis darüber, welche Karte Spieler Ben erhalten hat und umgekehrt. Jeder kennt jedoch seine eigene Karte.

14

Vgl. [Thi10] 15

Vgl. Abschnitt Game Description Language (GDL)

Random Player

In der Regel reicht obige Relation nicht aus, um zum Beispiel Kartenspiele zu modellieren, da diese häufig zufällig verteilt werden. Für Spiele mit stochastischen Ereignissen schlägt der Autor der GDL II daher einen Player random (definiert durch role(random)) vor, der seine Entscheidungen rein zufällig trifft. Die möglichen Ereignisse werden dabei durch die legal-Relation definiert. Die Wahl des Ereignisses wird dann durch den Game Controller getroffen, wobei die Wahrscheinlichkeiten gleichverteilt sind. Dies bedeutet jedoch nicht, dass für die möglichen Ergebnisse stets eine Gleichverteilung unterstellt wird. So ist es zum Beispiel dennoch möglich einen Spielwürfel darzustellen, der mit höherer Wahrscheinlichkeit eine „6“ zeigt. Ein solch unfairer Spielwürfel wäre wie folgt modellierbar:

role(random)

legal(random,1)

legal(random,2)

legal(random,3)

legal(random,4)

legal(random,5)

legal(random,6)

legal(random,6)

Wie ersichtlich ist, wurde das Ergebnis „6“ zweifach aufgenommen. Wir haben somit sieben

Ereignisse, die jeweils mit Wahrscheinlichkeit

(Gleichverteilung der Ereignisse) auftreten. Zwei

dieser Ereignisse liefern jedoch dasselbe Ergebnis. Somit ist die Wahrscheinlichkeit eine „6“ zu

würfeln

und für jede andere Zahl

(keine Gleichverteilung der Ergebnisse).

Erweiterung der GDL Restriktionen

In der GDL wurden bereits einige Restriktionen eingeführt, die eine eindeutige Interpretation einer Spielbeschreibung ermöglichen. Aufgrund der neu eingeführten sees Relation der GDL II müssen auch die Restriktionen geringfügig angepasst werden:

Die init Relation darf nur im head einer Datalog Regel auftauchen. Der init Knoten in enthält zudem keine der folgenden Komponenten: true, does, next, sees, legal, goal oder terminal.

Die next und sees Relation taucht nur im head einer Datalog Regel auf Insbesondere ist die zweite Restriktion interessant, da hier nochmal die Bedeutung der sees Relation klar definiert wird. Es soll vermieden werden, dass die Informationen, die ein Spieler besitzt in irgendeiner Art und Weise mögliche Spielzüge oder gar etwaige Auszahlungen beeinflussen. Die vorhandene Information bleibt dadurch unverwechselbar mit identifizierbaren Strukturen des Spiels, wie z.B. Spielsteinen.16

Semantik eines Spiels

Auf Basis der GDL II ist die Semantik eines Spiels durch ein Tupel der Form gegeben. Wenn die Menge der domänenspezifischen ground Terms und die endliche Teilmenge von bezeichnet, sind obige Parameter wie folgt definiert:

{ } (Erklärung: Dies beschreibt die verschiedenen Rollen des Spiels)

{ } (Erklärung: Dies beschreibt den Startzustand)

{ } (Erklärung: Dies beschreibt die Endzustände)

16

Näheres zur Identifikation und Definition von Strukturen kann in [Kuh06] nachgelesen werden

{ } (Erklärung: Dies beschreibt die erlaubten Spielzüge eines Spielers im Zustand )

{ } (Erklärung: Dies ist die Aktualisierungsfunktion, die Zustandsänderungen auf Basis der Menge aller gewählten Spielzüge im Zustand beschreibt)

{ } { } (Erklärung: Dies beschreibt den Informationsfluss auf Basis aller gewählten Spielzüge im aktuellen Zustand zu Spieler )

{ } { } (Erklärung: Dies beschreibt den Zielwert für Spieler im Zustand )

{ } ,

Wenn : {

Sonst wird dem Zustand durch folgende Wahrscheinlichkeit zugeordnet: |{ { } }|

| | mit { } (Erklärung: ist das

Wahrscheinlichkeitsmaß über die resultierenden Spielzüge auf Basis des aktuellen Zustands und allen gewählten Spielzügen , ohne den random-Player)

2.4. Auktionstypen17 Im Folgenden wird ein kurzer Exkurs mit den wesentlichen Grundlagen zur Auktionstheorie vorgestellt. Insbesondere werden einige Auktionstypen vorgestellt, um die Funktionsweise derer zu verstehen. Spiegelbildlich dazu verhalten sich Ausschreibungen („reverse auctions“), die jedoch in diesem Abschnitt ausgeklammert und nicht weiter betrachtet werden. Ebenso liegt der Fokus hierbei nicht in dem konkreten Design der Auktion, sondern vielmehr dem darunterliegendem Konzept welches den Mechanismus charakterisiert und von anderen Mechanismen unterscheidet. So können die verschiedenen Auktionstypen wie folgt kategorisiert werden:

Einseitige Zweiseitige Auktionen

Offene Verdeckte Gebote

Absteigend Aufsteigend Die Bedeutung dieser Kategorien wird anhand gängiger Auktionstypen erläutert. Hierzu zählen insbesondere die Höchstpreisauktion, Vickrey-Auktion, Holländische Auktion, Englische Auktion, Call Market und die Continuous Double Auction (CDA). Neben diesen Kategorien unterscheiden McAffee und McMillan jedoch noch zwei Modelle zur Wertschätzung der versteigerten Güter:

Independent-private-value-model

In diesem Modell hat das Gut für jeden Teilnehmer einen Wert, der unabhängig von der Wertschätzung anderer Teilnehmer und nur ihm bekannt ist. Dies ist zum Beispiel besonders für Güter mit Liebhaberwert plausibel.

Common-value-model

Nach diesem Modell besitzt das versteigerte Gut einen objektiven Wert, der für alle gleich, jedoch keinem bekannt ist. Jeder Teilnehmer gibt demnach mit seinem Gebot lediglich eine Schätzung ab,

17

Vgl. [McA87] und [Rei00]

die wiederum die Gebote anderer beeinflussen können. Das Prinzip ist daher vergleichbar mit der „Weisheit der Vielen“18 wie sie von James Surowiecki beschrieben wird. In Verbindung mit dem common-value-model spricht man auch häufig vom „winner‘s curse“. Da der wahre Wert des Guts in der Regel unter der höchsten Schätzung liegt, ist es naheliegend, dass derjenige der den Zuschlag erhält, den wahren Wert am meisten überschätzt hat und somit der Zuschlag für ihn eher nachteilig ist.

2.4.1. Höchstpreisauktion19

Die Höchstpreisauktion gehört zu den einseitigen Auktionen mit verdeckten Geboten. Hierbei gibt jeder Teilnehmer genau ein verdecktes Gebot ab. Der Auktionator ermittelt den Bieter mit dem höchsten Gebot. Dieser erhält den Zuschlag und zahlt den Preis in Höhe des abgegebenen Gebots. Eine gute Bietstrategie im independent-private-value-model berücksichtigt also die Reservationspreise der anderen Teilnehmer derart, dass das eigene Gebot marginal über dem höchsten Gebot der anderen Teilnehmer ist, ohne die eigene Wertschätzung zu übersteigen. Allerdings können diese Reservationspreise aufgrund der Geheimhaltung und der Abgabe eines einmaligen Gebots nur vorab geschätzt werden und nicht auf Basis abgegebener Gebote erfolgen. Im common-value-model ist das Risiko des „winner’s curse“ besonders hoch und wird daher in solchen Fällen gemieden. Diese Auktionsform wird häufig im Rahmen der Vergabe von öffentlichen Aufträgen angewandt.20

2.4.2. Vickrey-Auktion21

Die Vickrey-Auktion ist ebenfalls unter die einseitigen Auktionen mit verdeckter Gebotsabgabe einzuordnen. Sie ist benannt nach William Vickrey, der diesen Auktionstyp erstmals im Jahre 1961 in seiner Ausarbeitung „Counterspeculation, Auctions, and Competitive Sealed Tenders“ beschreibt. Sie funktioniert ganz ähnlich wie die zuvor erläuterte Höchstpreisauktion. Jeder Teilnehmer gibt verdeckt genau ein Gebot ab. Analog zur Höchstpreisauktion erhält der Bieter mit dem höchsten Gebot den Zuschlag. Allerdings muss dieser nur den Preis des zweithöchsten Gebots zahlen. Daher ist dieser Auktionstyp auch als Zweitpreisauktion bekannt. Ein rationaler Teilnehmer wird bei diesem Auktionstyp stets seine wahre Wertschätzung bieten. Dies bringt jedoch auch Probleme mit sich. So könnte die persönliche Wertschätzung von einigen Teilnehmern als sensible Information gesehen werden, die sie in dem Fall ungern preisgeben möchten. So könnten Bieter einen Betrug durch den Auktionator befürchten. Rothkopf, Teisberg und Kahn sehen darin die Ursache für die Tatsache, dass diese Auktionsform nur selten in der Praxis angewandt wird. Lucking-Reiley präsentiert jedoch Maßnahmen, die diese Probleme umgehen. So ist es inzwischen technologisch möglich den Auktionator durch ein vollautomatisiertes System zu ersetzen. Doch auch bei einem menschlichen Auktionator reiche die Kraft der Reputation, um Missbrauch auszuschließen. Ebenso stelle die Transparenz der Gebote eine Lösung dar.

2.4.3. Holländische Auktion22

Die holländische Auktion ist ebenfalls einseitig, wobei die Gebote offen abgegeben werden. Der Auktionator nennt absteigende Kaufpreise. Der Teilnehmer, der als erster einen Preis annimmt erhält den Zuschlag zum genannten Kaufpreis.

18

Vgl. [Sur04] 19

Vgl. [McA87] , [Ste10] und [Fis98] 20

Vgl. hierbei handelt es sich dann um eine „reverse auction“ (siehe Einführung) 21

Vgl. [Vic61] , [McA87] , [Rot90] und [Luc00] 22

Vgl. [McA87] und [Vic61]

Interessanter Weise führt diese Auktion zum selben Ergebnis wie die Höchstpreisauktion, da der Teilnehmer mit derselben Situation konfrontiert wird. Er kennt nicht die Wertschätzung der anderen Teilnehmer und muss diese schätzen. Diese Auktionsform wurde z.B. beim Tabakverkauf in Canada angewandt. Aber auch heute noch existiert diese Art der Auktion z.B. bei der Fernsehshow „1-2-3.tv“.

2.4.4. Englische Auktion23

Die englische Auktion gehört sicherlich zu den bekanntesten Auktionsformen und hat ihre Berühmtheit nicht zuletzt dem wohl bekanntesten Auktionshaus „Sotheby’s“ zu verdanken. Diese Auktion verläuft ganz ähnlich wie die holländische Auktion. Allerdings geben die Teilnehmer bei der englischen Auktion aufsteigende Gebote ab. Der letzte Bieter erhält den Zuschlag und zahlt den Preis in Höhe seines Gebotes. Die Besonderheit bei dieser Auktionsform ist, dass das jeweils höchste, aktuelle Gebot jedem bekannt ist und die Teilnehmer sich so untereinander beobachten können. Vor allem kann ein Bieter innerhalb einer Versteigerung mehrere aufsteigende Gebote abgeben. Das Inkrement kann jedoch vom Auktionator reglementiert werden. Gebote, die unter dem Reservationspreis des Auktionators liegen, müssen nicht angenommen werden. Eine gute Bietstrategie bei dieser Auktionsform, unter der Annahme des Independent-private-value-models, ist es solange ein Gebot abzugeben, bis ein anderer Teilnehmer ein Gebot abgibt, welches die eigene Wertschätzung übersteigt. Dies führt dazu, dass der Teilnehmer mit der höchsten Wertschätzung den Zuschlag erhalten wird und zwar zum Preis der zweithöchsten Wertschätzung. Demzufolge erhält man ein äquivalentes Ergebnis zur Vickrey-Auktion.

2.4.5. Call Auction24

Bei den bisherigen Auktionsformen wurden die Gebote stets von einer Partei, also einseitig, abgegeben. Anders verhält es sich bei der Call Auction. Diese gehört zu den zweiseitigen Auktionsformen mit verdeckter Gebotsabgabe. Dabei werden bei der Durchführung folgende Schritte durchlaufen: Zunächst werden die Gebote25 der Teilnehmer über einen fixen Zeitraum gesammelt. Sobald die Zeit abgelaufen ist, werden die Gebote analysiert und es wird nach bestimmten Vorgaben ein Preis fixiert, der für alle Teilnehmer gleich ist. In der Regel wird der Preis derart bestimmt, dass das Handelsvolumen maximal ist. Anschließend kommt es zwischen den Teilnehmern zum Kaufabschluss. Dieser Auktionstyp wird in der Regel an Börsen im Wertpapierhandel angewandt. Er eignet sich besonders, um z.B. am Morgen eines Handelstages Liquidität zu aggregieren und neue Informationen einzupreisen.

2.4.6. Continuous Double Auction (CDA)26

Die CDA ist ein an den Börsen weit verbreiteter Mechanismus, der einen flexiblen und dynamischen Wertpapierhandel ermöglicht. Ebenso wie bei der Call Auction handelt es sich hierbei um eine zweiseitige Auktion. Das heißt, sowohl Käufer, als auch Verkäufer geben ihre Gebote („Order“) ab. Man unterscheidet zwischen Kaufgeboten („Bid“) und Verkaufsgeboten („Ask“). Anders als bei der Call Auction können die Gebote jedoch jederzeit, also kontinuierlich (daher continuous), abgegeben werden. Diese Gebote werden dann in das sogenannte „Orderbuch“ aufgenommen. Dies ist eine sortierte Auflistung aller Kaufs- und Verkaufsgebote, die für jeden öffentlich einsehbar ist. Ein Teilnehmer kann sich jederzeit eine der platzierten Gebote

23

Vgl. [McA87] , [Rei00] und [Yam72] 24

Vgl. [Sch88] 25

Hierbei handelt es sich sowohl um Kauf-, als auch um Verkaufsgebote. Daher ist die Call Auction zweiseitig 26

Vgl. [Wil80]

auswählen und akzeptieren. Dies führt dann zum Kaufabschluss. Sofern die Order nach der Ausführung nicht mehr verfügbar ist, wird sie aus dem Orderbuch entfernt. Zur Übersicht sind die hier vorgestellten Auktionstypen in folgender Grafik nochmals aufgeführt und anhand der genannten Kategorien eingeordnet:

Abbildung 2: Auktionstypen Quelle: Prof. Dr. Christof Weinhardt, Institut für Informationswirtschaft und -management am KIT

3. Modellierung in GDL II Nachdem die Grundlagen der Modellierung und der Auktionstheorie erläutert wurden, sollen nun im folgenden Abschnitt die vorgestellten Auktionstypen modelliert werden. Hierbei wird die Beschreibungssprache GDL II als Mittel der Wahl eingesetzt. Die GDL II basiert in großen Teilen auf der bereits bewährten GDL, die auch im Rahmen von jährlichen Wettkämpfen verwendet wird.27 Aufgrund dieser Erfahrungswerte wird sie den Alternativen Gala und MSL vorgezogen. Die stochastische Erweiterung, wie sie in [Kul09] beschrieben wird, ist nicht ausreichend. Insbesondere der Aspekt unvollständiger, asymmetrischer Information ist nämlich essentiell, um zum Beispiel die Auktionstypen mit verdeckter Gebotsabgabe modellieren zu können. Die GDL II ist mächtig genug, um diesen Anforderungen gerecht zu werden. Die Beschreibungen werden stets in die Abschnitte „Initialisierung“, „Auktionsverlauf“ und „Auktionsende“ gegliedert. Dabei beschreibt der erste Abschnitt Startzustände und definiert Rollen. Im zweiten Abschnitt werden die Spielzüge und Informationsflüsse modelliert. Am Schluss werden die Abbruchbedingungen und Auszahlungen beschrieben. Um dem Leser das Verständnis zu erleichtern, wird darauf verzichtet, die Axiome in der Beschreibungssprache KIF zu modellieren, wie sie zu Beginn eingeführt wurde. Dies ist nur für die tatsächliche Umsetzung relevant, um das automatisierte Reasoning durch Agenten zu ermöglichen. Für einen menschlichen Leser kann jedoch darauf verzichtet werden. Die

27

Vgl. [Gen05]

Beschreibungen können jedoch bei Bedarf leicht, wie im Abschnitt „Game Description Language (GDL)“ beschrieben transferiert werden. In den nachfolgenden Modellen wird zudem davon ausgegangen, dass die Wertschätzung der Teilnehmer für das versteigerte Gut zwischen 0 und 100 liegt. In unseren Berechnungen wird stets davon ausgegangen, dass die Wertschätzung durch einen monetären Wert repräsentiert wird, der unmittelbar realisiert werden kann. Diese wird zu Beginn zufällig durch den random-Player festgelegt. Dabei wird eine Gleichverteilung der möglichen Werte unterstellt. In unseren Berechnungen wird stets davon ausgegangen, dass die Wertschätzung durch einen monetären Wert repräsentiert wird, der unmittelbar realisiert werden kann. Je nach Anwendung, könnten die Anfangsbedingungen selbstverständlich auch leicht angepasst werden, um zum Beispiel ein konkretes Szenario nachzustellen. So könnte man bei der Initialisierung auch direkt die Wertschätzungen der Teilnehmer definieren. Allerdings sind diese aus Sicht der anderen Teilnehmer in der Regel unbekannt und bewegen sich innerhalb eines bestimmten Intervalls. Daher sind die hier getroffenen Annahmen durchaus plausibel. Die Größe des Intervalls und die Höhe der Wertschätzung lassen sich durch minimale Veränderungen beliebig skalieren.

3.1. Einseitige Auktionen Zunächst werden die einseitigen Auktionen modelliert, so wie im Abschnitt „Auktionstypen“ beschrieben wurden.

3.1.1. Höchstpreisauktion

Initialisierung

Bei einer Englischen Auktion gibt es einen oder mehrere Bieter, die Gebote abgeben, sowie einen Auktionator, der dem Bieter mit dem höchsten Gebot den Zuschlag erteilt:

role(a_1)

…

role(a_m)

role(auctioneer)

role(random)

val(0)

…

val(100)

init(initRound)

Auktionsverlauf

Der Verlauf der Auktion wird in vier Phasen eingeteilt. In der „initRound“ werden die Wertschätzungen der einzelnen Teilnehmer durch den random-Player festgelegt. Erst wenn diese vergeben und mitgeteilt wurden beginnt die „bettingRound“, in der die Teilnehmer ihre verdeckten Gebote abgeben können. Hat jeder Teilnehmer ein Gebot abgegeben, beginnt die „clearingRound“ in der der Auktionator das Höchstgebot ermitteln und den Zuschlag erteilen kann. Danach ist die Auktion beendet („finishedRound“):

accept(bid(R,P)) does(R, my_bid(P)) true(bettingRound)

legal(auctioneer, clearing(R,P))

true(bid(R,P)) bestbid(P) true(clearingRound)

legal(R, my_bid(P))

role(R) distinct(R, auctioneer) distinct(R, random)

true(bettingRound) P 0

legal(random, set_values(V1,…,Vm))

true(initRound) val(V1) … val(Vm)

next(hasValue(a_1,V1)) does(random, set_values(V1,…,Vm))

…

next(hasValue(a_m,Vm)) does(random, set_values(V1,…,Vm))

next(hasValue(a_1,V1)) true(hasValue(a_1,V1))

…

next(hasValue(a_m,Vm)) true(hasValue(a_m,Vm))

next(bettingRound) does(random, set_values(V1,…,Vm))

next(bid(R,P)) accept(bid(R,P))

next(bid(R,P)) bid(R,P)

next(clearingRound) does(a_1, my_bid(P1)) … does(a_m, my_bid(Pm))

next(finishedRound) does(auctioneer, clearing(R,P))

bestbid(P) true(bid(R,P)) outbid(P)

outbid(P) true(bid(R,P1)) P1 P

sees(a_1, V1) does(random, set_values(V1,…,Vm))

…

sees(a_m, Vm) does(random, set_values(V1,…,Vm))

sees(auctioneer, bid(R1,P)) does(R1, my_bid(P))

sees(R, call_for_bid) true(bettingRound)

sees(R1, bid_accepted(P)) accept(bid(R1,P))

sees(R, winner(R1,P)) does(auctioneer, clearing(R1,P))

Auktionsende

Sobald die Auktion durch das Clearing des Auktionators beendet wurde, erhält der Meistbietende den Zuschlag. Seine Auszahlung ist abhängig von seiner Wertschätzung und dem Preis, den der Auktionator als Auszahlung erhält. Alle anderen Teilnehmer erhalten nichts:

terminal true(finishedRound)

goal(R1,V-P) true(bid(R1,P)) true(hasValue(R1,V)) true(bestbid(P))

goal(R,0)

true(bid(R1,P)) true(bestbid(P)) distinct(R,R1)

distinct(R, auctioneer)

goal(auctioneer, P) true(bestbid(P))

3.1.2. Vickrey-Auktion

Die Vickrey-Auktion ähnelt der Höchstpreisauktion in großen Teilen. Es muss lediglich noch das zweithöchste Gebot für die Auszahlungen ermittelt werden. Daher müssen nur geringfügig Änderungen vorgenommen werden. Diese wurden fett hervorgehoben, um ein zügiges Nachvollziehen zu ermöglichen.

Initialisierung

Bei einer Vickrey-Auktion gibt es zwei oder mehrere Bieter, die Gebote abgeben, sowie einen Auktionator, der dem Bieter mit dem höchsten Gebot den Zuschlag erteilt. Im Vergleich zur Höchstpreisauktion sind keine Änderungen notwendig:

role(a_1)

…

role(a_m)

role(auctioneer)

role(random)

val(0)

…

val(100)

init(initRound)

Auktionsverlauf

Der Verlauf der Auktion wird wie bei der Höchstpreisauktion in vier Phasen gegliedert. Diese bleiben bei der Vickrey-Auktion gleich:




legal(R, my_bid(P))


true(bettingRound) P 0




…



…



next(bid(R,P)) accept(bid(R,P))

next(bid(R,P)) bid(R,P)

next(clearingRound) does(a_1, my_bid(P1)) … does(a_m, my_bid(Pm))

next(finishedRound) does(auctioneer, clearing(R,P))

bestbid(P) true(bid(R,P)) outbid(P)


secondbestbid(P)

true(bid(R,P)) true(bestbid(P1)) P<P1 true(bid(R,P2)) P2<P


…



sees(R, call_for_bid) true(bettingRound)

sees(R1, bid_accepted(P)) accept(bid(R1,P))

sees(R, winner(R1,P))

does(auctioneer, clearing(R1,P1)) secondbestbid(P)

Auktionsende

Sobald die Auktion durch das Clearing des Auktionators beendet wurde, erhält der Meistbietende den Zuschlag. Seine Auszahlung ist abhängig von seiner Wertschätzung und dem Preis, den der Auktionator als Auszahlung erhält. Der Preis entspricht hierbei jedoch dem zweithöchstem Gebot und nicht dem Gebot des Gewinners der Auktion. Alle anderen Teilnehmer erhalten nichts:


goal(R1,V-P)

true(bid(R1,P1)) true(hasValue(R1,V)) true(bestbid(P1))

secondbestbid(P)

goal(R,0)



goal(auctioneer, P) true(secondbestbid(P))

3.1.3. Holländische Auktion

Initialisierung

Bei einer Holländischen Auktion gibt es einen oder mehrere Bieter, die eines der Gebote annehmen, die von einem Auktionator in absteigender Reihenfolge genannt werden. Der Bieter der zuerst ein Gebot annimmt erhält den Zuschlag und zahlt den genannten Preis:

role(a_1)

…

role(a_m)

role(auctioneer)

role(random)

val(0)

…

val(100)

init(auction(closed))

Auktionsverlauf

Der Verlauf der Auktion wird aufgrund der Parallelität der Gebotsabgabe und –annahme dieses Mal in nur drei Phasen eingeteilt. Zu Beginn ist die Auktion geschlossen (auction(closed)), um die Wertschätzungen der einzelnen Teilnehmer durch den random-Player festzulegen. Erst wenn diese vergeben und mitgeteilt wurden, ist die Auktion eröffnet (auction(opened)) und der Auktionator beginnt die Gebote zu nennen. Hat ein Teilnehmer ein Gebot akzeptiert, wird die Auktion beendet und der Zuschlag erteilt (auction(finished)):

accept(bid(P)) does(auctioneer, submitBid(P)) reject(P)

reject(P) true(bid(P1)) P1 P

legal(R, acceptBid(P))

true(auction(opened)) role(R) distinct(R, auctioneer)

distinct(R, random) true(bid(P))

legal(R, noop)


distinct(R, random)

legal(auctioneer, submitBid(P)) true(auction(opened)) P 0


true(auction(closed)) val(V1) … val(Vm)

next(B) accept(B)

next(auction(opened)) accept(B)

next(bid(P)) true(bid(P)) outbid

outbid accept(B)

next(auction(finished)) does(R, acceptBid(P))

next(winner(R,P)) does(R, acceptBid(P))


…


next(auction(opened)) does(random, set_values(V1,…,Vm))


…



…


sees(R, bid(P)) does(auctioneer, submitBid(P))

sees(R, bid_accepted(P)) accept(bid(P))

sees(R, bid_rejected(P)) reject(P)

sees(R, auction(finished)) auction(finished)

sees(R, winner(R1,P)) does(R1, acceptBid(P))

Auktionsende

Sobald die Auktion durch die Annahme eines Gebots geschlossen wurde, ist die Auktion beendet und der erste annehmende Teilnehmer erhält den Zuschlag. Seine Auszahlung ist abhängig von seiner Wertschätzung und dem Preis, den der Auktionator als Auszahlung erhält. Alle anderen Teilnehmer erhalten nichts:

terminal true(auction(finished))

goal(R1,V-P) true(winner(R1,P)) true(hasValue(R1,V))

goal(R,0) true(winner(R1,P)) distinct(R,R1) distinct(R, auctioneer)

goal(auctioneer, P) true(winner(R,P))

3.1.4. Englische Auktion

Zur Veranschaulichung wurde die Englische Auktion in [Thi09] als vereinfachtes Interaktionsprotokoll auf Basis der Modellierung der FIPA Spezifikation28 erstellt:

Abbildung 3: Interaktionsprotokoll Englische Auktion Quelle: [Thi09]

Angelehnt an diese Darstellung kann nun das GDL-II-Modell erstellt werden. Allerdings wird auf einen Timer verzichtet, sondern stattdessen die Terminierung durch den Auktionator offen gelassen. Statt des Timers wird daher eine Nachricht gesendet sobald die Auktion beendet wurde:

Initialisierung

Bei einer Englischen Auktion gibt es einen oder mehrere Bieter, die Gebote abgeben, sowie einen Auktionator, der dem Bieter mit dem höchsten Gebot nach einer angemessenen Zeit den Zuschlag erteilt:

role(a_1)

…

role(a_m)

role(auctioneer)

role(random)

val(0)

…

val(100)


28

Diese ist im Internet verfügbar. Vgl. [FIP01]

Auktionsverlauf

Der Auktionsverlauf ähnelt dem einer Holländischen Auktion. Allerdings läuft diese nun andersherum. Insbesondere die erlaubten Aktionen drehen sich um. Bezeichne RESERVE_PRICE den Reservationspreis des Auktionators unter diesem er kein Gebot annimmt. Dann beschreiben folgende Axiome den Verlauf der Auktion:

accept(bid(R,P)) does(R, my_bid(P)) reject(P)

reject(P) P

reject(P) true(bid(R,P1)) P P1

reject(P) does(R, my_bid(P1)) P P1

legal(R, my_bid(P))


distinct(R, random) P 0

legal(auctioneer, clearing(R,P)) true(bid(R,P)) true(auction(opened))

legal(auctioneer, noop) true(auction(opened))



next(B) accept(B)

next(auction(opened)) accept(B)

next(bid(R,P)) true(bid(R,P)) outbid

outbid accept(B)

next(auction(finished)) does(auctioneer, clearing(R,P))


…




…



…


sees(R, bid(R1,P)) does(R1, my_bid(P))

sees(R, bid_accepted(P)) accept(bid(R1,P))


sees(R, auction(finished)) auction(finished)

sees(R, best_price(P)) true(bid(R1,P))


Auktionsende

Sobald die Auktion durch das Clearing des Auktionators geschlossen wurde, ist die Auktion beendet und der Meistbietende erhält den Zuschlag. Seine Auszahlung ist abhängig von seiner Wertschätzung und dem Preis, den der Auktionator als Auszahlung erhält. Alle anderen Teilnehmer erhalten nichts:


goal(R1,V-P) true(bid(R1,P)) true(hasValue(R1,V))

goal(R,0) true(bid(R1,P)) distinct(R,R1) distinct(R, auctioneer)

goal(auctioneer, P) true(bid(R,P))

3.2. Zweiseitige Auktionen

Die Modellierung von zweiseitigen Auktionen ist grundsätzlich vergleichbar mit obigen Modellen. Allerdings müssen im Folgenden insbesondere Kauf- und Verkaufsgebote unterschieden werden.

3.2.1. Call Auction

Bei der Call Auction wird die Auktion nach einem zuvor festgelegtem Intervall beendet und ein Preis für alle Teilnehmer ermittelt. In diesem Modell wird dies durch eine Aktion des Auktionators umgesetzt. Das heißt der Auktionator wird nach Ablauf der Zeit die Auktion beenden. Da die Ermittlung des Preises dem Auktionator überlassen ist, wird die PRICING_POLICY(P) zunächst nicht näher spezifiziert und bleibt den Teilnehmern der Auktion verborgen. Jedoch wird im anschließenden Exkurs eine beispielhafte Möglichkeit diese Policy zu beschreiben vorgestellt. Außerdem wird davon ausgegangen, dass ein bestimmtes Gut gehandelt wird. Dies vereinfacht die Modellierung dahingehend, dass zu einer Gebotsabgabe neben dem Preis lediglich die Menge angegeben werden muss. Es entfällt also die Angabe, welches Produkt gehandelt werden möchte. Dies wäre selbstverständlich umsetzbar, dadurch würde das Modell jedoch unnötigerweise komplizierter, da die Versteigerung von mehreren unabhängigen Gütern auch als parallel laufende Auktionen mit jeweils einem Gut verstanden werden können.

Initialisierung

Die Rollen unterscheiden sich nicht von den anderen Auktionstypen. Allerdings übernimmt der Auktionator in unserem Modell die Rolle des Market Maker. Die Teilnehmer handeln folglich ihre Güter nicht direkt untereinander, sondern über den Market Maker, der die Liquidität bereitstellt:

role(a_1)

…

role(a_m)

role(auctioneer)

role(random)

val(0)

…

val(100)

init(initRound)

Auktionsverlauf

Analog zu den Auktionen mit verdeckter Gebotsabgabe wird der Verlauf der Auktion in vier Phasen gegliedert. Zur Vereinfachung des Models kann jeder Teilnehmer genau ein Kauf- und ein Verkaufsgebot abgeben:

legal(auctioneer, clearing(P)) PRICING_POLICY(P) true(clearingRound)

legal(auctioneer, endBettingRound) true(bettingRound)

legal(auctioneer, noop) true(bettingRound)

legal(R, my_bid(Q,P))


true(bettingRound) Q>0 P true(bid(R,Q1,P1))

legal(R, my_ask(Q,P))


true(bettingRound) Q>0 P true(ask(R,Q1,P1))



cleared(R,Q,P1,bid)

does(auctioneer, clearing(P1)) true(bid(R,Q,P)) P P1

cleared(R,Q,P1,ask)

does(auctioneer, clearing(P1)) true(ask(R,Q,P)) P P1

sum_bid(P1, Q1*P1+…+ Qm*P1)

cleared(a_1,Q1,P1,bid) … cleared(a_m,Qm,P1,bid)

sum_ask(P1, Q1*P1+…+ Qm*P1)

cleared(a_1,Q1,P1,ask) … cleared(a_m,Qm,P1,ask)


…



…



next(bettingRound) true(bettingRound) true(clearingRound)

next(clearingRound) does(auctioneer, endBettingRound)

next(finishedRound) does(auctioneer, clearing(P))

next(bid(R,Q,P)) does(R, my_bid(Q,P))

next(ask(R,Q,P)) does(R, my_ask(Q,P))

next(bid(R,Q,P)) true(bid(R,Q,P)) cleared(R,Q,P,D)

next(ask(R,Q,P)) true(ask(R,Q,P)) cleared(R,Q,P,D)

next(cleared(R,Q,P,D)) true(cleared(R,Q,P,D))


…


sees(auctioneer, bid(R,Q,P)) does(R, my_bid(Q,P))

sees(auctioneer, ask(R,Q,P)) does(R, my_ask(Q,P))

sees(R, bettingRound) does(random, set_values(V1,…,Vm))

sees(R, clearingRound) does(auctioneer, endBettingRound)

sees(R, finishedRound) does(auctioneer, clearing(P))

sees(R, quote(P)) does(auctioneer, clearing(P))

sees(R, cleared(Q,P,D)) cleared(R,Q,P,D)

sees(R, not_cleared(Q,P,bid)) bid(R,Q,P) true(finishedRound)

sees(R, not_cleared(Q,P,ask)) ask(R,Q,P) true(finishedRound)

Auktionsende

Die Auszahlungen zu bestimmen ist dieses Mal etwas komplexer, da der Auktionator mehrere Gebote akzeptiert und seine Auszahlung der Summe aller ausgeführten Aktionen entspricht:


goal(R1,Q1*(V-P)+Q2*(P-V)))

(true(cleared(R1,Q1,P,bid)) true(cleared(R1,Q2,P,ask)))

true(hasValue(R1,V)

goal(R,0)

true(cleared(R1,Q,P,D)) distinct(R,R1) distinct(R, auctioneer)

goal(auctioneer, VOL1-VOL2)

true(sum_bid(auctioneer,VOL1)) true(sum_ask(auctioneer,VOL2))

Exkurs: Pricing Policy

Wie im Abschnitt “Auktionstypen” bereits beschrieben, wird der Preis in der Regel so festgelegt, dass das Handelsvolumen maximal ist. Eine solche Pricing Policy lässt sich analog zu den oben beschriebenen Literalen „sum_ask“ und „sum_bid“ ableiten. Die GDL-II Beschreibung müsste demnach wie folgt ergänzt werden:

PRICING_POLICY(P) HIGHEST_VOLUME(P)

HIGHEST_VOLUME(P) true(sum_quotes(P,VOL)) betterSum(P,VOL)

betterSum(P1,VOL)

true(sum_quotes(P1,VOL)) true(sum_quotes(P,VOL1)) VOL1 VOL

sum_quotes(P1,VOL_BID+VOL_ASK)

true(vol_bid(P1,VOL_BID)) true(vol_ask(P1,VOL_ASK))

vol_bid(P1,Q1*P1+…+Qm*P1)

accept(bid(a_1,Q1,P),P1) … accept(bid(a_m,Qm,P),P1)

vol_ask(P1,Q1*P1+…+Qm*P1)

accept(ask(a_1,Q1,P),P1) … accept(ask(a_m,Qm,P),P1)

accept(bid(R,Q,P),P1) true(bid(R,Q,P)) P P1

accept(ask(R,Q,P),P1) true(ask(R,Q,P)) P P1

3.2.2. Continuous Double Auction (CDA)

Die CDA stellt aufgrund ihrer großen Flexibilität und Dynamik die größte Herausforderung hinsichtlich der Modellierung dar. Jeder Teilnehmer kann beliebig Gebote abgeben, welche sofort ausgeführt werden, sobald sie sich überschneiden. Insbesondere sind bei diesem Auktionstyp auch Teilausführungen möglich. Analog zur Call Auction wird genau ein bestimmtes Gut gehandelt.

Initialisierung

Die Rollen unterscheiden sich nicht von den anderen Auktionstypen. Allerdings übernimmt der Auktionator in unserem Modell die Rolle des Market Maker. Die Teilnehmer handeln also ihre Güter nicht direkt untereinander, sondern über den Market Maker, der die Liquidität bereitstellt:

role(a_1)

…

role(a_m)

role(auctioneer)

role(random)

val(0)

…

val(100)


Auktionsverlauf

Die Auktion wird erneut in drei Phasen gegliedert. Zunächst werden wieder die Wertschätzungen der Teilnehmer ermittelt. Anschließend wird solange gehandelt bis der Auktionator die Auktion beendet. Zusätzlich zur Wertschätzung der Teilnehmer werden bei dieser Auktion die Umsätze „C“ (für Cashflow) mitverfolgt um später die Auszahlungen bestimmen zu können:

minimum(Q1,Q2,Q1) Q1 Q2

minimum(Q1,Q2,Q2) Q1 Q2

legal(auctioneer, match(R1,Q1,P1,R2,Q2,P2,Q,P))

true(auction(opened))

((true(ask(R1,Q1,P1)) true(bid(R2,Q2,P2)) minimum(Q1,Q2,Q)

P1 P2 P1 P P P2)

(does(R1, accept(bid(R2,Q2,P2))) Q1=Q2=Q P1=P2=P)

(does(R2, accept(ask(R1,Q1,P1))) Q1=Q2=Q P1=P2=P))

legal(auctioneer, endBettingRound) true(auction(opened))



distinct(R, auctioneer) distinct(R, random)

true(auction(opened)) Q>0 P




legal(R1, accept(bid(R,Q,P)))

distinct(R, auctioneer) distinct(R, random) distinct(R, R1)

true(auction(opened)) true(bid(R,Q,P))

legal(R1, accept(ask(R,Q,P)))


true(auction(opened)) true(ask(R,Q,P))



cleared(ask(R1,Q1,P1))

does(auctioneer, match(R1,Q1,P1,R2,Q2,P2,Q,P))

cleared(bid(R2,Q2,P2))


next(hasValue(a_1,V1,0)) does(random, set_values(V1,…,Vm))

…

next(hasValue(a_m,Vm,0)) does(random, set_values(V1,…,Vm))

next(hasValue(a_1,V1,C)) true(hasValue(a_1,V1,C))

…

next(hasValue(a_m,Vm,C)) true(hasValue(a_m,Vm,C))

next(hasValue(R1,V,C1+Q*(P-V)))

true(hasValue(R1,V,C1)) does(auctioneer,

match(R1,Q1,P1,R2,Q2,P2,Q,P))

next(hasValue(R2,V,C2-Q*(P-V)))




next(auction(opened)) true(auction(opened)) true(auction(finished))

next(auction(finished)) does(auctioneer, endBettingRound)



next(bid(R,Q,P)) true(bid(R,Q,P)) cleared(bid(R,Q,P))

next(ask(R,Q,P)) true(ask(R,Q,P)) cleared(ask(R,Q,P))

next(ask(R1,Q1-Q,P1))

true(ask(R1,Q1,P1)) does(auctioneer, match(R1,Q1,P1,R2,Q2,P2,Q,P))

Q1 Q

next(bid(R2,Q2-Q,P2))

true(bid(R2,Q2,P2)) does(auctioneer, match(R1,Q1,P1,R2,Q2,P2,Q,P))

Q2 Q


…


sees(R1, bid(R,Q,P)) does(R, my_bid(Q,P))

sees(R1, ask(R,Q,P)) does(R, my_ask(Q,P))

sees(R, auction(opened)) does(random, set_values(V1,…,Vm))

sees(R, cleared(O)) true(cleared(O))

sees(R, auction(finished)) does(auctioneer, endBettingRound)

Auktionsende

Aufgrund der Dynamik erfolgte die Berechnung der Auszahlungen bereits im Auktionsverlauf. In diesem Abschnitt werden die Ergebnisse dieser Berechnungen nur noch mitgeteilt. In diesem Modell haben der Auktionator und der random-Player lediglich unterstützende Funktionen und daher keine Auszahlungen:


goal(R,C)

true(hasValue(R,V,C)) distinct(R,auctioneer) distinct(R,random)

4. Korrektheitsprüfung der Modelle Nachdem die formale Beschreibung der Auktionen abgeschlossen wurde, werden diese einer Korrektheitsprüfung unterzogen. Zunächst werden die Beschreibungen gegen die zuvor gelieferte Spezifikation geprüft (Verifikation). Anschließend wird kontrolliert, ob die Beschreibung tatsächlich das gewünschte Verhalten der Auktionen wiederspiegelt (Validierung). Bei Validierung der einseitigen Auktionsmodelle wird lediglich auf wesentliche Merkmale eingegangen, da die Modelle in Teilen große Analogien zu den ausführlich beschriebenen, zweiseitigen Auktionen aufweisen, die nicht explizit wiederholt werden müssen. Die umfangreiche Korrektheitsprüfung erfolgt dann im Anschluss für die Call Auction und die Continuous Double Auction. Diese Auktionstypen sind besonders relevant für Börsen.

4.1. Höchstpreisauktion

4.1.1. Verifikation

Bei der Verifikation wird die Beschreibung gegen die zuvor beschriebene Spezifikation der GDL-II geprüft. Insbesondere gilt es zu beachten die gegebenen Restriktionen nicht zu verletzen:


Die Rekursionsrestriktion ist nur relevant, falls der head einer Datalog Regel auf einem Kreis mit einem Literal des dazugehörigen body liegt.29 Dies ermöglicht eine zügige Überprüfung, da diese Restriktion nicht verletzt sein kann, solange es keinen Kreis gibt.

Bei der Initialisierung der Höchstpreisauktion gibt es keine Datalog Regeln. Dementsprechend kann es auch keinen Kreis geben. OK

Die legal-Relationen tauchen in unserer Beschreibung lediglich im head einer Regel auf. Auch hier kann es also keinen Kreis geben. OK

Das „accept“-Statement besteht lediglich aus der does-Relation, der true-Relation. Da diese Relationen gemäß den GDL-Restriktionen lediglich im body auftauchen dürfen, kann es auch hier keinen Kreis geben. OK

Das „bestbid“-Statements könnte auf einem Kreis mit dem „legal“-Statement liegen. Dies ist jedoch nicht möglich, da die legal-Relationen, wie oben bereits festgestellt, lediglich im head auftauchen. OK

Es könnte jedoch das „outbid“-Statement auf einem Kreis mit dem „bestbid“-Statement liegen. Bei genauer Beobachtung stellt man jedoch fest, dass es keinen Pfad von „bestbid“ zu „outbid“, sondern lediglich anders herum. OK

Die next-Relation taucht gemäß den GDL-Restriktionen lediglich im head auf und kann demzufolge auf keinem Kreis liegen.

Gemäß der Erweiterung der GDL-Restriktionen aus der GDL-II Spezifikation gilt selbiges auch für die sees-Relation. OK

Die terminal- und goal-Relationen tauchen lediglich im head auf. OK Die Prüfung ergibt, dass die Rekursionsrestriktion nicht verletzt sein kann, da es im Abhängigkeitsgraphen der GDL-II-Beschreibung keinen Kreis gibt.

GDL Restriktionen

Die GDL-Restriktionen dürfen in keinem Fall verletzt sein, um die Spezifikation zu erfüllen. Da unsere Beschreibung in GDL-II erfolgte, müssen die Restriktionen unter Hinzunahme der Erweiterungen herangezogen werden. Diese finden sich in den Abschnitten „GDL Restriktionen“ (Seite 10) und „Erweiterung der GDL Restriktionen“ (Seite 14).

Die role-Relation wird in unserer Beschreibung lediglich zur Initialisierung im head ohne body verwendet. OK

Die init-Relation wird ebenfalls lediglich im head ohne body verwendet. OK

Die true-Relation wird niemals im head verwendet. OK

Im Gegensatz dazu werden die next- und die sees-Relation nur im head verwendet. OK

Die does-Relation wird nur im body eingesetzt. Zudem existiert kein Pfad zu einem goal, terminal oder legal Knoten. OK

Die Prüfung ergibt, dass auch die (erweiterten) GDL-Restriktionen nicht verletzt sind.

Die Relationen wurden in der Beschreibung gemäß der Spezifikation eingesetzt. Es wurden dabei insbesondere keinerlei Restriktionen der Spezifikation verletzt. Demzufolge ist die Beschreibung hinsichtlich der GDL-II-Spezifikation korrekt.

29

Vgl. Abschnitt „Rekursionsrestriktion“ in Kapitel „‎2.2.3 Erweiterung der Definitionen“

4.1.2. Validierung

Bei der Validierung kommt es darauf an zu überprüfen, ob die Beschreibung sich tatsächlich wie gewünscht verhält. Da die Rahmengestaltung sich stark mit den zweiseitigen Auktionen ähnelt, wird an dieser Stelle auf eine Prüfung verzichtet und lediglich auf die entsprechenden Abschnitte im späteren Kapitel verwiesen.

Auktionsmechanismus

Gebotsabgabe

Die Gebotsabgabe ist bei der Höchstpreisauktion einseitig. Von jedem Teilnehmer wird dabei genau ein Gebot abgegeben. Sobald ein Gebot abgegeben wurde, wird dieses mittels


akzeptiert. Die Gebote sind bei einer Höchstpreisauktion werden verdeckt abgegeben. Bei den Informationsflüssen gilt es demnach insbesondere zu beachten, dass die verdeckte Gebotsabgabe korrekt umgesetzt wurde. Lediglich der Auktionator darf diese Gebote kennen, um auf deren Basis den Preis zu bestimmen. Dies ist durch folgende Regel sichergestellt:


Andere Teilnehmer können aufgrund einer fehlenden entsprechenden sees-Relation keine Informationen über die Gebote der anderen Teilnehmer erhalten. Die Gebotsabgabe funktioniert demnach wie gewünscht und ist somit korrekt.

Clearing

Das Clearing erfolgt unmittelbar nachdem alle Teilnehmer ihre Gebote abgegeben haben. Die Rundensteuerung sorgt dafür, dass nach der Gebotsabgabe von allen Teilnehmern die Clearing-Runde eingeläutet wird. Erst dann hat der Auktionator die Möglichkeit, dass Clearing einzuleiten indem er mittels



Das beste Gebot annimmt. Das beste Gebot wird dabei mittels bestbid(P) true(bid(R,P)) outbid(P)


bestimmt. Das ausgeführte Gebot wird allen Teilnehmern durch sees(R, winner(R1,P)) does(auctioneer, clearing(R1,P))

mitgeteilt. Das Clearing funktioniert demnach wie gewünscht und ist somit korrekt.

Auszahlungen

Bei der Auszahlung gibt es genau einen Bieter, dessen Gebot angenommen wurde, und den Auktionator, bei denen Geldeinheiten fließen. Alle anderen erhalten die Auszahlung „0“:

goal(R1,V-P) true(bid(R1,P)) true(hasValue(R1,V)) true(bestbid(P))

goal(R,0)



goal(auctioneer, P) true(bestbid(P))

Die Auszahlungen entsprechen der Auszahlung einer realen Höchstpreisauktion und sind somit korrekt.

Die Beschreibung verhält sich in allen Punkten wie gewünscht und ist somit auch hinsichtlich der gewünschten Funktionalität als korrekt anzusehen.

4.2. Vickrey-Auktion

4.2.1. Verifikation




Bei der Initialisierung der Vickrey-Auktion gibt es keine Datalog Regeln. Dementsprechend kann es auch keinen Kreis geben. OK


Das „accept“-Statement besteht lediglich aus der does-Relation, der true-Relation. Da diese Relationen gemäß den GDL-Restriktionen lediglich im body auftauchen dürfen, kann es auch hier keinen Kreis geben. OK

Das „bestbid“-Statements könnte auf einem Kreis mit dem „legal“-Statement liegen. Dies ist jedoch nicht möglich, da die legal-Relationen, wie oben bereits festgestellt, lediglich im head auftauchen. OK

Das „secondbestbid“-Statement besteht lediglich aus true-Relationen und Fakten. Analog zu obiger Begründung kann es demnach keinen Kreis geben. OK

Es könnte jedoch das „outbid“-Statement auf einem Kreis mit dem „bestbid“-Statement liegen. Bei genauer Beobachtung stellt man jedoch fest, dass es keinen Pfad von „bestbid“ zu „outbid“, sondern lediglich anders herum. OK




GDL Restriktionen


30









4.2.2. Validierung


Auktionsmechanismus

Gebotsabgabe

Die Gebotsabgabe ist bei der Vickrey-Auktion einseitig. Von jedem Teilnehmer wird dabei genau ein Gebot abgegeben. Sobald ein Gebot abgegeben wurde, wird dieses mittels


akzeptiert. Die Gebote sind bei einer Vickrey-Auktion werden verdeckt abgegeben. Bei den Informationsflüssen gilt es demnach insbesondere zu beachten, dass die verdeckte Gebotsabgabe korrekt umgesetzt wurde. Lediglich der Auktionator darf diese Gebote kennen, um auf deren Basis den Preis zu bestimmen. Dies ist durch folgende Regel sichergestellt:



Clearing

Das Clearing erfolgt unmittelbar nachdem alle Teilnehmer ihre Gebote abgegeben haben. Die Rundensteuerung sorgt dafür, dass nach der Gebotsabgabe von allen Teilnehmern die Clearing-Runde eingeläutet wird. Erst dann hat der Auktionator die Möglichkeit, dass Clearing einzuleiten indem er mittels



Das beste Gebot annimmt. Das beste Gebot wird dabei mittels bestbid(P) true(bid(R,P)) outbid(P)


bestimmt. Die Besonderheit der Vickrey-Auktion besteht jedoch darin, dass der Meistbietende lediglich den Preis des zweithöchsten Gebots zahlen muss. Dieser Preis wird mittels

secondbestbid(P)

true(bid(R,P)) true(bestbid(P1)) P<P1 true(bid(R,P2)) P2<P

ermittelt. Dementsprechend muss auch der Informationsfluss angepasst werden. sees(R, winner(R1,P))

does(auctioneer, clearing(R1,P1)) secondbestbid(P)

Das Clearing funktioniert demnach wie gewünscht und ist somit korrekt.

Auszahlungen

Bei der Auszahlung gibt es genau einen Bieter, dessen Gebot angenommen wurde, und den Auktionator, bei denen Geldeinheiten fließen. Alle anderen erhalten die Auszahlung „0“. Die Tatsache, dass der Ausführungspreis dem zweithöchsten Gebot entspricht, erfordert lediglich eine geringfügige Anpassung:

goal(R1,V-P)

true(bid(R1,P1)) true(hasValue(R1,V)) true(bestbid(P1))

secondbestbid(P)

goal(R,0)



goal(auctioneer, P) true(secondbestbid(P))

Die Auszahlungen entsprechen der Auszahlung einer realen Vickrey-Auktion und sind somit korrekt.


4.3. Holländische Auktion

4.3.1. Verifikation




Bei der Initialisierung der Holländischen Auktion gibt es keine Datalog Regeln. Dementsprechend kann es auch keinen Kreis geben. OK


Das „reject“-Statement besteht lediglich aus der true-Relation und einem Faktum. Hierbei kann es keinen Kreis geben. OK

Das „accept“-Statement besteht lediglich aus einer does-Relation und dem „reject“-Statement. Die does-Relation taucht niemals im head auf und kann daher auf keinem Kreis liegen. Ebenso wurde im vorangegangenen Punkt bereits gezeigt, dass auch „reject“ auf keinem Kreis liegen kann. Demzufolge liegt auch das „accept“-Statement auf keinem Kreis. OK

31





GDL Restriktionen









4.3.2. Validierung


Auktionsmechanismus

Gebotsabgabe

Die Gebotsabgabe ist bei der holländischen Auktion einseitig. Der Auktionator nennt fallende Gebote mittels

legal(auctioneer, submitBid(P)) true(auction(opened)) P 0

Dabei wird sichergestellt, dass ein Preis größer gleich null genannt wird. Dieses Gebot wird jedoch erst durch das accept-Statement angenommen, welches prüft, ob das neue Gebot tatsächlich unter allen bisherigen liegt.

accept(bid(P)) does(auctioneer, submitBid(P)) reject(P)

reject(P) true(bid(P1)) P1 P

Sollte es das erste überhaupt genannte Gebot sein, wird es ebenfalls akzeptiert, da true(bid(P1)) falsch ist und reject nicht wahr wird. Die folgenden next-Statements stellen dabei sicher, dass immer genau ein Gebot, nämlich das Beste, wahr ist:

next(B) accept(B)

next(bid(P)) true(bid(P)) outbid

outbid accept(B)

Dieses kann dann von den Teilnehmern bei Interesse angenommen werden legal(R, acceptBid(P))


distinct(R, random) true(bid(P))

legal(R, noop)


distinct(R, random)

wobei die noop-Operation ihm auch erlaubt ein weiteres Gebot des Auktionators abzuwarten. Die Gebote sind bei einer Holländischen Auktion öffentlich. Dementsprechend müssen diese den Teilnehmern durch entsprechende sees-Statements mitgeteilt werden:

sees(R, bid(P)) does(auctioneer, submitBid(P))

sees(R, bid_accepted(P)) accept(bid(P))


Für jedes abgegebene Gebot erhalten die Teilnehmer zwei Informationen: Einmal erfahren sie das Gebot und in einer zweiten Nachricht erfahren sie ob dieses Gebot akzeptiert wurde oder nicht. Die Gebotsabgabe funktioniert demnach wie gewünscht und ist somit korrekt.

Clearing

Das Clearing erfolgt unmittelbar nachdem der erste Teilnehmer ein Gebot angenommen hat. Die Rundensteuerung sorgt dafür, dass dies die Auktion beendet. Das Clearing besteht in diesem Fall lediglich darin alle Teilnehmer über die Annahme des Gebots zu akzeptieren:

sees(R, winner(R1,P)) does(R1, acceptBid(P))


Auszahlungen

Bei der Auszahlung gibt es genau einen Bieter, der ein Gebot angenommen hat und den Auktionator, bei denen Geldeinheiten fließen. Alle anderen erhalten die Auszahlung „0“:

goal(R1,V-P) true(winner(R1,P)) true(hasValue(R1,V))

goal(R,0) true(winner(R1,P)) distinct(R,R1) distinct(R, auctioneer)

goal(auctioneer, P) true(winner(R,P))

Die Auszahlungen entsprechen der Auszahlung einer realen Holländischen Auktion und sind somit korrekt.


4.4. Englische Auktion

4.4.1. Verifikation




Bei der Initialisierung der Englischen Auktion gibt es keine Datalog Regeln. Dementsprechend kann es auch keinen Kreis geben. OK


Das „reject“-Statement besteht entweder aus der true-Relation, der does-Relation und/oder einem Faktum. Hierbei kann es keinen Kreis geben. OK

Das „accept“-Statement besteht lediglich aus einer does-Relation und dem „reject“-Statement. Die does-Relation taucht niemals im head auf und kann daher auf keinem Kreis liegen. Ebenso wurde im vorangegangenen Punkt bereits gezeigt, dass auch „reject“ auf keinem Kreis liegen kann. Demzufolge liegt auch das „accept“-Statement auf keinem Kreis. OK




GDL Restriktionen









32


4.4.2. Validierung


Auktionsmechanismus

Gebotsabgabe

Die Gebotsabgabe ist bei der englischen Auktion einseitig. Der Bieter nennen aufsteigende Gebote mittels

legal(R, my_bid(P))


distinct(R, random) P 0

Dabei wird sichergestellt, dass ein Preis größer gleich null genannt wird. Dieses Gebot wird jedoch erst durch das accept-Statement angenommen, welches prüft, ob das neue Gebot tatsächlich das höchste ist und über dem Reservationspreis des Auktionators liegt.

accept(bid(R,P)) does(R, my_bid(P)) reject(P)

reject(P) P

reject(P) true(bid(R,P1)) P P1

reject(P) does(R, my_bid(P1)) P P1

Die folgenden next-Statements stellen dabei sicher, dass immer genau ein Gebot, nämlich das Beste, wahr ist:

next(B) accept(B)

next(bid(R,P)) true(bid(R,P)) outbid

outbid accept(B)

Dieses kann dann vom Auktionator bei Interesse angenommen werden legal(auctioneer, clearing(R,P)) true(bid(R,P)) true(auction(opened))


wobei die noop-Operation ihm auch erlaubt weitere Gebote abzuwarten. Die Gebote sind bei einer Englischen Auktion öffentlich. Dementsprechend müssen diese den Teilnehmern durch entsprechende sees-Statements mitgeteilt werden:

sees(R, bid(R1,P)) does(R1, my_bid(P))

sees(R, bid_accepted(P)) accept(bid(R1,P))


sees(R, best_price(P)) true(bid(R1,P))

Für jedes abgegebene Gebot erhalten die Teilnehmer zwei Informationen: Einmal erfahren sie das Gebot und in einer zweiten Nachricht erfahren sie ob dieses Gebot akzeptiert wurde oder nicht. Zusätzlich sind sie durch die letzte Regel stets über das aktuell beste Gebot informiert. Die Gebotsabgabe funktioniert demnach wie gewünscht und ist somit korrekt.

Clearing

Das Clearing erfolgt unmittelbar nachdem der Auktionator ein Gebot angenommen hat. Die Rundensteuerung sorgt dafür, dass dies die Auktion beendet. Das Clearing besteht in diesem Fall lediglich darin alle Teilnehmer über die Annahme des Gebots zu akzeptieren:



Auszahlungen

Bei der Auszahlung gibt es genau einen Bieter, der ein Gebot angenommen hat und den Auktionator, bei denen Geldeinheiten fließen. Alle anderen erhalten die Auszahlung „0“:

goal(R1,V-P) true(bid(R1,P)) true(hasValue(R1,V))

goal(R,0) true(bid(R1,P)) distinct(R,R1) distinct(R, auctioneer)

goal(auctioneer, P) true(bid(R,P))

Die Auszahlungen entsprechen der Auszahlung einer realen Englischen Auktion und sind somit korrekt.


4.5. Call Auction

4.5.1. Verifikation




Bei der Initialisierung der Call Auction gibt es keine Datalog Regeln. Dementsprechend kann es auch keinen Kreis geben. OK


Das „cleared“-Statement besteht lediglich aus der does-Relation, der true-Relation und einem Faktum. Da diese Relationen gemäß den GDL-Restriktionen lediglich im body auftauchen dürfen, kann es auch hier keinen Kreis geben. OK

Die „sum_bid/ask“-Statements könnten theoretisch auf einem Kreis mit dem „cleared“-Statement liegen. Dies ist jedoch nicht der Fall OK




GDL Restriktionen

Die GDL-Restriktionen dürfen in keinem Fall verletzt sein, um die Spezifikation zu erfüllen. Da unsere Beschreibung in GDL-II erfolgte, müssen die Restriktionen unter Hinzunahme der Erweiterungen herangezogen werden. Diese finden sich in den Abschnitten „GDL Restriktionen“ (Seite 10) und „Erweiterung der GDL Restriktionen“ (Seite 14). 33









4.5.2. Validierung

Bei der Validierung kommt es darauf an zu überprüfen, ob die Beschreibung sich tatsächlich wie gewünscht verhält. Insbesondere werden daher die Rahmengestaltung, der Auktionsmechanismus und die Auszahlungen überprüft.

Rahmengestaltung

Wertschätzungen

Zur Rahmengestaltung gehört insbesondere die Festlegung der Wertschätzungen. Die entscheidende Regel hierbei ist folgende legal-Relation:



Sie überlässt dem random-Player die Wahl von m Werten. Durch die anfänglichen Terme wurde festgelegt, dass val(V) einen Wert zwischen 0 und 100 beinhalten kann. Dies entspricht dem gewünschten Intervall. Die Werte werden ermittelt, sobald der random-Player seinen Zug ausführt. Gemäß der Spezifikation erfolgt die Wahl zufällig und ist gleichverteilt. Im selben Schritt werden die Werte den Playern durch


…


zugeordnet. Jeder erhält somit einen unabhängigen Wert gemäß dem Independent-private-value-model. Dieser bleibt außerdem durch folgende Regeln immer gleich:


…


Dieser Wert ist aufgrund von sees(a_1, V1) does(random, set_values(V1,…,Vm))

…


privat. Die Regeln beschreiben, dass jeder Teilnehmer nur seine eigene Wertschätzung als Information bekommt. Alle anderen Wertschätzungen sind unbekannt. Dieser Abschnitt der Beschreibung verhält sich demnach wie gewünscht und ist somit korrekt.

Rundensteuerung

Auch die Steuerung durch Runden der Auktion gehört zur Rahmengestaltung. Sie sollen sicherstellen, dass erst die Wertschätzungen ermittelt werden, dann die Gebote abgegeben und zum Schluss das Clearing durchgeführt wird. Da durch

init(initRound)

die Initialisierungsrunde begonnen wird, kann die oben beschriebene Festlegung der Wertschätzungen erfolgen.


stellt sicher, dass dies genau einmal passiert und mit der Festsetzung der Wertschätzungen, die Auktion eröffnet wird. Denn initRound ist ab sofort nicht mehr wahr. Durch

next(bettingRound) true(bettingRound) true(clearingRound)

wird sichergestellt, dass die Auktion eröffnet bleibt und nicht durch die Gebote der Teilnehmer beendet werden kann. Nur der Auktionator kann die Auktion beenden

legal(auctioneer, endBettingRound) true(bettingRound)

legal(auctioneer, noop) true(bettingRound)

die noop-Operation ermöglicht ihm dabei auch unter Zugzwang nicht die Auktion vorzeitig beenden zu müssen. Sobald er jedoch die Auktion beendet, sorgt

next(clearingRound) does(auctioneer, endBettingRound)

dafür, dass bettingRound nicht mehr wahr ist. Gebote können ab sofort nicht mehr abgegeben werden. Stattdessen kann nun der Auktionator den Preis ermitteln:

legal(auctioneer, clearing(P)) PRICING_POLICY(P) true(clearingRound)

Erst durch diese Aktion wird die Auktion durch next(finishedRound) does(auctioneer, clearing(P))

beendet. In diesem Zustand können keine Spielzüge mehr ausgeführt werden und der Endzustand wird erreicht:


Die jeweiligen Auslöser einer neuen Runde führen parallel zu einem Informationsfluss an alle Spieler, die durch

sees(R, bettingRound) does(random, set_values(V1,…,Vm))

sees(R, clearingRound) does(auctioneer, endBettingRound)

sees(R, finishedRound) does(auctioneer, clearing(P))

Kenntnis darüber erlangen in welcher Runde sie sich befinden.

Die Steuerung über die Runden funktioniert demnach wie gewünscht und ist somit korrekt.

Auktionsmechanismus

Gebotsabgabe

Die Gebotsabgabe ist bei der Call Auction zweiseitig. Ein Gebot kann dabei von jedem Teilnehmer abgegeben werden und entweder ein Kauf- oder Verkaufsangebot sein. Genau dies wird durch



true(bettingRound) Q>0 P true(bid(R,Q1,P1))



true(bettingRound) Q>0 P true(ask(R,Q1,P1))

beschrieben. Dabei bezeichnet Q die Menge und P den Preis des Gebots. Eine Menge kleiner gleich null ergibt keinen Sinn und wurde daher ausgeschlossen. Ebenso bedeutet ein negativer Preis

lediglich, dass die Fließrichtung des Gutes umgekehrt wird. Dies wird bereits durch die zwei Gebotstypen dargestellt, weshalb auch ein negativer Preis ausgeschlossen wird. Zudem wurde zur Vereinfachung der Beschreibung die Anzahl eines Bieters auf je ein Kauf- und Verkaufsgebot beschränkt. Dies wird durch das letzte Literal in den Regeln sichergestellt. Der Ausdruck „ask(R,Q1,P1)” ist genau dann wahr, wenn zu einem beliebigen vorherigen Zeitpunkt ein Verkaufsgebot von R abgegeben wurde. Dies wird durch die Regeln



sichergestellt. Ein Gebot verliert erst dann seine Gültigkeit, wenn es ausgeführt wurde. Dies ist jedoch nur bei Auktionsende möglich, wenn ohnehin keine Gebote mehr abgegeben werden können, denn zu diesem Zeitpunkt ist true(bettingRound) nicht mehr wahr. Die distinct-Klauseln sind notwendig, da der Auktionator und der random-Player nicht berechtigt sind Gebote abzugeben. Die Gebote sind bei einer Call Auction verdeckt. Bei den Informationsflüssen gilt es demnach insbesondere zu beachten, dass die verdeckte Gebotsabgabe korrekt umgesetzt wurde. Lediglich der Auktionator darf diese Gebote kennen, um auf deren Basis den Preis zu bestimmen. Dies ist durch folgende Regel sichergestellt:

sees(auctioneer, bid(R,Q,P)) does(R, my_bid(Q,P))

sees(auctioneer, ask(R,Q,P)) does(R, my_ask(Q,P))


Clearing

Der Preismechanismus, sowie die Sichtbarkeit dieser Information sind im Allgemeinen nicht festgelegt. Allerdings wurde in dieser Beschreibung ein nicht-öffentlicher Mechanismus geplant, der den Preis derart bestimmt, dass das Handelsvolumen maximal ist. Dieser Preis muss dann für alle gelten. Alle passenden Gebote werden anschließend ausgeführt. Die im Exkurs beschriebenen Regeln

HIGHEST_VOLUME(P) true(sum_quotes(P,VOL)) betterSum(P,VOL)

betterSum(P1,VOL)

true(sum_quotes(P1,VOL)) true(sum_quotes(P,VOL1)) VOL1 VOL

beschreiben genau das. Der Preis P mit dem maximalen Handelsvolumen wurde gefunden, wenn es keinen anderen Preis mit höherem Handelsvolumen gibt. Dabei addiert sum_quotes(P,VOL) lediglich die Handelsvolumina der bid- und ask-Seite, die jeweils durch vol_bid(P1,Q1*P1+…+Qm*P1) bzw. vol_ask(P1,Q1*P1+…+Qm*P1) berechnet werden. Diese wiederum addieren jeweils das Ausführungsvolumen eines Gebotes welches zum Preis P1 durchgeführt werden würde. Da keiner dieser Klauseln im Rahmen von sees-Relationen auftauchen, sind sie für niemanden sichtbar und dementsprechend nicht-öffentlich. Wenn der Preis ermittelt wurde und der Auktionator zum gefundenen Preis P1 das Clearing einleitet, wird durch

cleared(R,Q,P,bid)

does(auctioneer, clearing(P1)) true(bid(R,Q,P)) P P1

bzw. cleared(R,Q,P,ask)

does(auctioneer, clearing(P1)) true(ask(R,Q,P)) P P1

sichergestellt, dass alle passenden Gebote ausgeführt werden können. Ein Kaufgebot (Verkaufsgebot) passt, wenn sein Preis P über (unter) dem Ausführungspreis P1 liegt. Nicht-ausgeführte Gebote bleiben durch

next(bid(R,Q,P)) true(bid(R,Q,P)) cleared(R,Q,P,D)


erhalten, wohingegen ausgeführte Gebote ihre Gültigkeit mangels einer entsprechenden next-Relation verlieren. Diese werden zur späteren Berechnung der Auszahlungen durch

sum_bid(P1, Q1*P1+…+ Qm*P1)

cleared(a_1,Q1,P1,bid) … cleared(a_m,Qm,P1,bid)

sum_ask(P1, Q1*P1+…+ Qm*P1)

cleared(a_1,Q1,P1,ask) … cleared(a_m,Qm,P1,ask)

aufaddiert. Dabei entspricht diese Summe dem zuvor berechneten Handelsvolumen vol_bid(P,VOL). Diese Redundanz ist notwendig, da grundsätzlich auch eine andere Pricing Policy möglich ist, die ggf. ohne vol_bid(P,VOL) auskommt. Der ermittelte Preis wird durch

sees(R, quote(P)) does(auctioneer, clearing(P))

allen mitgeteilt. Ebenso erfahren alle Teilnehmer ob ihre Gebote ausgeführt wurden oder nicht: sees(R, cleared(Q,P,D)) cleared(R,Q,P,D)

sees(R, not_cleared(Q,P,bid)) bid(R,Q,P) true(finishedRound)

sees(R, not_cleared(Q,P,ask)) ask(R,Q,P) true(finishedRound)

Lediglich die nicht-ausgeführten Gebote sind bei Auktionsende noch gültig. Daher kann dies zur Ermittlung der nicht-ausgeführten Gebote verwendet werden. Das Clearing funktioniert demnach wie gewünscht und ist somit korrekt.

Auszahlungen

Da jeder Teilnehmer maximal ein Kauf- und ein Verkaufsgebot abgeben kann, ist die Ermittlung der Auszahlungen trivial. Es muss lediglich unterschieden werden, ob ein, zwei oder kein Gebot ausgeführt wurde. Durch

goal(R1,Q1*(V-P)+Q2*(P-V)))

(true(cleared(R1,Q1,P,bid)) true(cleared(R1,Q2,P,ask)))

true(hasValue(R1,V)

Kann die Auszahlung in einem Schritt berechnet werden. Dabei wird zunächst geprüft, ob Kauf- oder Verkaufsgebote durchgeführt wurden, um sie anschließend durch Q1*(V-P)+Q2*(P-V)) zu konsolidieren. Dabei entspricht Q1 der gekauften Menge des Gutes und Q2 der verkauften Menge des Gutes. P ist der Ausführungspreis und V entspricht der Wertschätzung. Ein Teilnehmer bei dem keines seiner Gebote ausgeführt wurde, erhält die Auszahlung null:

goal(R,0)

true(cleared(R1,Q,P,D)) distinct(R,R1) distinct(R, auctioneer)

durch distinct(R,R1) wird sichergestellt, dass R nicht zu den Teilnehmern gehört dessen Gebote ausgeführt wurden. Der Auktionator muss für alle Verkaufsgebote aufkommen, verdient jedoch an den Kaufgeboten. Seine Auszahlung ist also vom entsprechenden Verhältnis abhängig und kann durchaus negativ sein:

goal(auctioneer, VOL1-VOL2)

true(sum_bid(auctioneer,VOL1)) true(sum_ask(auctioneer,VOL2))

Hier kommen die entsprechenden sum_bid/ask Klauseln zum Einsatz. Die Auszahlungen entsprechen der Auszahlung einer realen Call Auction und sind somit korrekt.


4.6. Continuous Double Auction

4.6.1. Verifikation

Analog zur obigen Verifikation wird die Beschreibung gegen die zuvor beschriebene Spezifikation der GDL-II geprüft. Insbesondere gilt es zu beachten die gegebenen Restriktionen nicht zu verletzen:



Bei der Initialisierung der CDA gibt es keine Datalog Regeln. Dementsprechend kann es auch keinen Kreis geben. OK

Das „minimum“-Statement besteht lediglich aus einem Faktum. Hier kann es keinen Kreis geben. OK


Das „cleared“-Statement besteht lediglich aus der does-Relation. Da diese Relation gemäß den GDL-Restriktionen lediglich im body auftauchen darf, kann es hier keinen Kreis geben. OK




GDL Restriktionen







34




4.6.2. Validierung

Bei der Validierung kommt es darauf an zu überprüfen, ob die Beschreibung sich tatsächlich wie gewünscht verhält. Insbesondere werden daher die Rahmengestaltung, der Auktionsmechanismus und die Auszahlungen überprüft.

Rahmengestaltung

Wertschätzungen

Zur Rahmengestaltung gehört insbesondere die Festlegung der Wertschätzungen. Die entscheidende Regel hierbei ist folgende legal-Relation:



Sie überlässt dem random-Player die Wahl von m Werten. Durch die anfänglichen Terme wurde festgelegt, dass val(V) einen Wert zwischen 0 und 100 beinhalten kann. Dies entspricht dem gewünschten Intervall. Die Werte werden ermittelt, sobald der random-Player seinen Zug ausführt. Gemäß der Spezifikation erfolgt die Wahl zufällig und ist gleichverteilt. Im selben Schritt werden die Werte den Playern durch

next(hasValue(a_1,V1,0)) does(random, set_values(V1,…,Vm))

…

next(hasValue(a_m,Vm,0)) does(random, set_values(V1,…,Vm))

zugeordnet. Jeder erhält somit einen unabhängigen Wert gemäß dem Independent-private-value-model. Zur Ermittlung der späteren Auszahlungen, werden außerdem die individuellen Cashflows mit „0“ initialisiert, die sich im Laufe der Auktion verändern können. Die Wertschätzungen bleiben hingegen durch folgende Regeln immer gleich:

next(hasValue(a_1,V1,C)) true(hasValue(a_1,V1,C))

…

next(hasValue(a_m,Vm,C)) true(hasValue(a_m,Vm,C))

Dabei bleiben die Cashflows unberührt von dieser Regel und werden einfach in den nächsten Zustand übernommen. Die Wertschätzung ist aufgrund von


…


privat. Die Regeln beschreiben, dass jeder Teilnehmer nur seine eigene Wertschätzung als Information bekommt. Alle anderen Wertschätzungen sind unbekannt. Dieser Abschnitt der Beschreibung verhält sich demnach wie gewünscht und ist somit korrekt.

Rundensteuerung

Auch die Steuerung durch Runden der Auktion gehört zur Rahmengestaltung. Sie sollen sicherstellen, dass erst die Wertschätzungen ermittelt werden, dann das Gut gehandelt und zum Schluss die Auktion beendet wird. Da durch


die Initialisierungsrunde begonnen wird, kann die oben beschriebene Festlegung der Wertschätzungen erfolgen.


stellt sicher, dass dies genau einmal passiert und mit der Festsetzung der Wertschätzungen, die Auktion eröffnet wird. Denn auction(closed) ist ab sofort nicht mehr wahr. Durch

next(auction(opened)) true(auction(opened)) true(auction(finished))

wird sichergestellt, dass die Auktion eröffnet bleibt und nicht durch die Gebote der Teilnehmer beendet werden kann. Nur der Auktionator kann die Auktion beenden

legal(auctioneer, endBettingRound) true(auction(opened))


die noop-Operation ermöglicht ihm dabei auch unter Zugzwang nicht die Auktion vorzeitig beenden zu müssen. Sobald er jedoch die Auktion beendet, sorgt

next(auction(finished)) does(auctioneer, endBettingRound)

dafür, dass auction(opened) nicht mehr wahr ist. Dies beendet die Auktion. In diesem Zustand können keine Spielzüge mehr ausgeführt werden und der Endzustand wird erreicht:


Die jeweiligen Auslöser einer neuen Runde führen parallel zu einem Informationsfluss an alle Spieler, die durch

sees(R, auction(opened)) does(random, set_values(V1,…,Vm))

sees(R, auction(finished)) does(auctioneer, endBettingRound)

Kenntnis darüber erlangen in welcher Runde sie sich befinden.

Die Steuerung über die Runden funktioniert demnach wie gewünscht und ist somit korrekt.

Auktionsmechanismus

Gebotsabgabe

Die Gebotsabgabe ist bei der CDA zweiseitig. Ein Gebot kann dabei von jedem Teilnehmer abgegeben werden und entweder ein Kauf- oder Verkaufsangebot sein. Genau dies wird durch







beschrieben. Dabei bezeichnet Q die Menge und P den Preis des Gebots. Eine Menge kleiner gleich null ergibt keinen Sinn und wurde daher ausgeschlossen. Ebenso bedeutet ein negativer Preis lediglich, dass die Fließrichtung des Gutes umgekehrt wird. Dies wird bereits durch die zwei Gebotstypen dargestellt, weshalb auch ein negativer Preis ausgeschlossen wird. Die distinct-Klauseln sind notwendig, da der Auktionator und der random-Player nicht berechtigt sind Gebote abzugeben. Sobald ein Gebot abgegeben wurde, wird es durch



in das Orderbuch aufgenommen. Dort verbleibt es durch folgende Regeln solange, bis das Gebot ausgeführt wurde:

next(bid(R,Q,P)) true(bid(R,Q,P)) cleared(bid(R,Q,P))


Ein Gebot verliert also erst bei der Ausführung seine Gültigkeit. Diese wird im Abschnitt „Clearing“ näher beschrieben. Bei der CDA wurde zusätzlich eine besondere Form der Gebotsabgabe implementiert. Da die Gebote öffentlich sind, können bereits abgegebene Gebote einfach akzeptiert werden. Dies entspricht einer Gebotsabgabe mit den gleichen Parametern wie der Vertragspartner. In der Beschreibung wurde dies mittels:

legal(R1, accept(bid(R,Q,P)))


true(auction(opened)) true(bid(R,Q,P))

legal(R1, accept(ask(R,Q,P)))


true(auction(opened)) true(ask(R,Q,P))

umgesetzt. Dabei wurde verhindert, dass ein Teilnehmer sein eigenes Gebot akzeptieren kann, da dies einer Rücknahme des bereits abgegebenem Gebots entspricht, was nicht gewünscht ist. Die Gebote sind bei einer CDA öffentlich. Die Gebote müssen also für alle sichtbar sein, damit die Teilnehmer diese auch bei Interesse annehmen können. Dies wird durch folgende Regeln sichergestellt:

sees(R1, bid(R,Q,P)) does(R, my_bid(Q,P))

sees(R1, ask(R,Q,P)) does(R, my_ask(Q,P))

sees(R, cleared(O)) true(cleared(O))

Alle Teilnehmer werden umgehend informiert, sobald ein Gebot abgegeben wurde. Ebenso wird ein ausgeführtes Gebot unmittelbar mitgeteilt. Dadurch haben die Teilnehmer stets einen Überblick über gültige Gebote. Die Gebotsabgabe funktioniert demnach wie gewünscht und ist somit korrekt.

Clearing

Das Clearing bei der CDA besteht im Wesentlichen darin „passende“ Gebote zu finden und diese dann auszuführen. Es gibt zwei Möglichkeiten, wann ein Gebot als „passend“ betrachtet wird: Entweder gibt es zwei sich im Preis überschneidende Gebote oder ein Teilnehmer hat ein existierendes Gebot akzeptiert. Dies wird durch folgende legal-Relation repräsentiert:

legal(auctioneer, match(R1,Q1,P1,R2,Q2,P2,Q,P))

true(auction(opened))

((true(ask(R1,Q1,P1)) true(bid(R2,Q2,P2)) minimum(Q1,Q2,Q)

P1 P2 P1 P P P2)

(does(R1, accept(bid(R2,Q2,P2))) Q1=Q2 Q2=Q P1=P2 P2=P)

(does(R2, accept(ask(R1,Q1,P1))) Q1=Q2=Q P1=P2=P))

Grundsätzlich kann ein Clearing nur bei eröffneter Auktion stattfinden. Existieren ein Verkaufsgebot mit einem kleineren Preis, als der Preis eines anderen Kaufgebots, wurde ein passendes Gebot gefunden. Hierbei wird die maximal mögliche Menge Q gehandelt. Man beachte, dass bei dieser Modellierung der tatsächliche Ausführungspreis zwischen den abgegebenen Preisen der Gebote liegt und vom Auktionator bestimmt wird. Im anderen Fall, wenn ein Gebot lediglich akzeptiert wurde, werden die Menge und der Preis des bestehenden Gebots als Clearing-Parameter gewählt. Ausgeführte Gebote werden mittels

cleared(ask(R1,Q1,P1))


cleared(bid(R2,Q2,P2))


entsprechend gekennzeichnet. Nicht-ausgeführte Gebote bleiben durch next(bid(R,Q,P)) true(bid(R,Q,P)) cleared(bid(R,Q,P))


erhalten, wohingegen ausgeführte Gebote ihre Gültigkeit mangels einer entsprechenden next-Relation verlieren. Zusätzlich müssen Teilausführungen als Sonderfälle explizit modelliert werden:

next(ask(R1,Q1-Q,P1))

true(ask(R1,Q1,P1)) does(auctioneer, match(R1,Q1,P1,R2,Q2,P2,Q,P))

Q1 Q

next(bid(R2,Q2-Q,P2))

true(bid(R2,Q2,P2)) does(auctioneer, match(R1,Q1,P1,R2,Q2,P2,Q,P))

Q2 Q

Analog zur Call Auction werden bei der CDA ebenfalls zur späteren Berechnung die Auszahlungen im Verlauf der Auktion berechnet durch:

next(hasValue(R1,V,C1+Q*(P-V)))



next(hasValue(R2,V,C2-Q*(P-V)))



Da die Cashflows mit „0“ initialisiert wurden, können diese leicht neu berechnet werden. Das Clearing funktioniert demnach wie gewünscht und ist somit korrekt.

Auszahlungen

Da die Auszahlungen aller Teilnehmer bereits im Verlauf der Auktionen berechnet und im hasValue-Statement gespeichert wurden, ist die Codierung der goal-Relation trivial:

goal(R,C)

true(hasValue(R,V,C)) distinct(R,auctioneer) distinct(R,random)

Hier zahlt sich erneut die anfängliche Initialisierung mit „0“ aus, die eine korrekte Auszahlung auch bei keinem stattgefundenen Handel ermöglicht. Die Auszahlungen entsprechen der Auszahlung einer realen Continuous Double Auction und sind somit korrekt.


5. Zusammenfassung und Ausblick Im Rahmen dieser Arbeit wurden formale Beschreibungen von gängigen Auktionstypen vorgestellt, die ein automatisiertes Reasoning durch Agenten ermöglichen. Da es bereits zahlreiche solcher Agenten35 gibt, die Beschreibungen auf Basis der GDL interpretieren, ist es nur noch ein kleiner Schritt zur Entwicklung von Agenten, die diese GDL-II Modelle interpretieren

35

Beispielhaft seien an dieser Stelle der FLUX-Player, sowie der CADIA-Player erwähnt. Vgl. [Fin07] und [Sch07]

können. Die bestehenden Agenten können in großen Teilen adaptiert und müssen lediglich hinsichtlich der Erweiterungen der GDL-II geringfügig angepasst werden.

5.1. Umsetzung im Börsenhandel Da insbesondere die Call Auction und die CDA an den Börsen weit verbreitet sind, wäre eine Umsetzung in diesem Bereich also prinzipiell denkbar. Bereits heute ist der Börsenhandel durch das Algorithmic Trading (AT) stark computergestützt, was zu massiven Entwicklungen hinsichtlich der Liquidität und Information auf Börsenmärkten geführt hat. Eine ausführliche Betrachtung der Auswirkungen von AT auf den Märkten wurde bereits in diversen wissenschaftlichen Arbeiten durchgeführt. Beispielhaft sind die Arbeiten von Terrence Hendershott et. al zu erwähnen.36 Das AT beruht jedoch stets auf Strategien, die durch Menschen entwickelt und in Programme umgesetzt wurden. Das automatische Reasoning durch Agenten würde den computergestützten Börsenhandel erneut auf eine ganz andere Ebene heben, da nun die Entwicklung einer Strategie ohne jegliche menschliche Interaktion erfolgen kann. Die Folgen für die Börsenmärkte sind zum jetzigen Zeitpunkt nicht abzusehen, aber es ist mit weiteren revolutionären Veränderungen zu rechnen, so wie sie einst durch das AT ausgelöst wurden. Fraglich ist auch, wie sich mit zunehmender Anzahl solcher automatisierten Agenten die Börse verhält. Bei allen Potenzialen, die das automatisierte Reasoning an der Börse bietet, gibt es dennoch gravierende Beschränkungen, die eine zeitnahe Umsetzung im Börsenhandel höchst Unwahrscheinlich erscheinen lassen. So gilt es zu bedenken, dass diese Beschreibungen lediglich ein Grundgerüst darstellen, welches noch lange nicht ausgereift genug ist um alle Dimensionen des Wertpapierhandels abzudecken. So fehlt es hier gänzlich an der Verarbeitung von Unternehmensinformationen, Marktdaten und Nachrichten. Insbesondere fehlt es auch an einer Einbeziehung der Kreditwürdigkeit und Risiken, da in der Beschreibung das Ausfallrisiko stets „0“ ist, was selbstverständlich in der realen Welt nicht plausibel ist. Der aktuelle Stand dieser Technologie ist der Komplexität einer Börse demnach nicht gewachsen. Allerdings ist die GDL-II grundsätzlich mächtig genug, um dem gerecht zu werden. Hierfür bedarf es lediglich noch einiger Jahre Entwicklung.

5.2. Umsetzung in Internetauktionen

Wahrscheinlicher scheint es hingegen, dass solche Agenten sich vorher in einem einfacheren Umfeld etablieren. So wären klassische Bietauktionen wie z.B. eBay ein praktikables Anwendungsgebiet. Hier sind der Preis eines Gutes und das Verhalten der anderen Bieter tatsächlich die einzig für den Kauf relevanten Informationen. Zusätzliche Regeln, die von den Internetauktionshäusern gestellt werden, könnten leicht umgesetzt werden. Ebenso könnte die Wertschätzung zum Beispiel zu Beginn einer Auktion manuell eingegeben werden, sodass der Bietagent völlig autark agieren kann. Während der Auktion ist der Mensch demnach überflüssig und kann sich anderen Dingen widmen. Hierbei würde das Internetauktionshaus die Rolle des Game Managers übernehmen37. Dies bedeutet, dass es eine entsprechende Beschreibung zur Verfügung stellen und die Teilnehmer koordinieren müsste. Da Zweites ohnehin bereits geschieht, ergibt sich für das Internetauktionshaus kein zusätzlicher Mehraufwand. Lediglich die Beschreibung müsste einmalig entwickelt werden.

36

Vgl. [Hen11] und [Hen111] 37

Vgl. [Lov06]

Zusammenfassend lässt sich also feststellen, dass das automatisierte Reasoning durch Agenten auf Basis der GDL-II bereits in einfachen Umgebungen umgesetzt werden könnte, um dort den Menschen in seiner Funktion zu ersetzen. Allerdings wurden auch noch große Potenziale, insbesondere hinsichtlich einer Anwendung an den Börsen, aufgedeckt. Diese zu erschließen ist weniger eine Frage der Machbarkeit, sondern mehr eine Frage der Zeit.

5.3. Umsetzung bei auktionsähnlichen Methoden38

Die hier beschriebenen Modelle wurden anhand konkreter Auktionsmechanismen erstellt. Allerdings sind sie in der Anwendung keineswegs darauf beschränkt. Sie können durchaus auch in auktionsähnlichen Verfahren eingesetzt werden. So bieten Offenmarktgeschäfte ein weiteres Anwendungsfeld, welche nach einem ähnlichen Prinzip funktionieren. Beispielhaft wird an dieser Stelle auf das Tenderverfahren eingegangen, welches zu den wichtigsten Instrumenten der Geldpolitik der Europäischen Zentralbank (EZB) gehört. Man unterscheidet insbesondere zwischen einem Mengentender und einem Zinstender:

5.3.1. Mengentender

Beim Mengentender geben alle Interessenten eine Geldmenge an, die sie zu einem vorgegebenen Zinssatz annehmen möchten. Dabei können Gebote auch wieder zurückgezogen werden. Die Zuteilung erfolgt erst nach Ablauf einer vorgegebenen Frist. Sofern die Summe der nachgefragten Geldmenge nicht den Gesamtbetrag der zur Verfügung gestellten Menge übersteigt, erhält jeder Bieter seine gewünschte Menge. Sollte die Summe jedoch die angebotene Geldmenge übersteigen, werden die Gebote anteilig im Verhältnis des vorgesehenen Zuteilungsbetrags zum Gesamtbietungsaufkommen zugeteilt.

5.3.2. Zinstender

Das oben beschriebene Verfahren führte in der Praxis jedoch dazu, dass die Teilnehmer höhere Geldsummen forderten, als sie tatsächlich benötigt hätten, um bei der Zuteilung mit höherer Priorität behandelt zu werden. Daher wurde das der Zinstender eingeführt, bei dem jeder Teilnehmer zusätzlich zu seinem Gebot den Zinssatz angibt, zudem er bereit wäre die Geldmenge aufzunehmen. Im Rahmen der Zuteilung werden die Gebote dann absteigend nach dem Zinssatz sortiert, sodass zunächst die Gebote mit höherem Zins bedient werden. Die nächsthöheren Zinsgebote werden solange bedient, bis die der vorgesehene Zuteilungsbetrag erreicht wurde. Die großen Analogien zu den beschriebenen Auktionsverfahren werden sofort deutlich. Es bedarf lediglich geringfügiger Anpassungen, um das in der Geldmarktpolitik zentrale Instrument darstellen zu können. Dies würde es den Teilnehmern ermöglich automatisierte Agenten bei der Wahl der Gebote einzusetzen, um optimal handeln zu können.

Abbildungsverzeichnis Abbildung 1: Gala Spielzug ................................................................................................................. 13

Abbildung 2: Auktionstypen ............................................................................................................... 18

Abbildung 3: Interaktionsprotokoll Englische Auktion ...................................................................... 24

38

Das in diesem Abschnitt beschriebene Tenderverfahren beruht auf [Eur06]

Literaturverzeichnis [Apt88] Apt, R. Krzystof, Blair, Howard A. and Adrian, Walker. 1988. Towards a theory of declarative knowledge. Foundations of deductive databases and logic programming. San Francisco, CA, USA : Morgan Kaufmann Publishers Inc., 1988. [Fin07] Finnson, Hilmar. 2007. CADIA-Player: A General Game Playing Agent. 2007. [FIP01] FIPA. 2001. FIPA English Auction Interaction Protocol Specification. ID00031. [Online] Foundation for Intelligent Physical Agents, 2001. [Cited: September 4, 2011.] http://www.fipa.org/specs/fipa00031/. [Fis98] Fischer, K., Russ, C. and Vierke, G. 1998. Decision theory and coordination in multiagent systems. 1998. [Gen05] Genesereth, Michael, Love, Nathaniel and Pell, Barney. 2005. General Game Playing: Overview of the AAAI Competition. AI Magazine Volume 26 Number 2. 2005, pp. 62-72. [Har02] Harris, Larry. 2002. Trading and Exchanges - Market Microstructure for Practitioners. s.l. : Oxford University Press, 2002. [Hen11] Hendershott, Terrence and Riordan, Ryan. 2011. Algorithmic Trading and Information. NET Institute Working Paper No. 09-08. Available at SSRN: http://ssrn.com/abstract=1472050. 2011. [Hen111] Hendershott, Terrence, Jones, Charles M. and Menkveld, Albert J. 2011. Does Algorithmic Trading Improve Liquidity? The Journal of Finance Volume 66, Issue 1, pages 1–33, February 2011. 2011. [Kol97] Koller, Daphne and Pfeffer, Avi. 1997. Representations and solutions for game-theoretic problems. Artificial Intelligence 94. 1997. [Kuh06] Kuhlmann, Gregory and Stone, Peter. 2006. Automatic heuristic construction for general game playing. AAAI'06 proceedings of the 21st national conference on Artificial intelligence - Volume 2. 2006, pp. 1457-1462. [Kul09] Kulick, Johannes, Block, Marco and Rojas, Raúl. 2009. General Game Playing mit stochastischen Spielen. s.l. : Freie Universität Berlin, 2009. [Lov06] Love, Nathaniel, Hinrichs, Timothy and Genesereth, Michael. 2006. General Game Playing: Game Description Language Specification. Stanford, CA 94305 : Stanford University, 2006. [Luc00] Lucking-Reiley, David. 2000. Vickrey Auctions in Practice: From Nineteenth-Century Philately to Twenty-First-Century. The Journal of Economic Perspectives, Vol. 14, No. 3. 2000. [McA87] McAffee, Preston and McMillan, John. 1987. Auctions and Bidding. Journal of Economic Literature Vol. 25, No. 2. 1987. [Pel92] Pell, Barney. 1992. METAGAME in Symmetric Chess-Like Games. Cambridge, UK : University of Cambridge, 1992. pp. 1-30. [Rei00] Reichwald, Ralf, Hermann, Michael and Bieberbach, Florian. 2000. Auktionen als Preisfindungsmechanismus auf elektronischen Märkten. Lehrstuhls für Allgemeine und Industrielle Betriebswirtschaftslehre der Technischen Universität München : s.n., 2000. [Rot90] Rothkopf, Michael, Teisberg, Thomas and Kahn, Edward. 1990. Why Are Vickrey Auctions Rare? Journal of Political Economy, Vol. 98, No. 1. 1990. [Sch07] Schiffel, Stephan and Thielscher, Michael. 2007. Fluxplayer: A Successful General Game Player. 2007. [Sch88] Schwartz, Robert A. 1988. Equity Markets. New York : Harper and Row, 1988. [Ste10] Stephan, Christian. 2010. Strategisches Verhalten bei Internetauktionen: Eine empirische Analyse mit Fokus auf den Marktplatz eBay. s.l. : Volker Derballa, 2010. [Sur04] Surowiecki, James. 2004. The Wisdom of Crowds. Why the Many Are Smarter Than the Few and How Collective Wisdom Shapes Business, Economies, Societies and Nations. s.l. : Anchor, 2004.

[Thi10] Thielscher, Michael. 2010. A General Game Description Language for Incomplete Information Games. Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence (AAAI-10). 2010. [Thi09] Thielscher, Michael and Zhang, Dongmo. 2009. A formal market specification language for general trading agents. Proceedings of the IJCAI-09 Workshop on General Game Playing (GIGA'09) . 2009. [Vic61] Vickrey, William. 1961. Counterspeculation, Auctions, and Competitive Sealed Tenders. The Journal of Finance, Vol. 16, No. 1. 1961. [Wil80] Williams, Arlington W. 1980. Computerized Double-Auction Markets: Some Initial Experimental Results. The Journal of Business, Vol. 53, No. 3. 1980. [Yam72] Yamey, B.S. 1972. Why 2,310,000 [pounds] for a Velazquez?: An Auction Bidding Rule. Journal of Political Economy, Vol. 80, No. 6. 1972. [Eur06] Zentralbank, Europäische. 2006. DURCHFÜHRUNG DER GELDPOLITIK IM EURO-WÄHRUNGSGEBIET. Frankfurt am Main : s.n., 2006.

Formale Beschreibung von Auktionstypen zum … · B A C H E L O R A R B E I T Formale Beschreibung...

Documents

Transcript of Formale Beschreibung von Auktionstypen zum … · B A C H E L O R A R B E I T Formale Beschreibung...