Лекция 4. Логика вычисления программ. CTL. LTL (1185526), страница 2
Текст из файла (страница 2)
. .comp2 = b1 , b2 , b3 , . . .ïðåäñòàâëÿåòñÿ ìíîæåñòâîìïîñëåäîâàòåëüíîñòåé comp1 è comp2 ïåðåìåøèâàíèé,ñîõðàíÿþùèõ îòíîñèòåëüíûé ïîðÿäîê ñëåäîâàíèÿ ÷ëåíîâ îäíîéè òîé æå ïîñëåäîâàòåëüíîñòè.Ïðèìåð ÷åðåäîâàíèÿ: a1, b1, b2, a2, b3, a3, a4, . . . .÷åðåäîâàíèéÎãðàíè÷åíèÿ ñïðàâåäëèâîñòèÎäíàêî ïðè ïîñòðîåíèè ïàðàëëåëüíîé êîìïîçèöèè ìîäåëåéïðîöåññîâ ïðèíöèï ÷åðåäîâàíèÿ ñîáëþäàåòñÿ íå â ïîëíîé ìåðå.Ðàññìîòðèì ïàðó ìîäåëåé Êðèïêå äëÿ ïðîöåññîâ P1 è P2.P1 s1 a1a2- s2b1P2 r1 b2- r2Îãðàíè÷åíèÿ ñïðàâåäëèâîñòèÎäíàêî ïðè ïîñòðîåíèè ïàðàëëåëüíîé êîìïîçèöèè ìîäåëåéïðîöåññîâ ïðèíöèï ÷åðåäîâàíèÿ ñîáëþäàåòñÿ íå â ïîëíîé ìåðå.Ðàññìîòðèì ïàðó ìîäåëåé Êðèïêå äëÿ ïðîöåññîâ P1 è P2.P1 s1 a1a2- s2kb1P2 r1 b2- r2Ïàðàëëåëüíàÿ àñèíõðîííàÿ êîìïîçèöèÿ ýòèõ ïðîöåññîâ íåìîæåò èìåòü âû÷èñëåíèÿcomp(P1 k P2 ) = a1 , a2 , a1 , a2 , .
. . è.ò.ä.ïîñêîëüêó îíî íå ÿâëÿåòñÿ ðåçóëüòàòîì ÷åðåäîâàíèÿêàêèõ-ëèáî äâóõ âû÷èñëåíèé ýòèõ ïðîöåññîâ.Îãðàíè÷åíèÿ ñïðàâåäëèâîñòèÍî åñëè ïîñòðîèòü ìîäåëü Êðèïêå äëÿ ïàðàëëåëüíîéàñèíõðîííîé êîìïîçèöèè P1 k P2,(s1 , r1 )a1 @ b1@I@ @a2b2 @R@ (s2 , r1 )(s1 , r2 )a1 @b1I@@ @a2b2 @R@(s2 , r2 )òî â ýòîé ìîäåëè èìååòñÿ ïóòüπ = a1 , a2 , a1 , a2 , . . . è.ò.ä.Çíà÷èò, íóæíî ñðåäñòâî, ïîçâîëÿþùåå óñòðàíèòüíåäîïóñòèìûå (¾íå÷åñòíûå¿) ïóòè â ìîäåëÿõ Êðèïêå.Îãðàíè÷åíèÿ ñïðàâåäëèâîñòèÎãðàíè÷åíèÿ ñïðàâåäëèâîñòè ýòî óñëîâèÿ,êîòîðûì äîëæíû óäîâëåòâîðÿòü ïóòè â ìîäåëÿõÊðèïêå, ÷òîáû ýòè ïóòè ñîîòâåòñòâîâàëèâû÷èñëåíèÿì, ïîñòðîåííûì ïî ïðèíöèïó÷åðåäîâàíèÿ.Êàæäîå îãðàíè÷åíèå ñïðàâåäëèâîñòè îòíîñèòñÿ êíåêîòîðîìó äåéñòâèþ (ïåðåõîäó) â ìîäåëè èòðåáóåò îáÿçàòåëüíîãî âûïîëíåíèÿ ýòîãî äåéñòâèÿâ âû÷èñëåíèè ìîäåëè â çàâèñèìîñòè îò òîãî,íàñêîëüêî ÷àñòî âûïîëíÿþòñÿ óñëîâèÿ äëÿñîâåðøåíèÿ ýòîãî äåéñòâèÿ.Îãðàíè÷åíèÿ ñïðàâåäëèâîñòèÐàçëè÷àþò äâà òèïà îãðàíè÷åíèé ñïðàâåäëèâîñòè.I Ñëàáàÿ ñïðàâåäëèâîñòü : åñëè ïóòüïðîõîäèò÷åðåç ñîñòîÿíèÿ, â êîòîðûõ ìîæåò áûòü âûïîëíåíîäåéñòâèå act , òî äåéñòâèå act äîëæíî áûòü âûïîëíåíî.I Ñèëüíàÿ ñïðàâåäëèâîñòü : åñëè ïóòüïðîõîäèò ÷åðåç ñîñòîÿíèÿ, â êîòîðûõ ìîæåò áûòüâûïîëíåíî äåéñòâèå act , òî äåéñòâèå act äîëæíî áûòüâûïîëíåíî.ïî÷òè âñåãäàáåñêîíå÷íî ÷àñòîáåñêîíå÷íî ÷àñòîáåñêîíå÷íî ÷àñòîÎãðàíè÷åíèÿ ñïðàâåäëèâîñòèÒàêèì îáðàçîì, â ìîäåëè Êðèïêå äëÿ ïàðàëëåëüíîéàñèíõðîííîé êîìïîçèöèè P1 k P2(s1 , r1 )a1 @ b1@I@ @a2b2 @R@ (s2 , r1 )(s1 , r2 )a1 @b1I@@ @a2b2 @R@(s2 , r2 )ïóòüπ = a1 , a2 , a1 , a2 , .
. . è.ò.ä.íå óäîâëåòâîðÿåò îãðàíè÷åíèþ ñëàáîé ñïðàâåäëèâîñòèîòíîñèòåëüíî äåéñòâèÿ b1 , è ïîýòîìó íå ìîäåëèðóåò íèêàêîåâû÷èñëåíèå.Îãðàíè÷åíèÿ ñïðàâåäëèâîñòèÑïðàâåäëèâàÿ ìîäåëü Êðèïêå ýòî ñèñòåìà ðàçìå÷åííûõïåðåõîäîâ M = (S, S0, R, L, Act) ñ îãðàíè÷åíèÿìèñïðàâåäëèâîñòè Fair = (WeakFair , StrongFair ) , ãäåI Act ìíîæåñòâî äåéñòâèéI R îòíîøåíèå ïåðåõîäîâ, R ⊆ S × Act × SI WeakFair ìíîæåñòâî äåéñòâèé, ïîäïàäàþùèõ ïîäîãðàíè÷åíèå ñëàáîé ñïðàâåäëèâîñòè, WeakFair ⊆ Act ;I StrongFair ìíîæåñòâî äåéñòâèé, ïîäïàäàþùèõ ïîäîãðàíè÷åíèå ñëàáîé ñïðàâåäëèâîñòè, StrongFair ⊆ Act .Îãðàíè÷åíèÿ ñïðàâåäëèâîñòèÑïðàâåäëèâàÿ ìîäåëü Êðèïêå ýòî ñèñòåìà ðàçìå÷åííûõïåðåõîäîâ M = (S, S0, R, L, Act) ñ îãðàíè÷åíèÿìèñïðàâåäëèâîñòè Fair = (WeakFair , StrongFair ) , ãäåI Act ìíîæåñòâî äåéñòâèéI R îòíîøåíèå ïåðåõîäîâ, R ⊆ S × Act × SI WeakFair ìíîæåñòâî äåéñòâèé, ïîäïàäàþùèõ ïîäîãðàíè÷åíèå ñëàáîé ñïðàâåäëèâîñòè, WeakFair ⊆ Act ;I StrongFair ìíîæåñòâî äåéñòâèé, ïîäïàäàþùèõ ïîäîãðàíè÷åíèå ñëàáîé ñïðàâåäëèâîñòè, StrongFair ⊆ Act .Îáîçíà÷èì çàïèñüþ Tr (M, Fair ) ìíîæåñòâî òðàññ âñåõ òåõèíèöèàëüíûõ ïóòåé â ìîäåëè M , êîòîðûå óäîâëåòâîðÿþòîãðàíè÷åíèÿì ñïðàâåäëèâîñòè Fair .Òîãäà çàäà÷à âåðèôèêàöèè ìîäåëåé ïðîãðàìì ñîñòîèò âïðîâåðêå ñîîòíîøåíèé âèäàTr (M, Fair ) ⊆ P,êîòîðûå òàêæå îáîçíà÷àþòñÿ çàïèñüþ M, Fair |= P .Òåìïîðàëüíûå ëîãèêèÒåìïîðàëüíûå ëîãèêè ïðåäíàçíà÷åíû äëÿ îïèñàíèÿ ñâîéñòââû÷èñëåíèé ðåàãèðóþùèõ ñèñòåì, ò.å.
ìíîæåñòâ òðàññ âðàçìå÷åííûõ ñèñòåìàõ ïåðåõîäîâ (ìîäåëÿõ Êðèïêå). òåìïîðàëüíûõ ëîãèêàõ âðåìÿ ÿâíî íå óïîìèíàåòñÿ; âìåñòîýòîãî ôîðìóëû ïîçâîëÿþò, íàïðèìåð, çàïèñûâàòü óòâåðæäåíèÿî òîì, ÷òî íåêîòîðîå âûäåëåííîå ñîñòîÿíèå áóäåò êîãäà-íèáóäüïðîéäåíî èëè ÷òî ñîñòîÿíèå îøèáêè íèêîãäà íå áóäåòäîñòèãíóòî.Äëÿ ýòîãî èñïîëüçóþòñÿ ñïåöèàëüíûå òåìïîðàëüíûå îïåðàòîðû. Òåìïîðàëüíûå ëîãèêè îòëè÷àþòñÿ íàáîðîì èñïîëüçóåìûõòåìïîðàëüíûõ îïåðàòîðîâ è ñåìàíòèêîé ýòèõ îïåðàòîðîâ. öåíòðå íàøåãî âíèìàíèÿ áóäåò î÷åíü âûðàçèòåëüíàÿ ëîãèêàïîä íàçâàíèåì CTL∗.Ëîãèêà äåðåâüåâ âû÷èñëåíèé CTL∗Ôîðìóëû CTL∗ îïèñûâàþò ñâîéñòâà äåðåâüåâ âû÷èñëåíèé .Òàêîå äåðåâî îáðàçóåòñÿ çà ñ÷åò âûäåëåíèÿ íåêîòîðîãîñîñòîÿíèÿ â ìîäåëè Êðèïêå â êà÷åñòâå íà÷àëüíîãî ñîñòîÿíèÿ èïîñëåäóþùåé ðàçâåðòêè ìîäåëè â áåñêîíå÷íîå äåðåâî ñ êîðíåìâ âûäåëåííîìñîñòîÿíèè.-ababbcAAU6cÃðàô ïåðåõîäîâ,èëè ìîäåëü ÊðèïêåAAAAAAAAUbcc AAAAAAAAAUUAab AAUñ?c?Áåñêîíå÷íîå äåðåâî, ðàçâåðíóòîå èç ãðàôà ïåðåõîäîâËîãèêà äåðåâüåâ âû÷èñëåíèé CTL∗Ôîðìóëû CTL∗ ñòðîÿòñÿ èç êâàíòîðîâ ïóòè è òåìïîðàëüíûõîïåðàòîðîâ .Êâàíòîðû ïóòè (¾äëÿ âñåõ ïóòåé âû÷èñëåíèÿ¿) è (¾äëÿíåêîòîðîãî ïóòè âû÷èñëåíèÿ¿) ïðèìåíÿþòñÿ äëÿ îïèñàíèÿñòðóêòóðû âåòâëåíèÿ â äåðåâå âû÷èñëåíèé.
Ýòè êâàíòîðûèñïîëüçóþòñÿ â òîì èëè èíîì ñîñòîÿíèè äëÿ óêàçàíèÿ òîãî,÷òî âñå ïóòè èëè íåêîòîðûå èç ïóòåé, èñõîäÿùèõ èç äàííîãîñîñòîÿíèÿ, îáëàäàþò ïðåäïèñàííûì ñâîéñòâîì.Òåìïîðàëüíûå îïåðàòîðû îïèñûâàþò ñâîéñòâà ïóòè,ïðîõîäÿùåãî â äåðåâå.AEËîãèêà äåðåâüåâ âû÷èñëåíèé CTL∗Èìåþòñÿ òðè îäíîìåñòíûõ îïåðàòîðà.I Îïåðàòîð ñäâèãà ïî âðåìåíè(neXttime, ¾â ñëåäóþùèéìîìåíò¿): P îçíà÷àåò, ÷òî ñâîéñòâî P äîëæíîñîáëþäàòüñÿ â ñëåäóþùåì ñîñòîÿíèè ïóòè.I Îïåðàòîð ïðîèñøåñòâèÿ(Future, ¾ðàíî èëè ïîçäíî¿,¾êîãäà-òî â áóäóùåì¿): P îçíà÷àåò, ÷òî ñâîéñòâî P áóäåòñîáëþäàòüñÿ â êàêîì-òî ïîñëåäóþùåì ñîñòîÿíèè ïóòè.I Îïåðàòîð èíâàðèàíòíîñòè(Globally, ¾âñåãäà¿,¾ïîâñþäó¿): P îçíà÷àåò, ÷òî ñâîéñòâî P äîëæíîñîáëþäàåòñÿ â êàæäîì ñîñòîÿíèè ïóòè.XXFFGGËîãèêà äåðåâüåâ âû÷èñëåíèé CTL∗Èìåþòñÿ äâà äâóõìåñòíûõ îïåðàòîðîâ.I Îïåðàòîð óñëîâíîãî îæèäàíèÿ(Until, ¾äî òåõ ïîðïîêà¿): P1 P2 îçíà÷àåò, ÷òî íà ïóòè èìååòñÿ ñîñòîÿíèå, âêîòîðîì ñîáëþäàåòñÿ âòîðîå ñâîéñòâî P2 , è ïðè ýòîìêàæäîå ïðåäøåñòâóþùåå íà ýòîì ïóòè ñîñòîÿíèå îáëàäàåòïåðâûì ñâîéñòâîì P1 .I Îïåðàòîð ðàçáëîêèðîâêè(Release, ¾âûñâîáîäèòü¿):P1 P2 îçíà÷àåò, ÷òî âòîðîå ñâîéñòâî P2 äîëæíîâûïîëíÿòüñÿ íà ïóòè âïëîòü äî òàêîãî ñîñòîÿíèÿ, âêîòîðîì ñîáëþäàåòñÿ ïåðâîå ñâîéñòâî P1 .
Îäíàêî ïåðâîåñâîéñòâî P1 íå îáÿçàòåëüíî äîëæíî êîãäà-íèáóäü áûòüâûïîëíåíî.UURRËîãèêà äåðåâüåâ âû÷èñëåíèé CTL∗ CTL∗ èìåþòñÿ ôîðìóëû äâóõ òèïîâ: ôîðìóëû ñîñòîÿíèÿ(ñïîñîáíûå îáðàùàòüñÿ â èñòèíó â íåêîòîðîì ñîñòîÿíèè) èôîðìóëû ïóòè (ñïîñîáíûå áûòü èñòèííûìè íà ïðîòÿæåíèèíåêîòîðîãî ïóòè).Ëîãèêà äåðåâüåâ âû÷èñëåíèé CTL∗ CTL∗ èìåþòñÿ ôîðìóëû äâóõ òèïîâ: ôîðìóëû ñîñòîÿíèÿ(ñïîñîáíûå îáðàùàòüñÿ â èñòèíó â íåêîòîðîì ñîñòîÿíèè) èôîðìóëû ïóòè (ñïîñîáíûå áûòü èñòèííûìè íà ïðîòÿæåíèèíåêîòîðîãî ïóòè).Ôîðìóëû ñîñòîÿíèÿ îïðåäåëÿþòñÿ ñëåäóþùèìè ïðàâèëàìè:I Åñëè p ∈ AP , òî p ôîðìóëà ñîñòîÿíèÿ.I Åñëè f1 è f2 ôîðìóëû ñîñòîÿíèÿ, òî ¬f1 , f1 ∧ f2 è f1 ∨ f2 ôîðìóëû ñîñòîÿíèÿ.I Åñëè f ôîðìóëà ïóòè, òîf è f ôîðìóëûñîñòîÿíèÿ.EAËîãèêà äåðåâüåâ âû÷èñëåíèé CTL∗ CTL∗ èìåþòñÿ ôîðìóëû äâóõ òèïîâ: ôîðìóëû ñîñòîÿíèÿ(ñïîñîáíûå îáðàùàòüñÿ â èñòèíó â íåêîòîðîì ñîñòîÿíèè) èôîðìóëû ïóòè (ñïîñîáíûå áûòü èñòèííûìè íà ïðîòÿæåíèèíåêîòîðîãî ïóòè).Ôîðìóëû ñîñòîÿíèÿ îïðåäåëÿþòñÿ ñëåäóþùèìè ïðàâèëàìè:I Åñëè p ∈ AP , òî p ôîðìóëà ñîñòîÿíèÿ.I Åñëè f1 è f2 ôîðìóëû ñîñòîÿíèÿ, òî ¬f1 , f1 ∧ f2 è f1 ∨ f2 ôîðìóëû ñîñòîÿíèÿ.I Åñëè f ôîðìóëà ïóòè, òîf è f ôîðìóëûñîñòîÿíèÿ.Ôîðìóëû ïóòè îïðåäåëÿþòñÿ ñëåäóþùèìè ïðàâèëàìè:I Åñëè f ôîðìóëà ñîñòîÿíèÿ, òî f ôîðìóëà ïóòè.I Åñëè g1 è g2 ôîðìóëû ïóòè, òî ¬g1 , g1 ∧ g2 , g1 ∨ g2 ,g1 , g1 , g1 , g1 g2 , g1 g2 ôîðìóëû ïóòè.EXFGURAËîãèêà äåðåâüåâ âû÷èñëåíèé CTL∗ CTL∗ èìåþòñÿ ôîðìóëû äâóõ òèïîâ: ôîðìóëû ñîñòîÿíèÿ(ñïîñîáíûå îáðàùàòüñÿ â èñòèíó â íåêîòîðîì ñîñòîÿíèè) èôîðìóëû ïóòè (ñïîñîáíûå áûòü èñòèííûìè íà ïðîòÿæåíèèíåêîòîðîãî ïóòè).Ôîðìóëû ñîñòîÿíèÿ îïðåäåëÿþòñÿ ñëåäóþùèìè ïðàâèëàìè:I Åñëè p ∈ AP , òî p ôîðìóëà ñîñòîÿíèÿ.I Åñëè f1 è f2 ôîðìóëû ñîñòîÿíèÿ, òî ¬f1 , f1 ∧ f2 è f1 ∨ f2 ôîðìóëû ñîñòîÿíèÿ.I Åñëè f ôîðìóëà ïóòè, òîf è f ôîðìóëûñîñòîÿíèÿ.Ôîðìóëû ïóòè îïðåäåëÿþòñÿ ñëåäóþùèìè ïðàâèëàìè:I Åñëè f ôîðìóëà ñîñòîÿíèÿ, òî f ôîðìóëà ïóòè.I Åñëè g1 è g2 ôîðìóëû ïóòè, òî ¬g1 , g1 ∧ g2 , g1 ∨ g2 ,g1 , g1 , g1 , g1 g2 , g1 g2 ôîðìóëû ïóòè.Ôîðìóëàìè CTL∗ ÿâëÿþòñÿ âñå ôîðìóëû ñîñòîÿíèé,ïîñòðîåííûå ñîãëàñíî óêàçàííûì ïðàâèëàì.EXFGURAËîãèêà äåðåâüåâ âû÷èñëåíèé CTL∗Ñåìàíòèêà CTL∗ îïðåäåëåòñÿ íà ìîäåëÿõ ÊðèïêåM = (S, S0 , R, L) .
Ïóòåì â M íàçîâåì âñÿêóþ òàêóþáåñêîíå÷íóþ ïîñëåäîâàòåëüíîñòü ñîñòîÿíèé π = s0, s1, . . . , ÷òî(si , si+1 ) ∈ R äëÿ êàæäîãî i ≥ 0 . Ïóòü ìîæíî ïîíèìàòü êàêáåñêîíå÷íóþ âåòâü â äåðåâå âû÷èñëåíèé, ñîîòâåòñòâóþùåììîäåëè M .Ìû áóäåì èñïîëüçîâàòü çàïèñü πi äëÿ îáîçíà÷åíèÿ ñóôôèêñàπ , íà÷èíàþùåãîñÿ ñîñòîÿíèåì si .Åñëè f ôîðìóëà ñîñòîÿíèÿ, òî çàïèñü M, s |= f îçíà÷àåò,÷òî f âûïîëíÿåòñÿ â ñîñòîÿíèè s íà ìîäåëè Êðèïêå M .
Òî÷íîòàê æå, åñëè g ôîðìóëà ïóòè, òî çàïèñü M, π |= g îçíà÷àåò,÷òî g âûïîëíÿåòñÿ íà ïðîòÿæåíèè ïóòè π â ìîäåëè M .Ëîãèêà äåðåâüåâ âû÷èñëåíèé CTL∗Ñåìàíòèêà ôîðìóë ñîñòîÿíèÿ1).2).3).4).5).M, s |= p ⇔ p ∈ L(s);M, s |= ¬f1 ⇔ M, s 6|= f1;èëè M, s |= f2 ;M, s |= f1 ∧ f2 ⇔ M, s |= f1 è M, s |= f2 ;M, s |= f ⇔ â M åñòü òàêîé ïóòü èç ñîñòîÿíèÿ s , ÷òîM, π |= f ;6). M, s |= f ⇔ äëÿ ëþáîãî ïóòè π èç ñîñòîÿíèÿ s â ìîäåëèM âåðíî ñîîòíîøåíèå M, π |= f ;M, s |= f1 ∨ f2 ⇔ M, s |= f1EAËîãèêà äåðåâüåâ âû÷èñëåíèé CTL∗Ñåìàíòèêà ôîðìóë ïóòè7).8).9).10).11).12).13).14).15).äëÿ ïåðâîãî ñîñòîÿíèÿ s íà ïóòè π â ìîäåëèâåðíî ñîîòíîøåíèå M, s |= g1 ;M, π |= ¬g1 ⇔ M, π 6|= g1 ;M, π |= g1 ∨ g2 ⇔ M, π |= g1 èëè M, π |= g2 ;M, π |= g1 ∧ g2 ⇔ M, π |= g1 è M, π |= g2 ;M, π |= g1 ⇔ M, π 1 |= g1 ;M, π |= g1 ⇔ ñóùåñòâóåò òàêîå k > 0 , ÷òî M, π k |= g1 ;M, π |= g1 ⇔ äëÿ ëþáîãî k > 0 âåðíî ñîîòíîøåíèåM, π k |= g1 ;M, π |= g1 g2 ⇔ ñóùåñòâóåò òàêîå k > 0 , ÷òî M, π k |= g2è äëÿ êàæäîãî 0 6 j < k âåðíî ñîîòíîøåíèå M, πj |= g1 ;M, π |= g1 g2 ⇔ êàêîâî áû íè áûëî j > 0 , åñëè äëÿêàæäîãî i < j âåðíî ñîîòíîøåíèå M, πi 6|= g1 , òîM, π j |= g2 .M, π |= g1 ⇔MXFGURËîãèêà äåðåâüåâ âû÷èñëåíèé CTL∗Ëåãêî óáåäèòüñÿ â òîì, ÷òî îïåðàòîðîâ ∨ , ¬ , , ,äîñòàòî÷íî äëÿ òîãî, ÷òîáû ñ èõ ïîìîùüþ âûðàçèòü ëþáóþôîðìóëó CTL∗:I f ∧ g ≡ ¬(¬f ∨ ¬g ) ,I fg ≡ ¬(¬f ¬g ) ,If ≡ Truef ,If ≡ ¬ ¬f ,I(f ) ≡ ¬ (¬f ) .XRUFGAUFEUECTL è LTL×àùå âñåãî èñïîëüçóþò äâà ïîëåçíûõ ïîäìíîæåñòâà CTL∗:îäíà èç ýòèõ ëîãèê íàçûâàåòñÿ ëîãèêîé âåòâÿùåãîñÿ âðåìåíè ,à äðóãàÿ ëîãèêîé ëèíåéíîãî âðåìåíè .
Ðàçëè÷èå ìåæäó íèìèïðîÿâëÿåòñÿ â òîì, êàê îíè îòíîñÿòñÿ ê âåòâëåíèþ âóïîìÿíóòîì äåðåâå âû÷èñëåíèé.  ëîãèêå âåòâÿùåãîñÿ âðåìåíèòåìïîðàëüíûå îïåðàòîðû íàõîäÿòñÿ íåïîñðåäñòâåííî ïîääåéñòâèåì êâàíòîðîâ ïî òåì ïóòÿì, êîòîðûå èñõîäÿò èççàäàííîãî ñîñòîÿíèÿ.  ëîãèêå ëèíåéíîãî âðåìåíè îïåðàòîðûïðåäíàçíà÷åíû äëÿ îïèñàíèÿ ñîáûòèé íà ïðîòÿæåíèèåäèíñòâåííîãî ïóòè âû÷èñëåíèÿ.CTL è LTLËîãèêà äåðåâüåâ âû÷èñëåíèé (CTL) ïðåäñòàâëÿåò ñîáîéôðàãìåíò CTL∗, â êîòîðîì êàæäûé òåìïîðàëüíûé îïåðàòîð ,, , è äîëæåí ñëåäîâàòü íåïîñðåäñòâåííî çà êâàíòîðîìïóòè. Ãîâîðÿ áîëåå ñòðîãî, CTL ýòî ïîäìíîæåñòâî CTL∗, âêîòîðîì ñòðóêòóðà ôîðìóë ïóòè îãðàíè÷åíà ñëåäóþùèìïðàâèëîì.I Åñëè f è g ôîðìóëû ñîñòîÿíèÿ, òîf , f , f ,f g,è f g ôîðìóëû ïóòè.Òàêèì îáðàçîì, â ôîðìóëàõ CTL êàæäûé òåìïîðàëüíûéîïåðàòîð íåïîñðåäñòâåííî ñëåäóåò çà êâàíòîðîì ïóòè.XFGURXRÏðèìåðû.AGEFp1 → (p2EUp ∨ A G(p ∧ q)(A F p3 )).,FGUCTL è LTLËèíåéíàÿ òåìïîðàëüíàÿ ëîãèêà (LTL), â ñâîþ î÷åðåäü, ñîñòîèòèç âñåõ ôîðìóë âèäà f , ãäå f ôîðìóëà ïóòè, â êîòîðîé âñåôîðìóëû ñîñòîÿíèÿ ýòî àòîìàðíûå âûñêàçûâàíèÿ.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
