6 Представления неподвижной точки в CTL. Алгоритм символьной верификации моделей в CTL (1185958), страница 4
Текст из файла (страница 4)
äëÿ êàæäîãî ïðîöåññà P ïðîâåðÿåìîéSðàñïðåäåëåííîéñèñòåìû Syst ñòðîèòñÿ ROBDD RP = act∈P Ract ,îïèñûâàþùàÿ îòíîøåíèå ïåðåõîäîâ ýòîãî ïðîöåññà.3. äëÿ ïðîâåðÿåìîé ðàñïðåäåëåííîé ñèñòåìû Syst âçàâèñèìîñòè îò âèäà ïàðàëëåëüíîé êîìïîçèöèè ñòðîèòñÿROBDD RSyst =kP∈Syst RP , îïèñûâàþùàÿ îòíîøåíèåïåðåõîäîâ ñèñòåìû.4. ê ïîñòðîåííîé ROBDD RSyst è CTL ñïåöèôèêàöèè ϕïðèìåíÿåòñÿ ïðîöåäóðà Check(ϕ, RSyst ) è ïðîâåðÿåòñÿóñëîâèå S0 ⊆ Check(ϕ, RSyst ) .Íà êàêîì ýòàïå âîçíèêàþò ñàìûå áîëüøèå òðóäíîñòè?Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÓïðàæíåíèå.Ïðèìåíèòå ïðîöåäóðû âû÷èñëåíèÿ íàèìåíüøåé íåïîäâèæíîéòî÷êè è íàèáîëüøåé íåïîäâèæíîé òî÷êè äëÿ ïðîâåðêèâûïîëíèìîñòè ôîðìóë CTL íà ìîäåëè è ïðîâåðüòå, â êàêèõñîñòîÿíèé s ñîáëþäàþòñÿ îòíîøåíèÿ âûïîëíèìîñòè M, s |= ϕäëÿ ïðèâåäåííûõ íèæå ôîðìóë íà ìîäåëè M ,LfpGfpI AF qI AG(AF(p∨ r ))I EX EX rI AG A[q Rp]Ñèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÌîäåëü M s0 s q, r sp, q3kI@@@@6@@s1 ?r6&%@@ - p, t s2ÊÎÍÅÖ ËÅÊÖÈÈ 6..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
