Лекция 6. Символьный алгоритм верификации моделей для CTL (1185528), страница 2
Текст из файла (страница 2)
Òàêèì îáðàçîì, ∪i Pi = Pj , èâñëåäñòâèå ýòîãî ìû ïîëó÷àåì τ (∪i Pi ) = τ (Pj ) . Ñ äðóãîéñòîðîíû, â ñèëó ìîíîòîííîñòè τ ìû èìååìτ (P1 ) ⊆ τ (P2 ) ⊆ . . . Ïîýòîìó τ (Pj ) ⊆ τ (Pj ) äëÿ êàæäîãîj < j0 , è τ (Pj ) = τ (Pj ) äëÿ êàæäîãî j > j0 .  ðåçóëüòàòåïîëó÷àåì ñîîòíîøåíèå ∪i τ (Pi ) = τ (Pj ) , à ýòî îçíà÷àåò, ÷òîïðåîáðàçîâàòåëü τ ÿâëÿåòñÿ ∪ -íåïðåðûâíûì. Îáîñíîâàíèå ∩-íåïðåðûâíîñòè ïðåîáðàçîâàòåëÿ τ ïðîâîäèòñÿ àíàëîãè÷íî.0000000Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÇàïèñü τ i (Z ) áóäåò îáîçíà÷àòü i -êðàòíîå ïðèìåíåíèå τ ê Z .Áîëåå ñòðîãî τ i (Z ) îïðåäåëÿåòñÿ ðåêóðñèâíî ñîîòíîøåíèÿìèτ 0 (Z ) = Z è τ i+1 (Z ) = τ (τ i (Z )) .Ëåììà 2.
Åñëè τ ìîíîòîííûé ïðåîáðàçîâàòåëü, òî äëÿëþáîãî íàòóðàëüíîãî ÷èñëà i èìåþò ìåñòî âêëþ÷åíèÿτ i (False) ⊆ τ i+1 (False) è τ i (True) ⊇ τ i+1 (True).Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÇàïèñü τ i (Z ) áóäåò îáîçíà÷àòü i -êðàòíîå ïðèìåíåíèå τ ê Z .Áîëåå ñòðîãî τ i (Z ) îïðåäåëÿåòñÿ ðåêóðñèâíî ñîîòíîøåíèÿìèτ 0 (Z ) = Z è τ i+1 (Z ) = τ (τ i (Z )) .Ëåììà 2. Åñëè τ ìîíîòîííûé ïðåîáðàçîâàòåëü, òî äëÿëþáîãî íàòóðàëüíîãî ÷èñëà i èìåþò ìåñòî âêëþ÷åíèÿτ i (False) ⊆ τ i+1 (False) è τ i (True) ⊇ τ i+1 (True).Ëåììà 3. Åñëè τ ìîíîòîííûé ïðåîáðàçîâàòåëü, à S êîíå÷íîå ìíîæåñòâî, òî ñóùåñòâóþò òàêèå íàòóðàëüíûå ÷èñëài0 è j0 , ÷òî äëÿ ëþáîãî i > i0 âåðíî ðàâåíñòâîτ i (False) = τ i (False) , è äëÿ ëþáîãî j > j0 âåðíî ðàâåíñòâîτ j (True) = τ j (True) .00Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÇàïèñü τ i (Z ) áóäåò îáîçíà÷àòü i -êðàòíîå ïðèìåíåíèå τ ê Z .Áîëåå ñòðîãî τ i (Z ) îïðåäåëÿåòñÿ ðåêóðñèâíî ñîîòíîøåíèÿìèτ 0 (Z ) = Z è τ i+1 (Z ) = τ (τ i (Z )) .Ëåììà 2.
Åñëè τ ìîíîòîííûé ïðåîáðàçîâàòåëü, òî äëÿëþáîãî íàòóðàëüíîãî ÷èñëà i èìåþò ìåñòî âêëþ÷åíèÿτ i (False) ⊆ τ i+1 (False) è τ i (True) ⊇ τ i+1 (True).Ëåììà 3. Åñëè τ ìîíîòîííûé ïðåîáðàçîâàòåëü, à S êîíå÷íîå ìíîæåñòâî, òî ñóùåñòâóþò òàêèå íàòóðàëüíûå ÷èñëài0 è j0 , ÷òî äëÿ ëþáîãî i > i0 âåðíî ðàâåíñòâîτ i (False) = τ i (False) , è äëÿ ëþáîãî j > j0 âåðíî ðàâåíñòâîτ j (True) = τ j (True) .Ëåììà 4.
Åñëè τ ìîíîòîííûé ïðåîáðàçîâàòåëü, à S êîíå÷íîå ìíîæåñòâî, òî ñóùåñòâóþò òàêèå íàòóðàëüíûå ÷èñëài0 è j0 , ÷òîµZ . τ (Z ) = τ i (False) è νZ . τ (Z ) = τ j (True)0000Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÍà îñíîâàíèè ïðèâåäåííûõ ëåìì äëÿ âû÷èñëåíèÿ íàèìåíüøåéíåïîäâèæíîé òî÷êè ìîíîòîííîãî ïðåîáðàçîâàòåëÿ τ ìîæíîâîñïîëüçîâàòüñÿ ïðîãðàììîéfunctionLfp(Tau : PredicateTransformer ) : PredicateQ := False Q 0 := Tau(Q)0 dowhile Q 6= Q0Q := Q Q 0 := Tau(Q 0 )(;(Q )end whilereturnend function;);;;Ïðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÈíâàðèàíò öèêëàâ òåëå ïðîöåäóðû çàäàåòñÿ îòíîøåíèåì(Q 0 = τ (Q)) ∧ (Q 0 ⊆ µZ . τ (Z )) .Íåòðóäíî çàìåòèòü, ÷òî â íà÷àëå i -é èòåðàöèè öèêëàâûïîëíÿåòñÿ Q ⊆ τ i−1(False) è Q 0 ⊆ τ i (False) .whileÏðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÈíâàðèàíò öèêëàâ òåëå ïðîöåäóðû çàäàåòñÿ îòíîøåíèåì(Q 0 = τ (Q)) ∧ (Q 0 ⊆ µZ .
τ (Z )) .Íåòðóäíî çàìåòèòü, ÷òî â íà÷àëå i -é èòåðàöèè öèêëàâûïîëíÿåòñÿ Q ⊆ τ i−1(False) è Q 0 ⊆ τ i (False) .Èç ëåììû 4 âûòåêàåò False ⊆ τ (False) ⊆ τ 2(False) ⊆ . . .Ïîýòîìó ìàêñèìàëüíîå ÷èñëî èòåðàöèé îïåðàòîðà öèêëàîãðàíè÷åíî êîëè÷åñòâîì ýëåìåíòîâ â S . Ïðè âûõîäå èç öèêëà,Q = τ (Q) è Q ⊆ µZ . τ (Z ) . Òàê êàê Q ÿâëÿåòñÿ íåïîäâèæíîéòî÷êîé, µZ . τ (Z ) ⊆ Q , è ïîýòîìó Q = µZ .
τ (Z ) . Òåì ñàìûìïîêàçàíî, ÷òî çíà÷åíèå, êîòîðîå âîçâðàùàåò ïðîöåäóðà, ýòîäåéñòâèòåëüíî íàèìåíüøàÿ íåïîäâèæíàÿ òî÷êà.whileÏðåäñòàâëåíèÿ íåïîäâèæíîé òî÷êèÍàèáîëüøàÿ íåïîäâèæíàÿ òî÷êà âû÷èñëÿåòñÿ ïîäîáíûì æåîáðàçîì ïðè ïîìîùè äðóãîé ïðîãðàììû. Ïðèìåíÿÿ ïî ñóòèäåëà òó æå ñàìóþ àðãóìåíòàöèþ, ìîæíî ïîêàçàòü, ÷òî è ýòàïðîöåäóðà âñåãäà çàâåðøàåò ñâîè âû÷èñëåíèÿ è âîçâðàùàåò âêà÷åñòâå çíà÷åíèÿ νZ .
τ (Z ) .functionGfp(Tau : PredicateTransformer ) : PredicateQ := True Q 0 := Tau(Q)0 dowhile Q 6= Q0Q := Q Q 0 := Tau(Q 0 )(;(Q )end whilereturnend function;);;;Íåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûÅñëè ñîïîñòàâèòü êàæäîé ôîðìóëå f ïðåäèêàò {s | M, s |= f }íà ℘(S) , òî êàæäûé òåìïîðàëüíûé îïåðàòîð CTL ìîæíîîïèñàòü â òåðìèíàõ íàèìåíüøåé èëè íàèáîëüøåé íåïîäâèæíîéòî÷êè ïîäõîäÿùåãî ïðåîáðàçîâàòåëÿ ïðåäèêàòîâ. Ìû îáîñíóåìîïèñàíèÿ â òåðìèíàõ íåïîäâèæíûõ òî÷åê òîëüêî äëÿ è .If1 = νZ . f1 ∧Z,I[f1 f2 ] = µZ . f2 ∨ (f1 ∧Z) ,Èíòóèòèâíî ïîíÿòíî, ÷òî íàèìåíüøèå íåïîäâèæíûå òî÷êèñîîòâåòñòâóþò ñâîéñòâàì, êîòîðûå äîëæíû âûïîëíÿòüñÿêîãäà-íèáóäü, à íàèáîëüøèå íåïîäâèæíûå òî÷êè ñîîòâåòñòâóþòñâîéñòâàì, êîòîðûå äîëæíû âûïîëíÿòüñÿ âñåãäà. Ïîýòîìóf1 õàðàêòåðèçóåòñÿ ïðè ïîìîùè íàèìåíüøåé íåïîäâèæíîéòî÷êè, à f1 èìååò îïèñàíèå â òåðìèíàõ íàèáîëüøåéíåïîäâèæíîé òî÷êè.EGEGEEXUAFEGEXEUÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 5. Ïðåîáðàçîâàòåëü τ (Z ) = f1 ∧EXZìîíîòîííûé.Íåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 5.
Ïðåîáðàçîâàòåëü τ (Z ) = f1 ∧Äîê-âî. Ïðåäïîëîæèì, ÷òî P1 ⊆ P2 .EXZìîíîòîííûé.Íåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 5. Ïðåîáðàçîâàòåëü τ (Z ) = f1 ∧ Z ìîíîòîííûé.Äîê-âî. Ïðåäïîëîæèì, ÷òî P1 ⊆ P2 . ×òîáû ïðîâåðèòüâêëþ÷åíèå τ (P1) ⊆ τ (P2) , âîçüìåì ïðîèçâîëüíîå ñîñòîÿíèås ∈ τ (P1 ) .
Òîãäà s |= f1 è ñóùåñòâóåò òàêîå ñîñòîÿíèå s 0 , ÷òî(s, s 0 ) ∈ R è s 0 ∈ P1 .EXÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 5. Ïðåîáðàçîâàòåëü τ (Z ) = f1 ∧ Z ìîíîòîííûé.Äîê-âî. Ïðåäïîëîæèì, ÷òî P1 ⊆ P2 . ×òîáû ïðîâåðèòüâêëþ÷åíèå τ (P1) ⊆ τ (P2) , âîçüìåì ïðîèçâîëüíîå ñîñòîÿíèås ∈ τ (P1 ) .
Òîãäà s |= f1 è ñóùåñòâóåò òàêîå ñîñòîÿíèå s 0 , ÷òî(s, s 0 ) ∈ R è s 0 ∈ P1 . Íî ââèäó òîãî ÷òî P1 ⊆ P2 , âåðíî òàêæå èâêëþ÷åíèå s 0 ∈ P2 .EXÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 5. Ïðåîáðàçîâàòåëü τ (Z ) = f1 ∧ Z ìîíîòîííûé.Äîê-âî. Ïðåäïîëîæèì, ÷òî P1 ⊆ P2 . ×òîáû ïðîâåðèòüâêëþ÷åíèå τ (P1) ⊆ τ (P2) , âîçüìåì ïðîèçâîëüíîå ñîñòîÿíèås ∈ τ (P1 ) . Òîãäà s |= f1 è ñóùåñòâóåò òàêîå ñîñòîÿíèå s 0 , ÷òî(s, s 0 ) ∈ R è s 0 ∈ P1 . Íî ââèäó òîãî ÷òî P1 ⊆ P2 , âåðíî òàêæå èâêëþ÷åíèå s 0 ∈ P2 .
Çíà÷èò, s ∈ τ (P2) .EXÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 6. Ïóñòü τ (Z ) = f1 ∧ Z . Îáîçíà÷èì ÷åðåç τ i (True)ïðåäåë ïîñëåäîâàòåëüíîñòè True ⊇ τ (True) ⊇ . . . Òîãäà äëÿëþáîãî ñîñòîÿíèÿ s èç τ i (True) ìû èìååì s |= f1 è, êðîìåòîãî, íàéäåòñÿ òàêîå ñîñòîÿíèå s 0 , ÷òî (s, s 0) ∈ R ès 0 ∈ τ i (True) .EX000Íåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 6. Ïóñòü τ (Z ) = f1 ∧ Z . Îáîçíà÷èì ÷åðåç τ i (True)ïðåäåë ïîñëåäîâàòåëüíîñòè True ⊇ τ (True) ⊇ . . .
Òîãäà äëÿëþáîãî ñîñòîÿíèÿ s èç τ i (True) ìû èìååì s |= f1 è, êðîìåòîãî, íàéäåòñÿ òàêîå ñîñòîÿíèå s 0 , ÷òî (s, s 0) ∈ R ès 0 ∈ τ i (True) .Äîê-âî. Ïðåäïîëîæèì, ÷òî s ∈ τ i (True) . Ïîñêîëüêó ïðåäèêàòτ i (True) ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîé τ , èìååò ìåñòîðàâåíñòâî τ i (True) = τ (τ i (True)) .0EX000000Íåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 6. Ïóñòü τ (Z ) = f1 ∧ Z . Îáîçíà÷èì ÷åðåç τ i (True)ïðåäåë ïîñëåäîâàòåëüíîñòè True ⊇ τ (True) ⊇ .
. . Òîãäà äëÿëþáîãî ñîñòîÿíèÿ s èç τ i (True) ìû èìååì s |= f1 è, êðîìåòîãî, íàéäåòñÿ òàêîå ñîñòîÿíèå s 0 , ÷òî (s, s 0) ∈ R ès 0 ∈ τ i (True) .Äîê-âî. Ïðåäïîëîæèì, ÷òî s ∈ τ i (True) . Ïîñêîëüêó ïðåäèêàòτ i (True) ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîé τ , èìååò ìåñòîðàâåíñòâî τ i (True) = τ (τ i (True)) . Òàêèì îáðàçîì,s ∈ τ (τ i (True)) .0EX0000000Íåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 6. Ïóñòü τ (Z ) = f1 ∧ Z . Îáîçíà÷èì ÷åðåç τ i (True)ïðåäåë ïîñëåäîâàòåëüíîñòè True ⊇ τ (True) ⊇ . . . Òîãäà äëÿëþáîãî ñîñòîÿíèÿ s èç τ i (True) ìû èìååì s |= f1 è, êðîìåòîãî, íàéäåòñÿ òàêîå ñîñòîÿíèå s 0 , ÷òî (s, s 0) ∈ R ès 0 ∈ τ i (True) .Äîê-âî. Ïðåäïîëîæèì, ÷òî s ∈ τ i (True) .
Ïîñêîëüêó ïðåäèêàòτ i (True) ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîé τ , èìååò ìåñòîðàâåíñòâî τ i (True) = τ (τ i (True)) . Òàêèì îáðàçîì,s ∈ τ (τ i (True)) . Ïî îïðåäåëåíèþ ïðåîáðàçîâàòåëÿ τ ïîëó÷àåì,÷òî s |= f1 è, êðîìå òîãî, èìååòñÿ òàêîå ñîñòîÿíèå s 0 , ÷òî(s, s 0 ) ∈ R è s 0 ∈ τ i (True) .0EX00000000Íåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 7. Ïðåäèêàò f1 ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîéïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .EGEXÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 7. Ïðåäèêàò f1 ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîéïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .Äîê-âî.
Ïðåäïîëîæèì, ÷òî s0 |= f1 .EGEXEGÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 7. Ïðåäèêàò f1 ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîéïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .Äîê-âî. Ïðåäïîëîæèì, ÷òî s0 |= f1 . Òîãäà ïî îïðåäåëåíèþîòíîøåíèÿ âûïîëíèìîñòè |= ñóùåñòâóåò òàêîé ïóòü s0, s1, . . . âM , ÷òî äëÿ âñÿêîãî k èìååò ìåñòî ñîîòíîøåíèå sk |= f1 .EGEXEGÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 7. Ïðåäèêàò f1 ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîéïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .Äîê-âî.
Ïðåäïîëîæèì, ÷òî s0 |= f1 . Òîãäà ïî îïðåäåëåíèþîòíîøåíèÿ âûïîëíèìîñòè |= ñóùåñòâóåò òàêîé ïóòü s0, s1, . . . âM , ÷òî äëÿ âñÿêîãî k èìååò ìåñòî ñîîòíîøåíèå sk |= f1 .Îòñþäà ñëåäóåò, ÷òî s0 |= f1 è s1 |= f1 . Èíûìè ñëîâàìè,s0 |= f1 è s0 |=f1 .EGEXEGEGEX EGÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 7. Ïðåäèêàò f1 ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîéïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .Äîê-âî. Ïðåäïîëîæèì, ÷òî s0 |= f1 . Òîãäà ïî îïðåäåëåíèþîòíîøåíèÿ âûïîëíèìîñòè |= ñóùåñòâóåò òàêîé ïóòü s0, s1, . . . âM , ÷òî äëÿ âñÿêîãî k èìååò ìåñòî ñîîòíîøåíèå sk |= f1 .Îòñþäà ñëåäóåò, ÷òî s0 |= f1 è s1 |= f1 . Èíûìè ñëîâàìè,f1 ⊆ f1 ∧f1 .s0 |= f1 è s0 |=f1 .
ÏîýòîìóEGEXEGEGEX EGEGEX EGÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 7. Ïðåäèêàò f1 ÿâëÿåòñÿ íåïîäâèæíîé òî÷êîéïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .Äîê-âî. Ïðåäïîëîæèì, ÷òî s0 |= f1 . Òîãäà ïî îïðåäåëåíèþîòíîøåíèÿ âûïîëíèìîñòè |= ñóùåñòâóåò òàêîé ïóòü s0, s1, . . . âM , ÷òî äëÿ âñÿêîãî k èìååò ìåñòî ñîîòíîøåíèå sk |= f1 .Îòñþäà ñëåäóåò, ÷òî s0 |= f1 è s1 |= f1 . Èíûìè ñëîâàìè,f1 ⊆ f1 ∧f1 .s0 |= f1 è s0 |=f1 .
ÏîýòîìóÈ íàîáîðîò, åñëè s0 |= f1 ∧f1 , òî s0 |=f1 . Âðåçóëüòàòå ïîëó÷àåì f1 = f1 ∧f1 .EGEXEGEGEGEX EGEX EGEGEX EGEGEX EGÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 8. Ïðåäèêàò f1 ÿâëÿåòñÿ íàèáîëüøåé íåïîäâèæíîéòî÷êîé ïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .EGEXÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 8. Ïðåäèêàò f1 ÿâëÿåòñÿ íàèáîëüøåé íåïîäâèæíîéòî÷êîé ïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .Ëåììà 9. Ïðåäèêàò [f1 f2] ÿâëÿåòñÿ íàèìåíüøåéíåïîäâèæíîé òî÷êîé ïðåîáðàçîâàòåëÿ τ (Z ) = f2 ∨ (f1 ∧ Z ) .EGEXEUEXÍåïîäâèæíûå òî÷êè è òåìïîðàëüíûåîïåðàòîðûËåììà 8.
Ïðåäèêàò f1 ÿâëÿåòñÿ íàèáîëüøåé íåïîäâèæíîéòî÷êîé ïðåîáðàçîâàòåëÿ τ (Z ) = f1 ∧ Z .Ëåììà 9. Ïðåäèêàò [f1 f2] ÿâëÿåòñÿ íàèìåíüøåéíåïîäâèæíîé òî÷êîé ïðåîáðàçîâàòåëÿ τ (Z ) = f2 ∨ (f1 ∧ Z ) .Äîê-âî.EGEXEUEXÑàìîñòîÿòåëüíî. j jY66Y66 pps0qps0pτ 1 (False)q[p U q] = µZ . q ∨ (p ∧ EX Z )E j jY6Y666 3 s0ppτ 2 (False)qps0pτ (False)qÑèìâîëüíàÿ âåðèôèêàöèÿ ìîäåëåé äëÿ CTLÒàáëè÷íûé àãîðèòì âåðèôèêàöèè ìîäåëåé äëÿ CTL ñ ÿâíûìïðåäñòàâëåíèåì ìîäåëè èìååò ëèíåéíóþ ñëîæíîñòü êàê ïîðàçìåðó ìîäåëè, òàê è ïî äëèíå ôîðìóëû.Îäíàêî ðàçìåð ìîäåëè ïàðàëëåëüíîé ñèñòåìû, ñîñòîÿùåé èçìíîãèõ ïðîöåññîâ èëè êîìïîíåíòîâ, âîçðàñòàåòýêñïîíåíöèàëüíî ñ óâåëè÷åíèåì ÷èñëà ïðîöåññîâ.Ñèìâîëüíûå àëãîðèòìû âåðèôèêàöèè ìîäåëåé äëÿ CTLïîçâîëÿþò ïðåîäîëåò òðóäíîñòè().
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
