Reachability over word rewriting systems

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