| dc.date.accessioned | 2019-10-29T13:21:39Z | |
| dc.date.available | 2019-10-29T13:21:39Z | |
| dc.date.issued | 2019 | |
| dc.identifier | doi:10.17170/kobra-20191014716 | |
| dc.identifier.uri | http://hdl.handle.net/123456789/11329 | |
| dc.language.iso | eng | eng |
| dc.rights | Urheberrechtlich geschützt | |
| dc.rights.uri | https://rightsstatements.org/page/InC/1.0/ | |
| dc.subject | Automata Theory | eng |
| dc.subject | Language Inclusion | eng |
| dc.subject | Simulation | eng |
| dc.subject | Infinite Games | eng |
| dc.subject.ddc | 004 | |
| dc.title | Buffered Simulation for Büchi Automata | eng |
| dc.type | Dissertation | |
| dcterms.abstract | 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. | ger |
| dcterms.abstract | We introduce a new family of simulation relations between two non-deterministic Büchi automata (NBA) called buffered simulation. We extend the game framework of the standard fair simulation such that Duplicator can skip her turn and store the letter that is read by Spoiler temporarily to a buffer. Duplicator then can execute the letters in the buffer in some later round. In this way, she has a preview of Spoiler’s move and has more chances to mimic Spoiler’s run correctly than in the standard fair simulation game. We generalise such a simulation to the case where multiple buffers are involved. In such a case, a rule that tells us to which buffers a letter should be stored is given. Once Spoiler reads a letter, Duplicator stores it to all the associated buffers, and when she wants to execute the letter, she has to pop it from all the associated buffers.
We study the decidability and complexity of buffered simulation with one or multiple buffers. We show that buffered simulation is undecidable if some of the buffers are unbounded. It is even already highly undecidable in the case of two buffers where one is unbounded and the other one is of capacity 0. In the case where all buffers are bounded, buffered simulation is decidable in polynomial time. In the case of a single, but unbounded buffer, buffered simulation is PSPACE-complete for a variant that requires Duplicator to pop all the letters from the buffer each time she decides to move. It is, however, EXPTIME-complete for the general case.
We further show that buffered simulation with one buffer can be used to incrementally approximate language inclusion between two NBA. In the case of multiple buffers, it can be used to approximate a more general problem, namely the trace closure inclusion problem, which is known to be highly undecidable. We give a theoretical justification of buffered simulation by giving a characterisation using the notion of continuity. Buffered simulation with unbounded buffers can be characterised by the existence of a continuous function that witnesses the language or trace closure inclusion between the input automata. We can lift such a characterisation to the case of bounded buffers by considering a Lipschitz continuous function instead of just a continuous one. Such a characterisation, however, only holds for some restricted automata called cyclic-path-connected automata. | eng |
| dcterms.accessRights | open access | |
| dcterms.creator | Hutagalung, Milka | |
| dcterms.dateAccepted | 2018-09-27 | |
| dcterms.extent | 168 Seiten | |
| dc.contributor.corporatename | Kassel, Universität Kassel, Fachbereich Elektrotechnik / Informatik | ger |
| dc.contributor.referee | Lange, Martin (Prof. Dr.) | |
| dc.contributor.referee | Kučera, Antonín (Prof. Dr.) | |
| dc.subject.swd | Automatentheorie | ger |
| dc.subject.swd | Büchi-Automat | ger |
| dc.subject.swd | Simulation | ger |
| dc.subject.swd | Unendliches Spiel | ger |
| dc.type.version | publishedVersion | |
