Лекция 4. Логика вычисления программ. CTL. LTL (1185526), страница 3

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 3)

Áîëååñòðîãîå îïðåäåëåíèå ôîðìóë ïóòè LTL òàêîâî.I Åñëè p ∈ AP , òî f ôîðìóëà ïóòè.I Åñëè f è g ôîðìóëû ïóòè, òî ¬f , f ∧ g , f ∨ g ,f, f, f , f g , f g ôîðìóëû ïóòè.AXGUFRÏðèìåðû.(A FG(passive → (active U XAG óñëîâèå ñëàáîé ñïðàâåäëèâîñòè;passive)) .enabled → G F fired)CTL è LTLÂñå òðè ëîãèêè èìåþò ðàçíûå âûðàçèòåëüíûå âîçìîæíîñòè.Óòâåðæäåíèå 4.Íå ñóùåñòâóåò CTL-ôîðìóëû, ýêâèâàëåíòíîé LTL-ôîðìóëå(FG stable) .Ýòà ôîðìóëà âûðàæàåò ñëåäóþùåå ñâîéñòâî æèâîñòè: ïðèëþáîì ñöåíàðèè ðàçâèòèÿ ñîáûòèé ñèñòåìà ðàíî èëè ïîçäíîñòàáèëèçèðóåòñÿ è áóäåò äàëåå îñòàâàòüñÿ ñòàáèëüíîé.AÄîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî [Òðóäíàÿ çàäà÷à! Áóäåò âûñîêî îöåíåíà!] .CTL è LTLÓòâåðæäåíèå 5.Íå ñóùåñòâóåò LTL ôîðìóëû, êîòîðàÿ áûëà áû ýêâèâàëåíòíàCTL-ôîðìóëå ( restart) .Ýòà ôîðìóëà âûðàæàåò ñëåäóþùåå ñâîéñòâî: ïðè ëþáîìñöåíàðèè ðàçâèòèÿ ñîáûòèé ñèñòåìà âñåãäà èìååò âîçìîæíîñòüïåðåçàãðóçèòüñÿ.AGEFÄîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî [Òðóäíàÿ çàäà÷à! Áóäåò âûñîêî îöåíåíà!] .CTL è LTLÓòâåðæäåíèå 5.Íå ñóùåñòâóåò LTL ôîðìóëû, êîòîðàÿ áûëà áû ýêâèâàëåíòíàCTL-ôîðìóëå ( restart) .Ýòà ôîðìóëà âûðàæàåò ñëåäóþùåå ñâîéñòâî: ïðè ëþáîìñöåíàðèè ðàçâèòèÿ ñîáûòèé ñèñòåìà âñåãäà èìååò âîçìîæíîñòüïåðåçàãðóçèòüñÿ.AGEFÄîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî [Òðóäíàÿ çàäà÷à! Áóäåò âûñîêî îöåíåíà!] .À äèçúþíêöèÿ ýòèõ äâóõ ôîðìóë (FG p) ∨ ( p)ÿâëÿåòñÿ ôîðìóëîé CTL∗, êîòîðóþ íåëüçÿ âûðàçèòü íè â CTL,íè â LTL.AAGEFCTLÌû îãðàíè÷èìñÿ ïîäðîáíûì èçó÷åíèåì CTL.

