Im Kern bezeichnet Synthese eigentlich nur die Zusammenführung verschiedener Elemente, um etwas Neues zu schaffen. So nennt man in der Philosophie das Zusammenführen zweier unterschiedlicher Weltanschauungen zum Beispiel die Synthese der beiden. In diesem Blogeintrag meine ich allerdings eine modernere Art der Synthese. Nämlich das, was man üblicherweise in der Chemie und Technologie unter Synthese versteht: das künstliche Herstellen von Produkten (chemischen Stoffen), die durch neue Verbindungen entstehen. Das Wort Synthese wird also hier auch im weitesten Sinne für die Zusammenführung von Elementen verwendet. Wenn man zum Beispiel eine chemische Verbindung, die natürlich in Kuhmägen entsteht, im Labor - ganz ohne Kuh - erzeugt, so hat man sie synthetisiert. Das ist allerdings immer noch nicht ganz die Art von Synthese auf die ich hinaus möchte.

Synthese in der theoretischen Informatik

In den letzten Jahren hat sich auch in der theoretischen Informatik ein Typ von Synthese entwickelt: Ähnlich zur chemischen Synthese, haben Forschende versucht Computerprogramme "künstlich" zu erstellen. Das heißt, sie haben Software entwickelt, die - basierend auf genau definierten Anforderungen - automatisch und korrekt Programmcode schreibt, der genau die beschriebene Funktionalität erfüllt.

Im Gegensatz zu KI Tools wie ChatGPT, die zugegebenermaßen ebenfalls "programmieren" können, sind synthetisierte Programme garantiert fehlerfrei und erfüllen garantiert die definierten Anforderungen. Diese Garantie kommt wieder einmal vom Automatischen Beweisen (wie im Blogeintrag "Steht der Bauer..." beschrieben). Automated Reasoners werden dabei verwendet, um während der Synthese eines Programms jeden Programmbefehl zu verifizieren. Obwohl diese Technologie ziemlich cool ist, wie ich finde, kommt in meiner Forschung nochmal eine Abwandlung dieser Idee zum Einsatz. (Das ist dann die letzte Definition von Synthese. - Versprochen! :) )

Synthese von Spielen

Wie schon in vielen anderen Blogposts (CheckMate, CheckMate trifft Ethereum, 1 Jahr Netidee) berichtet, arbeite ich am automatischen Verfizieren der spieltheoretischen Sicherheit von Blockchain Protokollen. Dafür brauche ich bzw. die User*innen meines Tools allerdings ein spieltheoretisches Modell des zu analysierenden Protokolls. Nachdem die wenigsten meiner möglichen User*innen über spieltheoretische Kenntnisse verfügen, ist das ein sehr limitierender Faktor. Nach der langen Heranführung in diesem Blog, liegt nun die Lösung dieses Problems nahe: Synthese von (spieltheoretischen) Spielen!

Wie ich mir das vorstelle und über erste Ansätze habe ich bereits übersichtsmäßig in meinem Blog Eintrag CheckMate trifft Ethereum berichtet.

Details und Lösungsansätze

Die Forschungsfragen, die ich in CheckMate trifft Ethereum aufgelistet habe, sind nun größtenteils beantwortet:

• Wodurch (durch welche Parameter) wird der Gewinn/Verlust der Teilnehmer*innen bestimmt?  
  • Verlust bzw. Gewinn kann ausschließlich von Parametern abhängen, die das Protokoll kennt. Das heißt, es handelt sich um gespeicherte Größen deren Änderung wir im Laufe des Spiels verfolgen können. Dadurch ist es ausreichend, wenn User*innen die heranzuziehenden Parameter und deren Rolle (Summand, Faktor etc.) bereitstellen.
• Welche Kategorien von Spieler*innen gibt es?    
  • User*innen geben an welche Spieler*innen (abstrakte Namen) zu berücksichtigen sind. Sie können zusätzlich Protokollparameter der Spieler*innen definieren. Zum Beispiel: Spielerin A ist Administratorin des Protokolls, während Spieler B nur partielle Zugriffsrechte hat.
• Wie viele Spieler*innen sollten wir pro Kategorie betrachten?     
  • Die Liste an Spieler*innen, die die Userin bereitstellt, wird als vollständig angenommen. Im Falle des obigen Beispiels gibt es also genau 2 Spieler*innen A und B.
• Welche Spieler*in ist wann "dran"?     
  • Die bereitgestellte Liste wird ebenfalls als geordnet angenommen. Das hießt, die zuerstgenannte Spieler*in hat immer Vorrang, falls das Protokoll die nächste Spieler*in nicht bestimmt. Zusätzlich darf (mit Ausnahmen) nie zweimal dieselbe Person "drankommen".
• Wann endet das Spiel?   
  • Sollte das Protokoll eine Endlosschleife zulassen, beenden wir vorläufigerweise das Spiel nach einer gewissen maximalen Anzahl an Zügen.

Darüberhinaus habe ich die größten Herausforderungen in der Spielsynthese in folgender Übersicht zusammengefasst:

Die Tabelle stellt die unterschiedlichen Eigenschaften von Protokollen und Spielen gegenüber, die für unsere Spielsynthese eine Herausforderung darstellen. Wie beim Beantworten der Forschungsfragen schon kurz erwähnt, haben Protokolle und Spiele verschiedene Strukturen. Protokolle beschreiben einzelne Komponenten ohne chronologischen Kontext, während Spiele (zumindest die von uns betrachtete Art) lineare Verhalten beschreiben, bei denen eine Aktion nach der anderen gewählt wird. Weiters sind die agierenden Personen (Spieler*innen) in Protokollen abstrakte "Caller" (Aufrufer) einer Funktionalität. Bei Spielen jedoch, sind das genau definierte "Spieler*innen" mit genau definierten Fähigkeiten. Die Bedingungen, die das Ausführen von Teilen des Protokolls regulieren, müssen logischerweise nicht immer erfüllt sein, sonst wären sie ja überflüssig. Die zu wählenden Züge in einem Spiel müssen alllerdings immer möglich sein, sonst könnte ein Spiel ja einfach "stecken bleiben": es wäre zwar nicht aus, es gäbe aber auch keine weiteren möglichen Aktionen. Die besagten Aktionen - also Aufrufe von Funktionalität in Protokollen - sind in der Regel nicht leer, das heißt sie bezwecken irgendetwas und tun nicht einfach nichts. In unserem spieltheoretischen Kontext, ist das "Nichtstun" aber möglich und sogar erwünscht. Abschließend ist die Namensgebung von Parametern in Protokollen nur lokal, also auf die jeweilige Funktionalität beschränkt, in unseren Spielen sind sie aber global, also werden im gesamten Spiel verwendet.

Zur Zeit arbeite ich an der Implementierung der obigen Antworten zu den Forschungsfragen sowie den Lösungen der gelisteten Herauforderungen. Der zugehörige Code ist hier verfügbar. Das Projekt Spielsynthese bleibt also auf alle Fälle spannend!