next up previous contents
Next: Příklad . Up: Jazyk termů GCCS Previous: Lemma .

Důkaz:

Uvažme přechodový graf , v němž není určen počáteční stav. Idea je přidat, případně najít mezi všemi stavy systému, takový stav, který lze považovat za počáteční. V případě, že mezi stavy přechodového grafu existují takové, do nichž nevede žádný přechod, jsou tyto stavy potenciálními kandidáty na počáteční stav. Pokud je takový stav právě jeden, zvolíme jej počátečním stavem. Pokud je jich více, tyto stavy odebereme z grafu a přidáme nový stav simulující význam odebraných stavů.

Pokud takové izolované stavy neexistují, zvolíme za počáteční stav libovolný z existujících stavů přechodového grafu. Formální zápis následuje:

Označme .



David Safranek
Fri Apr 6 23:53:25 MET DST 2001