Formale Methoden treffen auf algorithmische Spieltheorie

Ziel dieses Fellowships ist es, Konzepte und Ideen zwischen zwei Gebieten der theoretischen Computerwissenschaft zu transferieren, die verschiedene Zugänge zur Spieltheorie haben; formale Methoden und die algorithmische Spieltheorie (kurz AST). Formale Methoden zielen darauf ab, Systeme formell zu analysieren, zum Beispiel formell zu beweisen, dass ein System seine Spezifikation erfüllt, oder a- priori korrekte Systeme von einer gegebenen Spezifikation zu generieren. Spieltheorie ist in den formalen Methoden beliebt, da es praktisch ist um die Interaktion eines Systems mit seiner Umwelt als zwei-Personen Spiel, das auf einem Graph gespielt wird, zu modellieren. Das Syntheseproblem reduziert sich dann darauf, eine Gewinnstrategie für den Spieler zu finden, der das System modelliert. AST ist ein rasch wachsendes Gebiet, das an der Schnittstelle zwischen Computerwissenschaften und Wirtschaft liegt. Anders als Spiele in den formalen Methoden, die typischerweise Nullsummenspiele sind, bei denen ein Spieler gewinnt und der andere Spieler verliert, sind die Spiele in der AST typischerweise mehrwertig, und die Fragen betreffen normalerweise die Stabilität des Spiels. In meiner Dissertation untersuchte ich den Transfer von Konzepten und Ideen zwischen formalen Methoden und Netzwerkspielen, eine gut untersuchte Kategorie von Spielen in der AST. Mir sind keine Versuche bekannt, Brücken zwischen diesen Feldern herzustellen, obwohl diese Verbindung als wichtig erachtet wird. Dieses Fellowship vertieft und verbreitert die Verbindung, die bereits hergestellt wurde, indem es die Treffpunkte zwischen formalen Methoden und Auktionstheorie, einem Kerngebiet der AST, untersucht. Eine Auktion ist der Prozess, bei denen Verkaufsartikel an Bieter verkauft werden. Es ist ein sehr generelles Konzept mit vielen Anwendungsgebieten. Ich werde auf neuen Ergebnissen aufbauen, bei denen wir Spiele auf Graphen untersuchten bei denen Spieler, anstatt abwechselnd zu spielen, um das Recht zu spielen bieten. Bei jedem Spielzeug findet eine Auktion statt, bei der die Spieler gleichzeitig ihre Gebote abgeben. Der höchste Bieter gewinnt, bezahlt die anderen Spieler und entscheidet, wie das Spiel weitergeht. Die Spieler haben widersprüchliche Zielsetzungen, zum Beispiel eine Position am Graph zu erreichen. Bei seinem Spielzug versucht ein Spieler zu forcieren, dass seine Zielsetzung erreicht wird, so dass er das Spiel gewinnt. Die Fragen, die wir untersuchten, beinhalteten etwa, wie viel Startbudget ausreicht, um zu gewinnen. Bieten um zu spielen ist ein extrem generelles Konzept, das eine spannende Verbindung zwischen diesen beiden Feldern eröffnet. Das Hauptziel dieses Fellowships ist, dieses Konzept extensiv zu untersuchen. Ich werde verschiedene Spiele auf Graphen sowie alternative Gebotsregeln theoretisch untersuchen, und ich werde die Anwendungen dieses Konzepts untersuchen, die dadurch entstehen, dass ein Bieterspiel als Spiel zwischen Prozessen in einem parallelen System gesehen wird und dass das Gebot eines Prozesses verwendet wird um die Wichtigkeit, es einzuplanen, zu quantifizieren; je höher das Gebot, desto mehr muss es eingeplant werden.

"Spiele auf Graphen" stellen eine wichtige Klasse von Spielen dar, die für mehrere Teilbereiche der Computerwissenschaften relevant ist. Das Spiel schreitet fort indem ein Spielstein auf einen der Knoten eines Graphen gelegt wird und die Spieler dürfen den Spielstein auf einen Nachbarknoten bewegen um einen unendlichen Pfad durch den Graphen zu erzeugen. Die Spieler bewegen abwechselnd den Spielstein. Wir betrachten "Bietspiele", bei denen beide Spieler über Budgets verfügen und in jeder Runde gibt es eine Auktion, um festzustellen, wer den Stein bewegen darf. Die Frage, die wir untersucht haben, war: Wie beeinflussen Änderungen am Mechanismus des Bietens die Eigenschaften des Spiels? Eines unserer Ergebnisse lässt sich wie folgt veranschaulichen. In dem von uns verwendeten konkreten Mechanismus des Bietens schreiben die beiden Spieler auf ein Blatt Papier, wie viel sie bereit sind, für den nächsten Zug zu zahlen. Sie enthüllen ihre "Angebote", indem sie gleichzeitig ihre Papiere umdrehen, und der höhere Bieter darf den Stein bewegen. Beim "Richman-Bieten" bezahlt der Höherbieter den Niedrigbieter, beim "Poorman-Bieten" wird das Angebot an die "Bank" bezahlt und das Geld geht verloren. Obwohl diese Änderung des Zahlungsschemas geringfügig erscheint hat sie einen drastischen Einfluss auf die Eigenschaften des Spiels. Wir haben gezeigt, dass bei Bietspielen mit "unendlicher Dauer" und Richman-Bieten die anfänglichen Budgets keine Rolle spielen und der Nutzen eines Spielers ausschließlich durch die Graphstruktur bestimmt wird. Beim Poorman-Bieten spielen die Budgets eine Rolle: Je höher das ursprüngliche Budget, desto höher der Nutzen, den ein Spieler erzielen kann. Darüber hinaus haben wir andere Zahlungsschemata sowie die folgenden zwei orthogonalen Eigenschaften der Biet-Mechanismen untersucht. Zuerst haben wir das "All-Pay" -Bieten untersucht, bei dem beide Spieler ihre Angebote bezahlen. Über die interessanten theoretischen Eigenschaften dieses Mechanismus hinaus führt er zu praktischen Anwendungen, indem die Budgets als begrenzte Ressourcen mit geringem oder keinem inhärenten Wert betrachtet werden, die dynamisch investiert werden müssen, um ein bestimmtes Ziel zu erreichen. Zum Beispiel werden politisches Lobbying oder Kampagnen natürlich durch solche Spiele modelliert. Zweitens haben wir, motiviert durch praktische Anwendungen, diskrete Bietspiele untersucht, bei denen die Budgets in Münzen angegeben werden. Das minimale positive Angebot, das ein Spieler machen kann, ist dabei eine Münze. Die in diesem Fellowship erzielten Ergebnisse sind ein erster wichtiger Schritt bei der Untersuchung dieses Modells seit den 90er Jahren. Sie demonstrieren die Nützlichkeit der Kombination mit "formalen Methoden", aus denen das Konzept des Studiums von Spielen mit "unendlicher Dauer" hervorgeht. Weiters lassen sie viel Raum für eine weiterführende Untersuchung des eleganten Modells der Bietspiele.