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

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

Мен берген жай-күй жиынының айқын алгоритмі <2 ef< f0Qq күйлері және көптеген R өткелдері 3-бөлімде қаралды. Мұндай күйлерді табу алгоритмі £?ЕҒф, оның ішіндеқадамдардың ақырғы саны Сф күйлеріне қол жеткізуге болады, схемаға боладыосылай ұсыну:

Бұл алгоритм efq формуласын рекурсивті анықтауға негізделеді.:

Ең алдымен ізделетін және жай-күй жиыны үшін көптеген Qp қабылданады, яғни ф формуласымен белгіленген жағдайлар.Содан кейін көптеген күйлерге А күйлеріне ауысу (бір қадам) бар күй қосылады . Мұндай түрлендіру бірнеше рет А көп пайда болғанша жасалады, оны өзгертпейтін түрлендіруді қолдану

Ең алдымен ізделетін және жай-күй жиыны үшін көптеген Qp қабылданады, яғни ф формуласымен белгіленген жағдайлар.Содан кейін көптеген күйлерге А күйлеріне ауысу (бір қадам) бар күй қосылады . Мұндай түрлендіру бірнеше рет А көп пайда болғанша жасалады, оны өзгертпейтін түрлендіруді қолдану

Алайда, сұрақ туындайды: алгоритм (яғни, Крипке құрылымының жай-күйінің астыңғы жиынына кейбір түрлендіруді қайталанатын қолдану қозғалмайтын нүктеге алып келеді ме) және нәтижесінде алынған көптеген күйлер бізге қажет (тиісті формуланы қанағаттандыратын жағдайлардың барлығы осы жиынға кіреді ме).

Алайда, сұрақ туындайды: алгоритм (яғни, Крипке құрылымының жай-күйінің астыңғы жиынына кейбір түрлендіруді қайталанатын қолдану қозғалмайтын нүктеге алып келеді ме) және нәтижесінде алынған көптеген күйлер бізге қажет (тиісті формуланы қанағаттандыратын жағдайлардың барлығы осы жиынға кіреді ме).

Бұл сұрақтарға жауаптар, басқаша айтқанда, көптеген түрлендірулерді қайталанатын қолданудан тұратын, белгісіз алгоритмдерді қолданудың теориялық негіздемесі предикат торларындағы операторлардың қозғалмайтын нүктесінің теориясын береді.

Бұл сұрақтарға жауаптар, басқаша айтқанда, көптеген түрлендірулерді қайталанатын қолданудан тұратын, белгісіз алгоритмдерді қолданудың теориялық негіздемесі предикат торларындағы операторлардың қозғалмайтын нүктесінің теориясын береді.

Соңы