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í.