Ersetzungssysteme und Programmanalyse

• R ein Ersetzungssystem, L eine Sprache (Menge) von Bäumen,
  R^*(L) = {t | $$\exists$$s $$\in$$ L : s$$\to_{R}^{*}$$t}
  alle Mehr-Schritt-Nachfolger von L.
• modelliert: R ein Programm, L eine Menge von (möglichen) Eingaben, dann R^*(L) Menge von erreichbaren Zuständen (Zwischenergebnissen)
• E eine Menge von verbotenen Zuständen. Kein verbotener Zustand erreichbar: R^*(L) $\cap$ E = $\emptyset$
• Beispiel: durch XSLT-Transformation soll immer Schema-konformes Dokument entstehen