Buffered Simulation for Büchi Automata

Wir stellen eine neue Familie von Simulationsrelationen zwischen zwei nicht deterministischen Büchi Automaten (NBA), genannt gepufferte Simulation vor. Wir erweitern das Spiel-Framework der üblichen fairen Simulation, so dass Duplicator ihren Spielzug überspringen und die Buchstaben, die Spoiler gelesenen hat, vorübergehend in einem Puffer speichern kann. Duplicator kann diese Buchstaben in ihrer Struktur dann später ausführen. Duplicator hat damit eine Vorschau in die Bewegungen von Spoiler und somit mehr Chancen, den Lauf Spoilers korrekt nachzuahmen als im Standard-Simulationsspiel. Wir verallgemeinern dann diese Simulationsrelationen auf mehrere Puffer. In einem solchen Fall gibt es eine Regel, die angibt, in welchen Puffern ein Buchstabe gespeichert werden soll. Sobald Spoiler einen Buchstaben liest, speichert Duplicator ihn in jedem zugeordneten Puffer und wenn Duplicator ihn in ihrer Struktur ausführen möchte, muss sie den Buchstaben von jedem zugehörigen Puffer löschen. Wir untersuchen die Entscheidbarkeit und Komplexität von gepufferten Simulationen mit einem oder mehreren Puffern. Wir zeigen, dass gepufferte Simulation nicht mehr entscheidbar ist, wenn einige Puffer unbegrenzt sind. Es ist tatsächlich sogar schon hochgradig unentscheidbar bei zwei Puffern, in denen einer unbegrenzt ist und der andere die Kapazität 0 hat. In dem Fall, in dem alle Puffer begrenzt sind, ist gepufferte Simulation in polynomieller Zeit entscheidbar. Für die Simulation mit einem einzelnen, aber unbeschränkten Puffer ist die gepufferte Simulation PSPACE-vollständig für eine Variante, bei der Duplicator alle Buchstaben aus dem Puffer löschen muss, jedes Mal wenn sie sich bewegt. Es ist jedoch EXPTIME-vollständig für den allgemeinen Fall. Wir zeigen weiterhin, dass gepufferte Simulation mit einem Puffer Spracheinklusion zwischen zwei NBA schrittweise approximiert. Mit mehreren Puffern kann gepufferte Simulation die Inklusion des Spurabschlusses zweier NBA approximieren, welche bekanntermaßen hochgradig unentscheidbar ist. Wir formulieren eine theoretische Untermauerung für gepufferte Simulation, indem wir sie als Stetigkeitsfrage in einem geeigneten topologischen Raum auffassen. Gepufferte Simulation mit unbeschränkten Puffern kann durch die Existenz einer stetigen Funktion, die die Sprache oder die Spurabschluss Inklusion zwischen den beiden Automaten bezeugt, charakterisiert werden. Wir können diese Charakterisierung auf gepufferte Simulation mit begrenzten Puffern erweitern, indem wir sogar Lipschitz-Stetigkeit der Funktion verlangen. Eine solche Charakterisierung gilt allerdings nur für eine beschränkte Klassen von Automaten, die wir zyklisch-pfad-verbunden nennen.