Reachability over word rewriting systems

Altenbernd, Jan-Henrik; Thomas, Wolfgang

doi:3399

Reachability over word rewriting systems = Erreichbarkeit über Wortersetzungssystemen

Altenbernd, Jan-Henrik (Author)

2010

Verantwortlichkeitsangabevorgelegt von Jan-Henrik Altenbernd

ImpressumAachen : Publikationsserver der RWTH Aachen University 2010

UmfangIII, 116 S. : graph. Darst.

Aachen, Techn. Hochsch., Diss., 2009

Zsfassung in engl. und dt. Sprache

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Thomas, Wolfgang (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2009-12-11

Online
URN: urn:nbn:de:hbz:82-opus-33993
URL: https://publications.rwth-aachen.de/record/63260/files/3399.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Wortersetzungssystem (Genormte SW) ; Erreichbarkeit (Genormte SW) ; Informatik (frei) ; Wortersetzung (frei) ; Erreichbarkeitsproblem (frei) ; word rewriting (frei) ; reachability (frei)

Thematische Einordnung (Klassifikation)
DDC: 004
ccs: F.1.1 * F.4.3

Kurzfassung
Wortersetzungssysteme sind während der letzten hundert Jahre unter verschiedenen Gesichtspunkten untersucht worden. Anfänglich wurden sie vor allem als Rahmenwerk zur Darstellung von Berechnungsprozessen und als Werkzeug zur Erzeugung formaler Sprachen betrachtet. In letzter Zeit sind sie auch als ein Mechanismus studiert worden, mit dem unendliche Graphen durch einen endlichen Formalismus repräsentiert werden können. Der Schwerpunkt dieser Dissertation liegt in diesem Bereich. Im ersten Teil der Arbeit betrachten wir gemischte Präfix- und Suffix-Ersetzungssysteme (MPSR-Systeme), welche Präfix- und Suffix-Ersetzung in nichtdeterministischem Modus kombinieren. Wir untersuchen zentrale algorithmische Eigenschaften der Graphen, die durch solche Systeme erzeugt werden können; dabei ist besonders das Erreichbarkeits-Problem (als Musterproblem des Model-Checking) von Interesse. Weiterhin untersuchen wir die Beziehung der Klassen von Graphen, die durch MPSR-Systeme erzeugt werden, zu anderen wohlbekannten Graphklassen, wie etwa denen der präfix-erkennbaren und der automatischen Graphen. Außerdem widmen wir uns den Trace-Sprachen von MPSR-Systemen, und wir zeigen, dass diese Klasse die Klasse der kontextfreien Sprachen echt umschließt und selbst eine echte Teilklasse der Klasse der kontextsensitiven Sprachen ist.Im zweiten Teil der Arbeit führen wir markierte Infix-Ersetzungssysteme (TIR-Systeme) ein, die eine Erweiterung der MPSR-Systeme sind, und in denen spezielle Symbole (sogenannte Marker) für eine eingeschränkte Form von Infix-Ersetzung benutzt werden. In ihrer Grundform, in der Ersetzungsregeln solche Marker nicht verändern dürfen, haben TIR- und MPSR-Systeme sehr ähnliche Model-Checking-Eigenschaften, und wir erhalten analoge Ergebnisse bezüglich ihrer Trace-Sprachen.Wir untersuchen außerdem zwei Varianten von TIR-Systemen. In der ersten können Marker durch Ersetzungsschritte gelöscht werden. Durch eine Adaption der Saturierungsmethode, wie sie von Pushdown-Systemen bekannt ist, zeigen wir, dass solche Systeme die Regularität von Sprachen erhalten. Die zweite Variante erlaubt es, einem Wort weitere Marker durch Ersetzungsschritte hinzuzufügen. Solche Systeme erhalten nicht die Regularität von Sprachen, erlauben aber trotzdem noch eine algorithmische Erreichbarkeitsanalyse.

Word rewriting systems have been studied over the last century under several aspects. In the beginning, they were considered as a framework for the representation of computation processes and as a tool for generating formal languages. In more recent years, they have also been investigated as a mechanism to represent infinite graphs by a finite formalism. This thesis has its main focus in the latter domain. In the first part of the thesis, we investigate mixed prefix/suffix rewriting (MPSR) systems, which combine prefix and suffix rewriting in a nondeterministic way. We study central algorithmic properties of the graphs that can be generated by such systems, with an emphasis on the reachability problem (as a master problem in model-checking), and we determine the connection between the classes of such graphs and other well-studied graph classes, such as the classes of prefix recognizable and of automatic graphs. Furthermore, we study the class of trace languages of graphs that are generated by MPSR systems, and we show that this class strictly includes the class of context-free languages, and is itself properly included in the class of context-sensitive languages. In the second part of the thesis, we introduce and investigate tagged infix rewriting (TIR) systems, which extend the MPSR systems, and which use special markers for a restricted form of infix rewriting. We show that in their basic form, where the markers may not be rewritten, TIR and MPSR systems share a number of model-checking properties, and we obtain analogous results concerning their trace languages.We also study two variants of TIR systems. For the first, where markers may be removed by rewriting steps, we show that such systems preserve regularity of languages under rewriting, by adapting the saturation method as known for pushdown systems. In the second variant, where markers may be added by rewriting steps, this does not hold; however, we show that an algorithmic reachability analysis is still possible.

Fulltext:
PDF