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

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

Текст из файла

Ìåòîäûâåðèôèêàöèèïðîãðàìì è ñõåìËÅÊÒÎÐ:Âëàäèìèð Àíàòîëüåâè÷ Çàõàðîâzakh@cs.msu.suËåêöèÿ 4.Ñâîéñòâà âû÷èñëåíèé ïðîãðàììÊëàññèôèêàöèÿ ñâîéñòââû÷èñëåíèé ïðîãðàììÎãðàíè÷åíèÿ ñïðàâåäëèâîñòè∗Ëîãèêà äåðåâüåâ âû÷èñëåíèé CTLÒåìïîðàëüíûå ëîãèêè CTL è LTLÑâîéñòâà âû÷èñëåíèé ïðîãðàììÂû÷èñëåíèå ðåàãèðóþùåé ñèñòåìû (óïðàâëÿþùåéïðîãðàììû, ïðîòîêîëà, ñõåìû) ñîïðîâîæäàåòñÿîñóùåñòâëåíèåì ñîáûòèé.Ìíîãèå ðåàãèðóþùèå ñèñòåìû ïðîåêòèðóþò òàê,÷òîáû èõ âû÷èñëåíèÿ âîîáùå íèêîãäà íåçàâåðøàëèñü.Ïîýòîìó ÿçûêè ñïåöèôèêàöèé ðåàãèðóþùèõñèñòåì äîëæíû ïîçâîëÿòü îïèñûâàòü áåñêîíå÷íûåïîñëåäîâàòåëüíîñòè ñîáûòèé, ïðîèñõîäÿùèå ïîõîäó âû÷èñëåíèÿ ñèñòåìû.Ñâîéñòâà âû÷èñëåíèé ïðîãðàììÏåðåêðåñòîê ñî ñâåòîôîðàìèyiyL2i L1Ñâîéñòâà âû÷èñëåíèé ïðîãðàììÏåðåêðåñòîê ñî ñâåòîôîðàìèiyiL2y L1Ñâîéñòâà âû÷èñëåíèé ïðîãðàììÏåðåêðåñòîê ñî ñâåòîôîðàìèiiyL2y L1Ñâîéñòâà âû÷èñëåíèé ïðîãðàììÏåðåêðåñòîê ñî ñâåòîôîðàìèyiiL2y L1Ñâîéñòâà âû÷èñëåíèé ïðîãðàììÏåðåêðåñòîê ñî ñâåòîôîðàìèyyiL2i L1Ñâîéñòâà âû÷èñëåíèé ïðîãðàììÊàæäîå ñîñòîÿíèå ñèñòåìû ðåãóëèðîâêèäîðîæíîãî äâèæåíèÿ õàðàêòåðèçóåòñÿ ñîáûòèåì ñîâîêóïíîñòüþ àêòèâíûõ öâåòîâ ñâåòîôîðîâ.Ñâîéñòâà âû÷èñëåíèé ïðîãðàììÊàæäîå ñîñòîÿíèå ñèñòåìû ðåãóëèðîâêèäîðîæíîãî äâèæåíèÿ õàðàêòåðèçóåòñÿ ñîáûòèåì ñîâîêóïíîñòüþ àêòèâíûõ öâåòîâ ñâåòîôîðîâ.Êàæäîå âû÷èñëåíèå ñèñòåìû õàðàêòåðèçóåòñÿòðàññîé ïîñëåäîâàòåëüíîñòüþ ñîáûòèé.Ñâîéñòâà âû÷èñëåíèé ïðîãðàììÊàæäîå ñîñòîÿíèå ñèñòåìû ðåãóëèðîâêèäîðîæíîãî äâèæåíèÿ õàðàêòåðèçóåòñÿ ñîáûòèåì ñîâîêóïíîñòüþ àêòèâíûõ öâåòîâ ñâåòîôîðîâ.Êàæäîå âû÷èñëåíèå ñèñòåìû õàðàêòåðèçóåòñÿòðàññîé ïîñëåäîâàòåëüíîñòüþ ñîáûòèé.Ïîâåäåíèå ñèñòåìû õàðàêòåðèçóåòñÿ ñâîéñòâîì ìíîæåñòâîì òðàññ.Ñâîéñòâà âû÷èñëåíèé ïðîãðàììyi i L1iyL2Òðàññà:{red1 , green2 },Ñâîéñòâà âû÷èñëåíèé ïðîãðàììiy L1yiL2Òðàññà:{red1 , green2 }, {green1 , red2 },Ñâîéñòâà âû÷èñëåíèé ïðîãðàììiy L1iyL2Òðàññà:{red1 , green2 }, {green1 , red2 }, {green1 , green2 }Ñâîéñòâà âû÷èñëåíèé ïðîãðàììyy L1iiL2Òðàññà:{red1 , green2 }, {green1 , red2 }, {green1 , green2 }{red1 , green1 },Ñâîéñòâà âû÷èñëåíèé ïðîãðàììii L1iiL2Òðàññà:{red1 , green2 }, {green1 , red2 }, {green1 , green2 }{red1 , green1 }, ???Ñâîéñòâà âû÷èñëåíèé ïðîãðàììL1L2Òðàññà:{red1 , green2 }, {green1 , red2 }, {green1 , green2 }{red1 , green1 }, ∅,Ñâîéñòâà âû÷èñëåíèé ïðîãðàììÑâîéñòâà ñèñòåìû ðåãóëèðîâêè äîðîæíîãîäâèæåíèÿ:Ñâîéñòâà âû÷èñëåíèé ïðîãðàììÑâîéñòâà ñèñòåìû ðåãóëèðîâêè äîðîæíîãîäâèæåíèÿ:Ó êàæäîãî ñâåòîôîðà âñåãäà àêòèâåí âòî÷íîñòè îäèí öâåò;IÑâîéñòâà âû÷èñëåíèé ïðîãðàììÑâîéñòâà ñèñòåìû ðåãóëèðîâêè äîðîæíîãîäâèæåíèÿ:Ó êàæäîãî ñâåòîôîðà âñåãäà àêòèâåí âòî÷íîñòè îäèí öâåò;Ó êàæäîãî ñâåòîôîðà ðàíî èëè ïîçäíîàêòèâèçèðóåòñÿ çåëåíûé öâåò;IIÑâîéñòâà âû÷èñëåíèé ïðîãðàììÑâîéñòâà ñèñòåìû ðåãóëèðîâêè äîðîæíîãîäâèæåíèÿ:Ó êàæäîãî ñâåòîôîðà âñåãäà àêòèâåí âòî÷íîñòè îäèí öâåò;Ó êàæäîãî ñâåòîôîðà ðàíî èëè ïîçäíîàêòèâèçèðóåòñÿ çåëåíûé öâåò;Ó îáîèõ ñâåòîôîðîâ íèêîãäà íå áûâàåòîäíîâðåìåííî àêòèâåí çåëåíûé öâåò;IIIÑâîéñòâà âû÷èñëåíèé ïðîãðàììÑâîéñòâà ñèñòåìû ðåãóëèðîâêè äîðîæíîãîäâèæåíèÿ:Ó êàæäîãî ñâåòîôîðà âñåãäà àêòèâåí âòî÷íîñòè îäèí öâåò;Ó êàæäîãî ñâåòîôîðà ðàíî èëè ïîçäíîàêòèâèçèðóåòñÿ çåëåíûé öâåò;Ó îáîèõ ñâåòîôîðîâ íèêîãäà íå áûâàåòîäíîâðåìåííî àêòèâåí çåëåíûé öâåò;Ó êàæäîãî ñâåòîôîðà ïåðåìåíà àêòèâíûõöâåòîâ ñëó÷àåòñÿ áåñêîíå÷íî ÷àñòî.IIIIÑâîéñòâà âû÷èñëåíèé ïðîãðàììÁîëåå ôîðìàëüíî âñå ýòè ïîíÿòèÿ îïðåäåëÿþòñÿ òàê.Ïóñòü çàäàíî ìíîæåñòâî àòîìàðíûõ âûñêàçûâàíèé AP .ÒîãäàI ñîáûòèå ëþáîå ïîäìíîæåñòâî àòîìàðíûõ âûñêàçûâàíèé,E , E ⊆ AP ;I òðàññà ëþáàÿ áåñêîíå÷íàÿ ïîñëåäîâàòåëüíîñòü ñîáûòèé,α, α ∈ (2AP )ω ,α = E0 , E1 , E2 , .

