mathend000#.
- Spur =
mathend000# eine Folge von Paaren
von Zustand und Aktion,
- ein Zustand
ist eine Belegung der Prädikatsymbole,
- jede Aktion zerstört
alle Zustandsinformation.
Satz: Diese Spursprachen
(von goto- und while-Programmen)
sind regulär.
Beweis: Konstruktion über endlichen Automaten.
- Zustandsmenge =
mathend000# Prädikatbelegungen ×
mathend000# Anweisungs-Nummer
- Transitionen? (Beispiele)
Damit ist Spur-Äquivalenz von Programmen entscheidbar.
Beziehung zu tatsächlicher Äquivalenz?
Johannes Waldmann
2014-03-31