Abstrakt
Jedním z vážných problémů metody 'model checking' je 'state explosion' problém, který zabraňuje použití této metody pro běžné ladící nástroje. Navrhujeme proto novou metodu identifikace stavů založenou na bitových polích, která významným způsobem sníží nároky na výpočetní čas i paměť potřebné pro testování protokolů chování.