Poznámka:

Předchozí definice předpokládá množinu jmen vnitřních sběrnic na rozdíl od jednoho jména uvažovaného v citované definici. Síť tedy může obsahovat více různých vnitřních sběrnic. Kdybychom měli pouze jedno jméno pro vnitřní sběrnici, nemohli bychom při transformaci do CCS od sebe rozlišit určité synchronizace (viz násl. kapitola).

Další drobný technický rozdíl od citované definice je v části definice termu proces a to v tom, že vycházíme z přechodového grafu. V přechodovém grafu (grafické podobě procesu) nepožadujeme, aby byl počáteční stav nutně určen. Požadavek existence právě jednoho počátečního stavu je nutný z hlediska sémantiky procesu jako přechodového systému s návěštími.

Aby modifikovaná definice zůstala korektní v souladu s citovanou definicí, předpokládáme, že počáteční stav je určen. Problém nedefinovaného počátečního stavu řeší následující lemma.

5mm