Abstrakt
Ověřování správnosti chování u rozsáhných komponentových systémů trpí strmým růstem stavů, zvláště jsou-li součástí systémů současně probíhající aktivity. Pro protokoly chování prezentujeme metodu redukce růstu stavů založenou na aplikování redukujících pravidel přímo u specifikace.
Současně uvádíme příklad, který má představit sílu této metody, kdy je specifikace redukována pouze na zlomek své původní velikosti.