Beschränkte Rekursion

beliebige Rekursion kann zu unendlichen Zustandsgraphen und nicht-regulären (Spur-)Sprachen führen.

Falls das nicht gewünscht ist, dann Syntax einschränken:

• μP.((a→P;c)b)

  Spursprache: ...

  Folgerung: Einschränken auf rechts-lineare Ausdrücke (P darf niemals links von ; stehen)

• Simulation von ; durch |_S:

  μP.((a→P|_aac)b)

  Folgerung: P darf gar nicht in |_S vorkommen