Èìåþòñÿ äåñÿòüîñíîâíûõ îïåðàòîðîâ CTL:I AX è EX ,I AF è EF ,I AG è EG ,I AU è EU ,I AR è ER .CTLËîãèêà äåðåâüåâ âû÷èñëåíèé CTLI , s0 |= AGps0yp = trueHHHHHHH s 2s 1 jH yp = trueyp = true@@@s3 ?s4s5@R y@p = true yp = true yp = true@@@s6s7 ?s8s9 ?s10@?s11Ry@yyyyyp = truep = truep = truep = truep = truep = trueCTLËîãèêà äåðåâüåâ âû÷èñëåíèé CTLI , s0 |= EGps0s6yyp = trueHHHHHHH s 2s 1 jH yp = truey@@@s3 ?s4s5@R y@p = true yy@@@s7 ?s8s9 ?s10@?s11Ry@yyyyp = trueCTLËîãèêà äåðåâüåâ âû÷èñëåíèé CTLI , s0 |= AFps0yHHHHHHH s 2s 1 jH yy@@s3 ?p = true y@s4p = true ys5@R y@@@s6ys7 ?y@s8@Ry@s9 ?ys10yp = true?s11yp = trueCTLËîãèêà äåðåâüåâ âû÷èñëåíèé CTLI , s0 |= EFps0yHHHHHHH s 2s 1 jH yy@@s3 ?ys4@ys5@R y@@@s6ys7 ?yp = true@s8@Ry@s9 ?ys10y?s11yËîãèêà äåðåâüåâ âû÷èñëåíèé CTLÊàæäûé èç ýòèõ îïåðàòîðîâ ìîæåò áûòü âûðàæåí ïðè ïîìîùèâñåãî ëèøü òðåõ îïåðàòîðîâ EX , EG è EU :If ≡¬(¬f ) ;If ≡ [True f ] ;If ≡ ¬ (¬f ) ;If ≡¬(¬f ) ;I[f g ] ≡ ¬ [¬g (¬f ∧ ¬g )] ∧ ¬¬g ;I[f g ] ≡ ¬ [¬f ¬g ] ;I[f g ] ≡ ¬ [¬f ¬g ] .AXEXEFEUAGEFAFEGAUEUAREUERAUEGËîãèêà äåðåâüåâ âû÷èñëåíèé CTLÍåêîòîðûå òèïè÷íûå CTL-ôîðìóëû, êîòîðûå âîçíèêàþò ïðèâåðèôèêàöèè ñèñòåì ïàðàëëåëüíûõ ïðîãðàìì ñ êîíå÷íûì÷èñëîì ñîñòîÿíèé, ïðèâîäÿòñÿ íèæå:Ëîãèêà äåðåâüåâ âû÷èñëåíèé CTLÍåêîòîðûå òèïè÷íûå CTL-ôîðìóëû, êîòîðûå âîçíèêàþò ïðèâåðèôèêàöèè ñèñòåì ïàðàëëåëüíûõ ïðîãðàìì ñ êîíå÷íûì÷èñëîì ñîñòîÿíèé, ïðèâîäÿòñÿ íèæå:I(Start ∧ ¬Ready ) : ìîæíî äîñòè÷ü òàêîãî ñîñòîÿíèÿ, âêîòîðîì óñëîâèå Start âûïîëíÿåòñÿ, à Ready íåò;EFËîãèêà äåðåâüåâ âû÷èñëåíèé CTLÍåêîòîðûå òèïè÷íûå CTL-ôîðìóëû, êîòîðûå âîçíèêàþò ïðèâåðèôèêàöèè ñèñòåì ïàðàëëåëüíûõ ïðîãðàìì ñ êîíå÷íûì÷èñëîì ñîñòîÿíèé, ïðèâîäÿòñÿ íèæå:I(Start ∧ ¬Ready ) : ìîæíî äîñòè÷ü òàêîãî ñîñòîÿíèÿ, âêîòîðîì óñëîâèå Start âûïîëíÿåòñÿ, à Ready íåò;I(Req →Ack) : êîãäà áû íè áûë ïîëó÷åí çàïðîñ, îíðàíî èëè ïîçäíî áóäåò ïîäòâåðæäåí;EFAGAFËîãèêà äåðåâüåâ âû÷èñëåíèé CTLÍåêîòîðûå òèïè÷íûå CTL-ôîðìóëû, êîòîðûå âîçíèêàþò ïðèâåðèôèêàöèè ñèñòåì ïàðàëëåëüíûõ ïðîãðàìì ñ êîíå÷íûì÷èñëîì ñîñòîÿíèé, ïðèâîäÿòñÿ íèæå:I(Start ∧ ¬Ready ) : ìîæíî äîñòè÷ü òàêîãî ñîñòîÿíèÿ, âêîòîðîì óñëîâèå Start âûïîëíÿåòñÿ, à Ready íåò;I(Req →Ack) : êîãäà áû íè áûë ïîëó÷åí çàïðîñ, îíðàíî èëè ïîçäíî áóäåò ïîäòâåðæäåí;I(DeviceEnabled) : óñëîâèå DeviceEnabledâûïîëíÿåòñÿ áåñêîíå÷íî ÷àñòî íà êàæäîì ïóòèâû÷èñëåíèÿ;EFAGAGAFAFËîãèêà äåðåâüåâ âû÷èñëåíèé CTLÍåêîòîðûå òèïè÷íûå CTL-ôîðìóëû, êîòîðûå âîçíèêàþò ïðèâåðèôèêàöèè ñèñòåì ïàðàëëåëüíûõ ïðîãðàìì ñ êîíå÷íûì÷èñëîì ñîñòîÿíèé, ïðèâîäÿòñÿ íèæå:I(Start ∧ ¬Ready ) : ìîæíî äîñòè÷ü òàêîãî ñîñòîÿíèÿ, âêîòîðîì óñëîâèå Start âûïîëíÿåòñÿ, à Ready íåò;I(Req →Ack) : êîãäà áû íè áûë ïîëó÷åí çàïðîñ, îíðàíî èëè ïîçäíî áóäåò ïîäòâåðæäåí;I(DeviceEnabled) : óñëîâèå DeviceEnabledâûïîëíÿåòñÿ áåñêîíå÷íî ÷àñòî íà êàæäîì ïóòèâû÷èñëåíèÿ;I( Restart) : èç ëþáîãî äîñòîæèìîãî ñîñòîÿíèÿäîñòèæèìî ñîñòîÿíèå Restart .EFAGAFAGAFAGEFÏðîâåðüòå âûïîëíèìîñòü ôîðìóë CTL âçàäàííîé ìîäåëè.$'&r%s0 @@@@s1 p, t, rp, q s36?1.q, r s2M1 , s0 |= AF t@ R@Ïðîâåðüòå âûïîëíèìîñòü ôîðìóë CTL âçàäàííîé ìîäåëè.$'&r%s0 @@@@s1 p, t, rp, q s36?2.q, r s2M1 , s0 |= E[t U q]@ R@Ïðîâåðüòå âûïîëíèìîñòü ôîðìóë CTL âçàäàííîé ìîäåëè.$'&r%s0 @@@@s1 p, t, rp, q s36?3.q, r s2M1 , s2 |= E[t U q]@ R@Ïðîâåðüòå âûïîëíèìîñòü ôîðìóë CTL âçàäàííîé ìîäåëè.$'&r%s0 @@@@s1 p, t, rp, q s36?4.q, r s2M1 , s0 |= AG(r ∨ q)@ R@Ïðîâåðüòå âûïîëíèìîñòü ôîðìóë CTL âçàäàííîé ìîäåëè.$'&r%s0 @@@@s1 p, t, rp, q s36?5.q, r s2M1 , s2 |= AG(r ∨ q)@ R@Ïðîâåðüòå âûïîëíèìîñòü ôîðìóë CTL âçàäàííîé ìîäåëè.s0s q, r sp, q3kI@@@@6@@s1?r66.&%M1 , s0 |= AG(AF(p ∨ r ))@@- p, t s2Ïðîâåðüòå âûïîëíèìîñòü ôîðìóë CTL âçàäàííîé ìîäåëè.s0s q, r sp, q3kI@@@@6@@s1?r67.&%M1 , s2 |= AG(AF(p ∨ r ))@@- p, t s2Çàïèøèòå ôîðìóëû ëîãèê CTL, àäåêâàòíîâûðàæàþùèå ñëåäóþùèå ñóæäåíèÿ.IËèôò, ïîäíÿâøèéñÿ íà âòîðîé ýòàæ, ìîæåò ñêîëü óãîäíîäîëãî îñòàâàòüñÿ íåïîäâèæíûì.Çàïèøèòå ôîðìóëû ëîãèê CTL, àäåêâàòíîâûðàæàþùèå ñëåäóþùèå ñóæäåíèÿ.IIËèôò, ïîäíÿâøèéñÿ íà âòîðîé ýòàæ, ìîæåò ñêîëü óãîäíîäîëãî îñòàâàòüñÿ íåïîäâèæíûì.Âñåãäà ïîñëå ïîëó÷åíèÿ çàïðîñà ðàíî èëè ïîçäíî áóäåòâûäàí îòâåò, åñëè òîëüêî çàïðîñ íå áóäåò îòìåíåí.Çàïèøèòå ôîðìóëû ëîãèê CTL, àäåêâàòíîâûðàæàþùèå ñëåäóþùèå ñóæäåíèÿ.IIIËèôò, ïîäíÿâøèéñÿ íà âòîðîé ýòàæ, ìîæåò ñêîëü óãîäíîäîëãî îñòàâàòüñÿ íåïîäâèæíûì.Âñåãäà ïîñëå ïîëó÷åíèÿ çàïðîñà ðàíî èëè ïîçäíî áóäåòâûäàí îòâåò, åñëè òîëüêî çàïðîñ íå áóäåò îòìåíåí.Åñëè âñëåä çà ñîáûòèåì p ïðîèñõîäèò ñîáûòèå q, òî ïîñëåýòîãî ñîáûòèå r íå íàñòóïèò äî òåõ ïîð, ïîêà íå ñëó÷èòñÿñîáûòèå t .Çàïèøèòå ôîðìóëû ëîãèê CTL, àäåêâàòíîâûðàæàþùèå ñëåäóþùèå ñóæäåíèÿ.IIIIËèôò, ïîäíÿâøèéñÿ íà âòîðîé ýòàæ, ìîæåò ñêîëü óãîäíîäîëãî îñòàâàòüñÿ íåïîäâèæíûì.Âñåãäà ïîñëå ïîëó÷åíèÿ çàïðîñà ðàíî èëè ïîçäíî áóäåòâûäàí îòâåò, åñëè òîëüêî çàïðîñ íå áóäåò îòìåíåí.Åñëè âñëåä çà ñîáûòèåì p ïðîèñõîäèò ñîáûòèå q, òî ïîñëåýòîãî ñîáûòèå r íå íàñòóïèò äî òåõ ïîð, ïîêà íå ñëó÷èòñÿñîáûòèå t .Âî âñåõ âû÷èñëåíèÿõ ñîáûòèå q ïðåäøåñòâóåò ñîáûòèÿì pè r.Çàïèøèòå ôîðìóëû ëîãèê CTL, àäåêâàòíîâûðàæàþùèå ñëåäóþùèå ñóæäåíèÿ.IIIIIËèôò, ïîäíÿâøèéñÿ íà âòîðîé ýòàæ, ìîæåò ñêîëü óãîäíîäîëãî îñòàâàòüñÿ íåïîäâèæíûì.Âñåãäà ïîñëå ïîëó÷åíèÿ çàïðîñà ðàíî èëè ïîçäíî áóäåòâûäàí îòâåò, åñëè òîëüêî çàïðîñ íå áóäåò îòìåíåí.Åñëè âñëåä çà ñîáûòèåì p ïðîèñõîäèò ñîáûòèå q, òî ïîñëåýòîãî ñîáûòèå r íå íàñòóïèò äî òåõ ïîð, ïîêà íå ñëó÷èòñÿñîáûòèå t .Âî âñåõ âû÷èñëåíèÿõ ñîáûòèå q ïðåäøåñòâóåò ñîáûòèÿì pè r.Âî âñåõ âû÷èñëåíèÿõ ìåæäó ñîáûòèÿìè p è q íè ðàçó íåïðîèñõîäèò ñîáûòèÿ r .Çàïèøèòå ôîðìóëû ëîãèê CTL, àäåêâàòíîâûðàæàþùèå ñëåäóþùèå ñóæäåíèÿ.IIIIIIËèôò, ïîäíÿâøèéñÿ íà âòîðîé ýòàæ, ìîæåò ñêîëü óãîäíîäîëãî îñòàâàòüñÿ íåïîäâèæíûì.Âñåãäà ïîñëå ïîëó÷åíèÿ çàïðîñà ðàíî èëè ïîçäíî áóäåòâûäàí îòâåò, åñëè òîëüêî çàïðîñ íå áóäåò îòìåíåí.Åñëè âñëåä çà ñîáûòèåì p ïðîèñõîäèò ñîáûòèå q, òî ïîñëåýòîãî ñîáûòèå r íå íàñòóïèò äî òåõ ïîð, ïîêà íå ñëó÷èòñÿñîáûòèå t .Âî âñåõ âû÷èñëåíèÿõ ñîáûòèå q ïðåäøåñòâóåò ñîáûòèÿì pè r.Âî âñåõ âû÷èñëåíèÿõ ìåæäó ñîáûòèÿìè p è q íè ðàçó íåïðîèñõîäèò ñîáûòèÿ r .Âî âñåõ âû÷èñëåíèÿõ ñîáûòèå p ïðîèñõîäèò íå áîëåå äâóõðàç.Çàïèøèòå ôîðìóëû ëîãèê CTL, àäåêâàòíîâûðàæàþùèå ñëåäóþùèå ñóæäåíèÿ.IIIIIIIËèôò, ïîäíÿâøèéñÿ íà âòîðîé ýòàæ, ìîæåò ñêîëü óãîäíîäîëãî îñòàâàòüñÿ íåïîäâèæíûì.Âñåãäà ïîñëå ïîëó÷åíèÿ çàïðîñà ðàíî èëè ïîçäíî áóäåòâûäàí îòâåò, åñëè òîëüêî çàïðîñ íå áóäåò îòìåíåí.Åñëè âñëåä çà ñîáûòèåì p ïðîèñõîäèò ñîáûòèå q, òî ïîñëåýòîãî ñîáûòèå r íå íàñòóïèò äî òåõ ïîð, ïîêà íå ñëó÷èòñÿñîáûòèå t .Âî âñåõ âû÷èñëåíèÿõ ñîáûòèå q ïðåäøåñòâóåò ñîáûòèÿì pè r.Âî âñåõ âû÷èñëåíèÿõ ìåæäó ñîáûòèÿìè p è q íè ðàçó íåïðîèñõîäèò ñîáûòèÿ r .Âî âñåõ âû÷èñëåíèÿõ ñîáûòèå p ïðîèñõîäèò íå áîëåå äâóõðàç.Âî âñåõ âû÷èñëåíèÿõ ñîáûòèå p ïðîèñõîäèò êîíå÷íîå÷èñëî ðàç.Êàêèå èç ïàð ôîðìóë, ïðèâåäåííûõ íèæå, ÿâëÿþòñÿýêâèâàëåíòíûìè?Iϕèϕ;EFEGÊàêèå èç ïàð ôîðìóë, ïðèâåäåííûõ íèæå, ÿâëÿþòñÿýêâèâàëåíòíûìè?Iϕèϕ;Iϕ∨ψè(ϕ ∨ ψ);EFEGEFEFEFÊàêèå èç ïàð ôîðìóë, ïðèâåäåííûõ íèæå, ÿâëÿþòñÿýêâèâàëåíòíûìè?Iϕèϕ;Iϕ∨ψè(ϕ ∨ ψ);Iϕ∨ψè(ϕ ∨ ψ);EFEGEFEFEFAFAFAFÊàêèå èç ïàð ôîðìóë, ïðèâåäåííûõ íèæå, ÿâëÿþòñÿýêâèâàëåíòíûìè?Iϕèϕ;Iϕ∨ψè(ϕ ∨ ψ);Iϕ∨ψè(ϕ ∨ ψ);I AF ¬ϕ è ¬ϕ;EFEGEFEFEFAFAFAFEGÊàêèå èç ïàð ôîðìóë, ïðèâåäåííûõ íèæå, ÿâëÿþòñÿýêâèâàëåíòíûìè?Iϕèϕ;Iϕ∨ψè(ϕ ∨ ψ);Iϕ∨ψè(ϕ ∨ ψ);I AF ¬ϕ è ¬ϕ;I EF ¬ϕ è ¬ϕ;EFEGEFEFEFAFAFAFEGAFÊàêèå èç ïàð ôîðìóë, ïðèâåäåííûõ íèæå, ÿâëÿþòñÿýêâèâàëåíòíûìè?Iϕèϕ;Iϕ∨ψè(ϕ ∨ ψ);Iϕ∨ψè(ϕ ∨ ψ);I AF ¬ϕ è ¬ϕ;I EF ¬ϕ è ¬ϕ;I[ϕ1[ϕ2 ϕ3 ]] è [ [ϕ1 ϕ2 ] ϕ3 ];EFEGEFEFEFAFAFAFEGAFAUAUA AUUÊàêèå èç ïàð ôîðìóë, ïðèâåäåííûõ íèæå, ÿâëÿþòñÿýêâèâàëåíòíûìè?Iϕèϕ;Iϕ∨ψè(ϕ ∨ ψ);Iϕ∨ψè(ϕ ∨ ψ);I AF ¬ϕ è ¬ϕ;I EF ¬ϕ è ¬ϕ;I[ϕ1[ϕ2 ϕ3 ]] è [ [ϕ1 ϕ2 ] ϕ3 ];I true èϕ →ϕ.EFEGEFEFEFAFAFAFEGAFAUAAFUA AEGUUÊÎÍÅÖ ËÅÊÖÈÈ 4..

Характеристики

Список файлов лекций