Символдық верификация

CTL үшін model checking әдісімен верификациялау міндеті келесіден тұрады: Крипке М құрылымы және тармақталған уақыт логикасының (CTL) темпоралдық формуласы берілген. Ф орындалатын Крипке М құрылымының көптеген жағдайларын табу . Егер бастапқы жағдай S0 болса , онда Ф М үшін орындалады .

CTL логика ф берілген формуласының әрбір подформуласы үшін model checking символдық алгоритмі сипаттамалық түйреуіш функциясын құрастырады Q күйлерінің көп санын есептейтін Крипке М құрылымы, онда ср формуласы орындалады. Бұл жағдайда операциялар көптеген күйлерден емес, BDD түріндегі сипаттамалық буль функцияларынан орындалады. CTL формуласының әртүрлі ішкі пішімдері үшін бұл өзінше жасалады. CTL формулаларының түрлері оларды синтаксиспен анықтайды