Abstrakt
Typický problém při použití techniky automatického ověřování je velikost stavového prostoru. Dokonce i v případě malého systému narůstá stavový prostor exponenciálně (problém 'state explosion').
V tomto článku prezentujeme novou reprezentaci stavového prostoru pro implementaci operací nad protokoly chování softwarových komponent. Navrhovaná reprezentace je lineární vzhledem k velikosti protokolu chování.
Omezení prostorové náročnosti při nárustu časové náročnosti umožňuje verifikaci prokotolů praktické velikosti. Jako důkaz použitelnosti nové reprezentace diskutujeme dvě verze nástroje pro verifikaci.