. . ;Iñâîéñòâî âû÷èñëåíèé ëþáîå ìíîæåñòâî òðàññ,P, P ⊆ (2AP )ω .Ñâîéñòâà âû÷èñëåíèé ïðîãðàììÏóñòü çàäàíà ìîäåëü Êðèïêå M = (S, S0, R, L) è íåêîòîðûéïóòü π = s0, s1, s2, . . . èç íà÷àëüíîãî ñîñòîÿíèÿ s0, s0 ∈ S0 âýòîé ìîäåëè. Òîãäà òðàññîé ïóòè π íàçîâåì ïîñëåäîâàòåëüíîñòüα(π) = L(s0 ), L(s1 ), L(s2 ), . . .ìíîæåñòâ àòîìàðíûõ âûñêàçûâàíèé, èñòèííûõ â ñîñòîÿíèÿõýòîãî ïóòè.Ñîâîêóïíîñòü âñåõ òðàññ ìîäåëè Êðèïêå M îáîçíà÷èì çàïèñüþTr (M) .Ñâîéñòâà âû÷èñëåíèé ïðîãðàììÏóñòü çàäàíà ìîäåëü Êðèïêå M = (S, S0, R, L) è íåêîòîðûéïóòü π = s0, s1, s2, .

. . èç íà÷àëüíîãî ñîñòîÿíèÿ s0, s0 ∈ S0 âýòîé ìîäåëè. Òîãäà òðàññîé ïóòè π íàçîâåì ïîñëåäîâàòåëüíîñòüα(π) = L(s0 ), L(s1 ), L(s2 ), . . .ìíîæåñòâ àòîìàðíûõ âûñêàçûâàíèé, èñòèííûõ â ñîñòîÿíèÿõýòîãî ïóòè.Ñîâîêóïíîñòü âñåõ òðàññ ìîäåëè Êðèïêå M îáîçíà÷èì çàïèñüþTr (M) .Ãîâîðÿò, ÷òî ìîäåëü M óäîâëåòâîðÿåò ñâîéñòâó P(îáîçíà÷àåòñÿ M |= P ), åñëè âåðíî âêëþ÷åíèå Tr (M) ⊆ P .Ñâîéñòâà âû÷èñëåíèé ïðîãðàììÌîäåëü Êðèïêå M1 íàçûâàåòñÿ óòî÷íåíèåì ìîäåëè M2 , åñëèTr (M1 ) ⊆ Tr (M2 ) .Óòâåðæäåíèå 1.Åñëè ìîäåëü Êðèïêå óäîâëåòâîðÿåò íåêîòîðîìó ñâîéñòâó, òî èâñÿêîå åå óòî÷íåíèå òàêæå óäîâëåòâîðÿåò ýòîìó ñâîéñòâó.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî .Êëàññèôèêàöèÿ ñâîéñòâ âû÷èñëåíèéÍàèáîëåå ðàñïðîñòðàíåííûå ñâîéñòâà âû÷èñëåíèéïðîãðàìì ðàçäåëÿþòñÿ íà ñëåäóþùèå êëàññû:ñâîéñòâà áåçîïàñíîñòè (safety),ñâîéñòâà æèâîñòè (liveness),îãðàíè÷åíèÿ ñïðàâåäëèâîñòè (fairnessconstraints),IIIÊëàññèôèêàöèÿ ñâîéñòâ âû÷èñëåíèéÑâîéñòâî áåçîïàñíîñòè: ¾íè÷åãî ïëîõîãî íèêîãäà íå ñëó÷èòñÿ¿.Ñâîéñòâî âû÷èñëåíèé P íàçûâàåòñÿ ñâîéñòâîì áåçîïàñíîñòè ,åñëè îíî óäîâëåòâîðÿåò ñëåäóþùåìó òðåáîâàíèþ:I êàêîâà áû íè áûëà òðàññà α, α ∈ (2AP )ω \ P , ñóùåñòâóåòòàêîé åå êîíå÷íûé ïðåôèêñ β , ÷òî äëÿ ëþáîé òðàññû α0âûïîëíÿåòñÿ ñîîòíîøåíèåβα0 ∈/ P.Êëàññèôèêàöèÿ ñâîéñòâ âû÷èñëåíèéÑâîéñòâî áåçîïàñíîñòè: ¾íè÷åãî ïëîõîãî íèêîãäà íå ñëó÷èòñÿ¿.Ñâîéñòâî âû÷èñëåíèé P íàçûâàåòñÿ ñâîéñòâîì áåçîïàñíîñòè ,åñëè îíî óäîâëåòâîðÿåò ñëåäóþùåìó òðåáîâàíèþ:I êàêîâà áû íè áûëà òðàññà α, α ∈ (2AP )ω \ P , ñóùåñòâóåòòàêîé åå êîíå÷íûé ïðåôèêñ β , ÷òî äëÿ ëþáîé òðàññû α0âûïîëíÿåòñÿ ñîîòíîøåíèåβα0 ∈/ P.Ñîäåðæàòåëüíûé ñìûñë: ¾îòñóòñòâèå áåçîïàñíîñòè ýòî êîãäàåñëè ÷òî-òî ïëîõîå ñëó÷èëîñü, òî ýòîãî óæå íå èñïðàâèòü¿.Êëàññèôèêàöèÿ ñâîéñòâ âû÷èñëåíèéÏðèìåðû ñâîéñòâ áåçîïàñíîñòè: ñâåòîôîðå êðàñíûé ñâåò çàãîðàåòñÿ òîëüêîïîñëå æåëòîãî.Ïîêà ïðèíòåð íå çàâåðøèò ïå÷àòü, îí íåäîñòóïåí äëÿ äðóãèõ óñòðîéñòâ.Äâà ïðîöåññà íèêîãäà íå ìîãóò îáðàùàòüñÿîäíîâðåìåííî ê îäíîé è òîé æå îáëàñòèïàìÿòè.Ïðîòîêîë ðàçäâèæíîãî îêíà íèêîãäà íå òåðÿåòïåðâóþ ïîðöèþ äàííûõ ïðè ïåðåäà÷å.IIIIÊëàññèôèêàöèÿ ñâîéñòâ âû÷èñëåíèéÑâîéñòâî æèâîñòè: ¾÷òî-òî õîðîøåå îáÿçàòåëüíî ïðîèçîéäåò¿.Ñâîéñòâî âû÷èñëåíèé P íàçûâàåòñÿ ñâîéñòâîì æèâîñòè , åñëèîíî óäîâëåòâîðÿåò ñëåäóþùåìó òðåáîâàíèþ:I äëÿ ëþáîãî êîíå÷íîãî ñëîâà β, β ∈ (2AP )∗ , ñóùåñòâóåòòàêàÿ òðàññà α, α ∈ (2AP )ω , äëÿ êîòîðîé âûïîëíÿåòñÿñîîòíîøåíèåβα ∈ P.Êëàññèôèêàöèÿ ñâîéñòâ âû÷èñëåíèéÑâîéñòâî æèâîñòè: ¾÷òî-òî õîðîøåå îáÿçàòåëüíî ïðîèçîéäåò¿.Ñâîéñòâî âû÷èñëåíèé P íàçûâàåòñÿ ñâîéñòâîì æèâîñòè , åñëèîíî óäîâëåòâîðÿåò ñëåäóþùåìó òðåáîâàíèþ:I äëÿ ëþáîãî êîíå÷íîãî ñëîâà β, β ∈ (2AP )∗ , ñóùåñòâóåòòàêàÿ òðàññà α, α ∈ (2AP )ω , äëÿ êîòîðîé âûïîëíÿåòñÿñîîòíîøåíèåβα ∈ P.Ñîäåðæàòåëüíûé ñìûñë: ¾÷òî áû íè ñëó÷èëîñü âíà÷àëå, ïîòîìâñåãäà ìîæíî äîñòè÷ü ñâîåé öåëè¿.Êëàññèôèêàöèÿ ñâîéñòâ âû÷èñëåíèéÏðèìåðû ñâîéñòâ æèâîñòè: ñâåòîôîðå êîãäà-íèáóäü çàãîðèòñÿ çåëåíûéñâåò.Ïîñëå òîãî êàê ïðèíòåð çàâåðøàåò ïå÷àòü, îíñòèðàåò ñîäåðæèìîå ñâîåãî áóôåðà.Ïðîöåññ ìîæåò áåñêîíå÷íî ÷àñòî îáðàùàòüñÿê çàäàííîé îáëàñòè ïàìÿòè.Ïðîòîêîë ðàçäâèæíîãî îêíà îáÿçàòåëüíîäîñòàâëÿåò ïåðâóþ ïîðöèþ äàííûõ ïîíàçíà÷åíèþ.IIIIÊëàññèôèêàöèÿ ñâîéñòâ âû÷èñëåíèéÓòâåðæäåíèå 2.Åñëè ñâîéñòâî P ÿâëÿåòñÿ êàê ñâîéñòâîì æèâîñòè, òàê èñâîéñòâîì áåçîïàñíîñòè, òî P = (2AP )ω .Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî .Êëàññèôèêàöèÿ ñâîéñòâ âû÷èñëåíèéÓòâåðæäåíèå 2.Åñëè ñâîéñòâî P ÿâëÿåòñÿ êàê ñâîéñòâîì æèâîñòè, òàê èñâîéñòâîì áåçîïàñíîñòè, òî P = (2AP )ω .Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî .Óòâåðæäåíèå 3.Äëÿ ëþáîãî ñâîéñòâà P ñóùåñòâóþò òàêèå ñâîéñòâà æèâîñòèè áåçîïàñíîñòè Psafe , äëÿ êîòîðûõ âåðíî ðàâåíñòâîPliveP = Plive ∩ PsafeÄîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî [Òðóäíàÿ çàäà÷à! Áóäåò âûñîêî îöåíåíà!] .Êëàññèôèêàöèÿ ñâîéñòâ âû÷èñëåíèéÀ ê êàêîìó êëàññó îòíîñèòñÿ òàêîå ñâîéñòâîâû÷èñëåíèé:¾Ïîñëå òîãî, êàê âíà÷àëå ïðîöåññ îòêðîåò ôàéë,äàëåå îí ìîæåò áåñêîíå÷íî ÷àñòî ïðîâîäèòü èçíåãî ñ÷èòûâàíèå äàííûõ¿?Êëàññèôèêàöèÿ ñâîéñòâ âû÷èñëåíèéÀ ê êàêîìó êëàññó îòíîñèòñÿ òàêîå ñâîéñòâîâû÷èñëåíèé:¾Ïîñëå òîãî, êàê âíà÷àëå ïðîöåññ îòêðîåò ôàéë,äàëåå îí ìîæåò áåñêîíå÷íî ÷àñòî ïðîâîäèòü èçíåãî ñ÷èòûâàíèå äàííûõ¿?Îíî íå ÿâëÿåòñÿ íè ñâîéñòâîì áåçîïàñíîñòè, íèñâîéñòâîì æèâîñòè.Îãðàíè÷åíèÿ ñïðàâåäëèâîñòèÏðè ìîäåëèðîâàíèè âû÷èñëåíèé èíôîðìàöèîííûõ ñèñòåì,ñîñòîÿùèõ èç íåñêîëüêèõ ïàðàëëåëüíî ðàáîòàþùèõ ïðîöåññîâ,ïðèìåíÿåòñÿ ïðèíöèï ÷åðåäîâàíèÿ (interleaving assumption ):ïàðàëëåëüíàÿ êîìïîçèöèÿ âû÷èñëåíèécomp1 = a1 , a2 , a3 , .

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

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

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