aufgabekann mir jemandsagen, wann genau eine rekursive spezifikation linear ist?am besten in klaren worten, weil die aussage im skript mir nichts sagt… ;)
Dabei ist Definition 4.42 im Skript schon ziemlich wortreich, der ist eigentlich nichts mehr hinzuzufügen.
Eine rekursive Spezifikation ist genau dann linear, wenn jede Zeile des Gleichungssystems genau der in der Definition genannten Syntax entspricht:
- Auf der linken Seite steht genau ein Variablensymbol.
- Auf der rechten Seite steht eine Summe aus Prozesstermen (der Einfachheit halber durchnummeriert von 1 bis k und von 1 bis l), welche jeweils wiederum entweder aus genau einer Aktion und einem Variablensymbol oder aus genau nur einer Aktion bestehen.
Beispiele:
- X = aY; Y = bX + c ist linear.
- X = aXb + c ist nicht linear.
Allerdings wäre auch
X = (a+a)Y; Y = bX + c nach dieser Definition
nicht linear, obwohl die Lösung äquivalent zum ersten Beispiel ist. Die Definition ist also zu korrigieren:
… ist linear, wenn ihre rekursiven Gleichungen in die folgende Form überführt werden können: …
Die im Skript folgende Behauptung, dass geschützte lineare Spezifikationen
genau diejenigen mit einer eindeutigen Lösung modulo initialer Verzweigungsbisimulation sind, wäre sonst nicht zu halten.
(Der Formulierungsfehler im Skript stammt direkt aus dem Buch von Fokking, welcher leider ebenfalls die Überführungsmöglichkeit außer Acht gelassen hat.)
Edit: Definitionskorrektur nach Rücksprache mit Herrn Valk und Moldt ergänzt.
