Spiel (Logik)

Ein Spiel $\mathcal{G}=(V,V_0,E,v_0,\mathrm{\Omega })$ besteht aus einer Arena und einer Gewinnbedingung:

• $V$: Menge aller Spielpositionen (Knoten eines Graphen).
• $V_0\subseteq V$: Positionen, an denen Spieler 0 (Verifiziererin) am Zug ist. An Positionen in $V\setminus V_0$ zieht Spieler 1 (Falsifizierer).
• $E\subseteq V\times V$: Die möglichen Züge (Kanten des Graphen).
• $v_0$: Die Startposition.
• $\mathrm{\Omega }\subseteq V^{\omega }$: Die Gewinnbedingung für unendliche Partien (Menge der gewinnen Folgen).

Bei endlichen Partien gewinnt der Spieler, dessen Gegner nicht mehr ziehen kann (in einer Sackgasse steckt).