I am deeply indebted to Franz Baader and Carsten Lutz, my thesis advisors, for their valuable guidance of my researching work and constant support of all technical problems. Without either of them, this thesis would not exist. I am grateful to Maja Miličic ́ and Frank Wolter who have also helped me a lot in the last four years. I would like to thank Conrad Drescher, Boontawee Suntisrivaraporn, and Rafael Peñaloza for proofreading the preliminary version of my thesis. I would also like to thank all members of the chair for automata theory. It is a pleasure to work with you. Many thanks go to our secretary, Kerstin Achtruth, for her support in countless matters. I am also thankful to Anni-Yasmin Turhan for her encouragement. I would like to...