Свойства предикатного трансформера системы VRS
Розглянуто моделі, записані в мові базових протоколів. Вони є атрибутними транзиційними системами, а їх стани задаються формулами багатосортного числення предикатів першого порядку над атрибутами системи. Допускаються атрибути простих числових символьних типів, функціональних типів, а також черги. В...
Збережено в:
| Опубліковано в: : | Кибернетика и системный анализ |
|---|---|
| Дата: | 2010 |
| Автори: | , , , , |
| Формат: | Стаття |
| Мова: | Російська |
| Опубліковано: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2010
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/45239 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Свойства предикатного трансформера системы VRS / А.А. Летичевский, А.Б. Годлевский, А.А. Летичевский (мл.), С.В. Потиенко, В.С. Песчаненко // Кибернетика и системный анализ. — 2010. — № 4. — С. 3-16. — Бібліогр.: 19 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859634754026995712 |
|---|---|
| author | Летичевский, А.А. Годлевский, А.Б. Летичевский, А.А. (мл.) Потиенко, С.В. Песчаненко, В.С. |
| author_facet | Летичевский, А.А. Годлевский, А.Б. Летичевский, А.А. (мл.) Потиенко, С.В. Песчаненко, В.С. |
| citation_txt | Свойства предикатного трансформера системы VRS / А.А. Летичевский, А.Б. Годлевский, А.А. Летичевский (мл.), С.В. Потиенко, В.С. Песчаненко // Кибернетика и системный анализ. — 2010. — № 4. — С. 3-16. — Бібліогр.: 19 назв. — рос. |
| collection | DSpace DC |
| container_title | Кибернетика и системный анализ |
| description | Розглянуто моделі, записані в мові базових протоколів. Вони є атрибутними транзиційними системами, а їх стани задаються формулами багатосортного числення предикатів першого порядку над атрибутами системи. Допускаються атрибути простих числових символьних типів, функціональних типів, а також черги. В постумовах базових протоколів використовуються оператори присвоювання, оновлення черг та довільні формули. Для здійснення переходу із одного стану в інший побудовано предикатний трансформер як функцію перетворення формул. Доведено основну властивість предикатного трансформера, згідно якій він обчислює найсильнішу постумову для символьних станів.
The paper considers models specified in basic protocol language. They are attribute transition systems and their states are defined by formulas of first-order multisort predicate calculus over system attributes. Attributes of simple numeric and symbolic types, functional types, and queues are allowed. Assignment operators, queue update operators, and arbitrary formulas are used in postconditions of basic protocols. To pass from one state to another, a predicate transformer has been set up as a function of formula transformation. The main property of the predicate transformer has been proved: it calculates the strongest postcondition for symbolic states.
|
| first_indexed | 2025-12-07T13:14:25Z |
| format | Article |
| fulltext |
À.À. ËÅÒÈ×ÅÂÑÊÈÉ, À.Á. ÃÎÄËÅÂÑÊÈÉ, À.À. ËÅÒÈ×ÅÂÑÊÈÉ (ìë.),
Ñ.Â. ÏÎÒÈÅÍÊÎ, Â.Ñ. ÏÅÑ×ÀÍÅÍÊÎ
ÓÄÊ 519.686.2 ÑÂÎÉÑÒÂÀ ÏÐÅÄÈÊÀÒÍÎÃÎ
ÒÐÀÍÑÔÎÐÌÅÐÀ ÑÈÑÒÅÌÛ VRS
Êëþ÷åâûå ñëîâà: âåðèôèêàöèÿ, ñèìâîëüíîå ìîäåëèðîâàíèå, àáñòðàêöèè.
ÂÂÅÄÅÍÈÅ
Ñèñòåìà VRS [1–5] ïðåäíàçíà÷åíà äëÿ âåðèôèêàöèè òðåáîâàíèé ê ïðîãðàììíûì ñèñ-
òåìàì.  êà÷åñòâå ôîðìàëüíîãî ÿçûêà òðåáîâàíèé è ñïåöèôèêàöèè ñèñòåì èñïîëüçó-
åòñÿ ÿçûê áàçîâûõ ïðîòîêîëîâ. Îáùàÿ òåîðèÿ áàçîâûõ ïðîòîêîëîâ ïîñòðîåíà â ðàáî-
òàõ [4, 5]. Äëÿ ñèìâîëüíîé âåðèôèêàöèè ìíîæåñòâà ñîñòîÿíèé ïðåäñòàâëÿþòñÿ ôîð-
ìóëàìè ìíîãîñîðòíîãî èñ÷èñëåíèÿ ïðåäèêàòîâ ïåðâîãî ïîðÿäêà. Íà ìíîæåñòâå ýòèõ
ôîðìóë îïðåäåëÿåòñÿ îòíîøåíèå ïåðåõîäîâ, ðàçìå÷åííûõ áàçîâûìè ïðîòîêîëàìè,
êîòîðûå ðàññìàòðèâàþòñÿ êàê äåéñòâèÿ, âûïîëíÿåìûå â ñèñòåìå. Â ïðîöåññå îñóùå-
ñòâëåíèÿ ïåðåõîäîâ â ïðîñòðàíñòâå ôîðìóë ïîñòóñëîâèå ðàññìàòðèâàåòñÿ êàê îïåðà-
òîð, îïðåäåëåííûé íà ìíîæåñòâå ôîðìóë. Ïîñêîëüêó ýòîò îïåðàòîð ïðåîáðàçóåò îäíè
ôîðìóëû â äðóãèå, èñïîëüçóåì òåðìèí «ïðåäèêàòíûé òðàíñôîðìåð», ââåäåííûé
Äèêñòðîé â [6] è ðàñïðîñòðàíåííûé Ëåìïîðòîì íà ïàðàëëåëüíûå ïðîãðàììû â [7].
 ñèñòåìå VRS ñòðîèòñÿ ïðåäèêàòíûé òðàíñôîðìåð è äîêàçûâàþòñÿ åãî îñíîâíûå
ñâîéñòâà, ñîãëàñíî êîòîðûì îí âû÷èñëÿåò ñèëüíåéøåå ïîñòóñëîâèå äëÿ ñèìâîëüíûõ
ñîñòîÿíèé. Äàåòñÿ êðàòêèé îáçîð ïðèìåíåíèé ïðåäèêàòíîãî òðàíñôîðìåðà äëÿ âåðè-
ôèêàöèè òðåáîâàíèé ê ïðîãðàììíûì ñèñòåìàì. ×àñòíûé ñëó÷àé ïðåäèêàòíîãî òðàíñ-
ôîðìåðà äëÿ áîëåå ïðîñòîãî ëîãè÷åñêîãî ÿçûêà (ïðîñòûå è ôóíêöèîíàëüíûå òèïû
äàííûõ, îïåðàòîðû ïðèñâàèâàíèÿ â ïîñòóñëîâèÿõ) ðàññìîòðåí â ðàáîòå [8]. Â íàñòîÿ-
ùåé ñòàòüå êðîìå ïðîñòûõ è ôóíêöèîíàëüíûõ òèïîâ äîïóñêàþòñÿ î÷åðåäè, à â ïî-
ñòóñëîâèÿõ êðîìå ïðèñâàèâàíèé äîïóñêàþòñÿ îïåðàòîðû îáíîâëåíèÿ î÷åðåäåé è ïðî-
èçâîëüíûå ôîðìóëû. Òàêæå, èñïîëüçóåòñÿ ïîäõîä, îñíîâàííûé íà ðàçäåëüíîì ðàñ-
ñìîòðåíèè ïåðåõîäîâ, îïðåäåëåííûõ ïîñòóñëîâèÿìè è áàçîâûìè ïðîòîêîëàìè.
ÀÒÐÈÁÓÒÍÛÅ ÂÛÐÀÆÅÍÈß
Ìîäåëü ñèñòåìû ñîñòîèò èç ìíîæåñòâà áàçîâûõ ïðîòîêîëîâ B è îïèñàíèÿ
ñðåäû E. Ñðåäà ïðåäñòàâëÿåòñÿ â âèäå êîìïîçèöèè ñâîåãî ÿäðà è ñîâîêóïíîñòè
àãåíòîâ, ïîãðóæåííûõ â ñðåäó [9, 10].
Ðàññìîòðèì ôðàãìåíò îïèñàíèÿ ñðåäû, êîòîðàÿ ìîäåëèðóåò òåëåôîííóþ ñåòü
(ñìûñë ñàìîé ìîäåëè â äàííîì ñëó÷àå íå èìååò çíà÷åíèÿ, ïðèìåð èñïîëüçóåòñÿ äëÿ
èëëþñòðàöèè íåêîòîðûõ ñèíòàêñè÷åñêèõ êîíñòðóêöèé).
environment (
types: obj (
PhoneNumber: ( phone_1, phone_2, phone_3, phone_4, NON_DEF),
PhoneState: (
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 3
© À.À. Ëåòè÷åâñêèé, À.Á. Ãîäëåâñêèé, À.À. Ëåòè÷åâñêèé (ìë.), Ñ.Â. Ïîòèåíêî, Â.Ñ. Ïåñ÷àíåíêo, 2010
BUSY_STATE, RINGING_STATE, FREE_STATE,
CONNECTED_STATE, DIAL_STATE, FASTBUSY_STATE, CWH,
CALL_WAITING_STATE, THREE_WAY_STATE, HOLD_STATE
)
);
attributes: obj (
State: PhoneNumber � PhoneState
) ;
agent_types: obj (
Phone: obj (
CW_Connected: PhoneNumber,
CW_Hold: PhoneNumber,
TW1: PhoneNumber,
TW2: PhoneNumber,
Three_Hold: PhoneNumber,
rel: PhoneNumber
)
);
................................
);
 ýòîì îïèñàíèè ñðåäû îïðåäåëÿþòñÿ äâà ïåðå÷èñëèìûõ òèïà äàííûõ:
PhoneNumber è PhoneState; ïåðå÷èñëÿþòñÿ ñèìâîëüíûå êîíñòàíòû, îòíîñÿùèåñÿ
ê ýòèì òèïàì; îïðåäåëÿþòñÿ àòðèáóò ñðåäû State ôóíêöèîíàëüíîãî òèïà, îòîáðàæà-
þùèé íîìåðà òåëåôîíîâ â èõ ñîñòîÿíèÿ, à òàêæå òèï àãåíòà Phone è åãî àòðèáóòû
ïåðå÷èñëèìîãî òèïà.
Áàçîâûé ïðîòîêîë ïðåäñòàâëÿåò ñîáîé ôîðìóëó äèíàìè÷åñêîé ëîãèêè (òðîéêó
Õîðà) � � � �x r x P r x r x( ( , ) ( , ) ( , ))� � è îïèñûâàåò ëîêàëüíûå ñâîéñòâà ñèñòåìû
â òåðìèíàõ ïðåä- è ïîñòóñëîâèé � è �. Îáà óñëîâèÿ ÿâëÿþòñÿ ôîðìóëàìè ìíîãî-
ñîðòíîé ëîãèêè ïåðâîãî ïîðÿäêà, èíòåðïðåòèðîâàííîé íà íåêîòîðûõ îáëàñòÿõ äàí-
íûõ. Ïîñòóñëîâèå â îòëè÷èå îò ïðåäóñëîâèÿ êðîìå ëîãè÷åñêèõ ôîðìóë ìîæåò ñî-
äåðæàòü îïåðàòîðû ïðèñâàèâàíèÿ. Ïðîöåññ Ð ïðåäñòàâëåí ñðåäñòâàìè MSC äèà-
ãðàìì [11–14] è îïèñûâàåò ñöåíàðèé ïîâåäåíèÿ ñïåöèôèöèðîâàííîé ñðåäû
ñ ïîãðóæåííûìè â íåå àãåíòàìè, êîòîðûé ìîæåò àêòèâèçèðîâàòüñÿ ïðè âûïîëíåíèè
ïðåäóñëîâèÿ. Ñèìâîë x ïðåäñòàâëÿåò ñïèñîê òèïèçèðîâàííûõ ïåðåìåííûõ, r —
ñïèñîê àòðèáóòíûõ âûðàæåíèé àãåíòîâ è ñðåäû.
Îïèñàíèå ñðåäû E îïðåäåëÿåò ñèãíàòóðó ÿçûêà, èñïîëüçóåìîãî äëÿ âûðàæåíèÿ
ïðåä- è ïîñòóñëîâèé â áàçîâûõ ïðîòîêîëàõ è èíòåðïðåòàöèþ ýòîé ñèãíàòóðû. Ñèã-
íàòóðà ÿçûêà âêëþ÷àåò ñèãíàòóðó òèïîâ (ñîðòîâ ìíîãîñîðòíîãî èñ÷èñëåíèÿ) è ñèã-
íàòóðó ôóíêöèîíàëüíûõ è ïðåäèêàòíûõ ñèìâîëîâ. Ñèãíàòóðà òèïîâ ñîäåðæèò
ïðåäîïðåäåëåííûå ïðîñòûå òèïû — int, real, symb, ïåðå÷èñëèìûå òèïû, êîòîðûå
îïðåäåëÿþòñÿ â îïèñàíèè ñðåäû, è ôóíêöèîíàëüíûå òèïû âèäà ( , ,... )� � �1 2 � , ãäå
� � �, , ,...1 2 — ïðîñòûå òèïû. Êðîìå òîãî, â ñèãíàòóðå òèïîâ èìååòñÿ ïðåäîïðåäå-
ëåííûé ïàðàìåòðè÷åñêèé òèï queue of � , ãäå � — ïðîñòîé òèï, îáîçíà÷àþùèé î÷å-
ðåäü ýëåìåíòîâ òèïà � .
Ïðåäîïðåäåëåííûå ôóíêöèîíàëüíûå è ïðåäèêàòíûå ñèìâîëû âêëþ÷àþò ñèì-
âîëû àðèôìåòè÷åñêèõ îïåðàöèé � , � , * è îòíîøåíèé >, � , �� , �� , � , à òàêæå êîí-
ñòðóêòîðû äëÿ ñèìâîëüíîãî òèïà («,», «;» è ò.ä.). Îáëàñòüþ çíà÷åíèé ñèìâîëüíîãî
òèïà äàííûõ ÿâëÿåòñÿ ìíîæåñòâî ñâîáîäíûõ òåðìîâ, îáðàçîâàííûõ êîíñòðóêòîðà-
ìè èç ñèìâîëüíûõ êîíñòàíò è äàííûõ ïðîñòûõ òèïîâ.
Ïðîñòûå àòðèáóòû ñðåäû ðàññìàòðèâàþòñÿ êàê íåèíòåðïðåòèðîâàííûå ôóíê-
öèîíàëüíûå ñèìâîëû àðíîñòè 0, âñå îñòàëüíûå àòðèáóòû ÿâëÿþòñÿ íåèíòåðïðåòè-
ðîâàííûìè ôóíêöèîíàëüíûìè ñèìâîëàìè àðíîñòè áîëüøå íóëÿ. Àòðèáóòíûå âûðà-
æåíèÿ — ýòî ïðîñòûå àòðèáóòû èëè âûðàæåíèÿ âèäà f t t( , ,... )1 2 , ãäå àòðèáóò f
èìååò ôóíêöèîíàëüíûé òèï ( , ,... )� � �1 2 � , à t t1 2, ,... — ïàðàìåòðû àòðèáóòíîãî
ôóíêöèîíàëüíîãî âûðàæåíèÿ, ò.å. òåðìû òèïîâ � �1 2, ,...
4 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
Âî âõîäíîì ÿçûêå VRS ðàçëè÷àþòñÿ àòðèáóòû ñðåäû è àòðèáóòû àãåíòîâ. Ñîîòâåò-
ñòâåííî ðàçëè÷àþòñÿ àòðèáóòíûå âûðàæåíèÿ ñðåäû è àãåíòíûå àòðèáóòíûå âûðàæåíèÿ.
Äëÿ àòðèáóòíûõ âûðàæåíèé ñðåäû èñïîëüçóåòñÿ ïðåôèêñíàÿ çàïèñü (êàê ïîêàçàíî
âûøå), à äëÿ àãåíòíûõ àòðèáóòíûõ âûðàæåíèé èñïîëüçóåòñÿ áîëåå ñëîæíûé ñèíòàêñèñ.
Òàê, åñëè � — òèï àãåíòà, à x — åãî ïðîñòîé àòðèáóò, òî ñîîòâåòñòâóþùåå àãåíòíîå
âûðàæåíèå èìååò âèä �( ).t x , ãäå t åñòü èìÿ àãåíòà, ïðåäñòàâëåííîå âûðàæåíèåì
ñèìâîëüíîãî òèïà (àòðèáóò x àãåíòà t òèïà � ). Åñëè æå àòðèáóò x èìååò àðíîñòü áîëüøå
íóëÿ, òî àòðèáóòíîå âûðàæåíèå èìååò âèä �( ). ( , ,... )t x t t1 2 .
 òåîðèè öåëåñîîáðàçíî óíèôèöèðîâàòü îáîçíà÷åíèÿ äëÿ àòðèáóòíûõ âûðàæå-
íèé, ñâåäÿ èõ âñå ê ïðåôèêñíîé çàïèñè. Äëÿ ýòîãî ïåðåêîäèðóåì àãåíòíûå àòðèáóò-
íûå âûðàæåíèÿ, ïîâûñèâ èõ àðíîñòü íà åäèíèöó, è áóäåì ðàññìàòðèâàòü èìÿ àãåíòà
êàê äîïîëíèòåëüíûé àðãóìåíò ñëåäóþùèì îáðàçîì. Àòðèáóòíîå âûðàæåíèå �( ).t x
çàìåíèì ( (). )( )� x t , à âûðàæåíèå �( ). ( , ,... )t x t t1 2 — âûðàæåíèåì
( (). )( , , ,... )� x t t t1 2 . Ïðè ýòîì âûðàæåíèå ( (). )� x ðàññìàòðèâàåòñÿ êàê íîâûé ñèìâîë
àòðèáóòà x àãåíòà òèïà � , èìÿ êîòîðîãî ÿâëÿåòñÿ ïåðâûì àðãóìåíòîì àòðèáóòíîãî
âûðàæåíèÿ. Èñõîäÿ èç ýòèõ ñîãëàøåíèé, ïðîèçâîëüíîå àòðèáóòíîå âûðàæåíèå áó-
äåì îáîçíà÷àòü êàê f t t( , ,... )1 2 , äîïóñêàÿ â êà÷åñòâå ÷àñòíîãî ñëó÷àÿ ïóñòîé
ñïèñîê ïàðàìåòðîâ f f() � äëÿ ïðîñòûõ àòðèáóòîâ.
Ìíîæåñòâî âñåõ àòðèáóòíûõ âûðàæåíèé äëÿ çàäàííîé ñðåäû E îáîçíà÷èì AE .
Àòðèáóòíîå âûðàæåíèå f t t( , ,... )1 2 íàçîâåì êîíñòàíòíûì, åñëè âñå åãî ïàðàìåòðû ñóòü
êîíñòàíòíûå òåðìû, ò.å. íå ñîäåðæàò íè àòðèáóòíûõ âûðàæåíèé, íè ïåðåìåííûõ. Ìíî-
æåñòâî âñåõ êîíñòàíòíûõ àòðèáóòíûõ âûðàæåíèé äëÿ ñðåäû E îáîçíà÷èì A
E
const .
Î×ÅÐÅÄÈ ÝËÅÌÅÍÒΠÏÐÎÑÒÛÕ ÒÈÏÎÂ
Ñïèñêîì íàçîâåì ñèìâîëüíóþ ñòðóêòóðó äàííûõ, êîòîðàÿ îáðàçóåòñÿ ñ ïîìîùüþ
êîíñòðóêòîðà ((),()). Ñïèñîê íàçûâàåòñÿ òåðìèíàëüíûì, åñëè îí îáðàçîâàí ïî
ñëåäóþùèì ïðàâèëàì:
1) ñèìâîëüíàÿ êîíñòàíòà Nil åñòü òåðìèíàëüíûé ñïèñîê (ïóñòîé òåðìèíàëüíûé
ñïèñîê);
2) åñëè a — ñèìâîëüíûé òåðì, à l — òåðìèíàëüíûé ñïèñîê, òî ñèìâîëüíûé
òåðì ( , )a l òàêæå åñòü òåðìèíàëüíûé ñïèñîê, à åãî ýëåìåíòàìè ÿâëÿþòñÿ òåðì a è
ýëåìåíòû òåðìèíàëüíîãî ñïèñêà l.
Ïðèìåð òåðìèíàëüíîãî ñïèñêà èç òðåõ ýëåìåíòîâ: ((x1,10), r2 + à2, 999, Nil).
Îáîçíà÷èì LE ìíîæåñòâî âñåõ òåðìèíàëüíûõ ñïèñêîâ, à L
E
const — ìíîæåñòâî âñåõ
êîíñòàíòíûõ òåðìèíàëüíûõ ñïèñêîâ, ò.å. òåðìèíàëüíûõ ñïèñêîâ, ñîñòàâëåííûõ èç
êîíñòàíòíûõ òåðìîâ.
Òåïåðü ìîæíî îïðåäåëèòü òèï äàííûõ queue of � . Çíà÷åíèÿìè ýòîãî òèïà ÿâ-
ëÿþòñÿ òåðìèíàëüíûå êîíñòàíòíûå ñïèñêè, ýëåìåíòàìè êîòîðûõ åñòü êîíñòàíòû
òèïà � . Íà î÷åðåäÿõ òèïà queue of � îïðåäåëåíû ôóíêöèè äîñòóïà get_from_head x
è get from tail x, êîòîðûå ìîãóò èñïîëüçîâàòüñÿ òîëüêî â ïðåäóñëîâèÿõ áàçîâûõ
ïðîòîêîëîâ, è îïåðàòîðû îáíîâëåíèÿ ñïèñêîâ add_to_head (x, t), add_to_tail (x, t),
remove_from_head (x) è remove_from_tail (x). Çäåñü x — ýòî àòðèáóòíîå âûðàæå-
íèå òèïà î÷åðåäü, à t — òåðì ñîîòâåòñòâóþùåãî òèïà.
Îïåðàòîðû ïðèñâàèâàíèÿ è îáíîâëåíèÿ ñïèñêîâ ìîãóò èñïîëüçîâàòüñÿ òîëüêî
â ïîñòóñëîâèÿõ. Äëÿ óíèôèêàöèè îáîçíà÷åíèé áóäåì ñ÷èòàòü, ÷òî îïåðàòîð óäàëå-
íèÿ (remove) òàêæå èìååò äâà àðãóìåíòà, íî â êà÷åñòâå âòîðîãî àðãóìåíòà
èñïîëüçóåòñÿ ñèìâîëüíàÿ êîíñòàíòà Nil.
ÎÏÅÐÀÒÎÐ ÏÎÑÒÓÑËÎÂÈß
Áàçîâûå ïðîòîêîëû îïðåäåëÿþò îòíîøåíèå ïåðåõîäîâ íà ìíîæåñòâå ñîñòîÿíèé
ñïåöèôèöèðóåìîé ñèñòåìû. Ïðè ýòîì ïðåäóñëîâèÿ èñïîëüçóþòñÿ äëÿ îïðåäåëå-
íèÿ ïðèìåíèìîñòè áàçîâîãî ïðîòîêîëà, à ïîñòóñëîâèÿ — äëÿ âûïîëíåíèÿ ïðåîá-
ðàçîâàíèé. Äàëåå áóäåì ðàññìàòðèâàòü ñâîéñòâà ïîñòóñëîâèé êàê îïåðàòîðîâ,
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 5
îïðåäåëåííûõ íà ñîñòîÿíèÿõ ñðåäû, íåçàâèñèìî îò ïðåäóñëîâèé. Ñèíòàêñè÷åñêè
îïåðàòîð ïîñòóñëîâèÿ ïðåäñòàâëÿåò ñîáîé êîíúþíêöèþ � � R U C , ãäå
R r t r t� � � ( : : ... )1 1 2 2
ÿâëÿåòñÿ êîíúþíêöèåé îïåðàòîðîâ ïðèñâàèâàíèÿ,
U p g h p g h� 1 1 1 2 2 2( , ) ( , ) �
ÿâëÿåòñÿ êîíúþíêöèåé îïåðàòîðîâ îáíîâëåíèÿ î÷åðåäåé, à C — ëîãè÷åñêàÿ ôîð-
ìóëà, ïîñòðîåííàÿ èç àòðèáóòíûõ âûðàæåíèé, îòíîøåíèé ðàâåíñòâ (îíè îïðåäåëå-
íû äëÿ âñåõ òèïîâ), àðèôìåòè÷åñêèõ îòíîøåíèé, ëîãè÷åñêèõ ñâÿçîê è êâàíòîðîâ
(â ÿçûêå VRS èñïîëüçóåòñÿ òîëüêî êâàíòîð ñóùåñòâîâàíèÿ ïî ïåðåìåííûì ïðîñòî-
ãî òèïà, äîïóñêàåòñÿ òàêæå èñïîëüçîâàíèå îãðàíè÷åííûõ êâàíòîðîâ îáùíîñòè).
Îïðåäåëèì ñåìàíòèêó îïåðàòîðîâ ïîñòóñëîâèé êàê ïðåîáðàçîâàíèé íà ìíî-
æåñòâå ñîñòîÿíèé ñðåäû. Îïåðàòîðû ïîñòóñëîâèé çàäàþò ïåðåõîäû íà ìíîæåñòâå
ñîñòîÿíèé ñðåäû, ðàçìå÷åííûå ýòèìè îïåðàòîðàìè, ïðåîáðàçóÿ ñðåäó â òðàíçèöè-
îííóþ ñèñòåìó. Ïðè ýòîì ðàçëè÷àþòñÿ äâà êëàññà ìîäåëåé ñðåäû: êîíêðåòíûå
è ñèìâîëüíûå ìîäåëè (ñîîòâåòñòâåííî êîíêðåòíàÿ è ñèìâîëüíàÿ ñåìàíòèêà îïåðà-
òîðîâ ïîñòóñëîâèé). Ñîñòîÿíèå êîíêðåòíîé ìîäåëè îïðåäåëÿåòñÿ ÿâíî çàäàííûìè
çíà÷åíèÿìè êîíñòàíòíûõ àòðèáóòíûõ âûðàæåíèé, ñîñòîÿíèå ñèìâîëüíîé ìîäåëè
îïðåäåëÿåòñÿ ëîãè÷åñêîé ôîðìóëîé, êîòîðàÿ «ïîêðûâàåò» ìíîæåñòâî êîíêðåòíûõ
ñîñòîÿíèé. Äëÿ ïîñòðîåíèÿ ñèìâîëüíîé ñåìàíòèêè ñëåäóåò ðàçëè÷àòü çíà÷åíèÿ àò-
ðèáóòíûõ âûðàæåíèé â ñîñòîÿíèè ìîäåëè äî è ïîñëå âûïîëíåíèÿ ïðåîáðàçîâàíèÿ.
Åñëè ñîñòîÿíèå ìîäåëè ïîñëå âûïîëíåíèÿ ïðåîáðàçîâàíèÿ îïðåäåëÿåòñÿ ëîãè÷å-
ñêîé ôîðìóëîé, ñâÿçûâàþùåé àòðèáóòíûå âûðàæåíèÿ è íàêëàäûâàþùåé îãðàíè÷å-
íèÿ íà èõ âîçìîæíûå êîíêðåòíûå çíà÷åíèÿ â òåêóùåì ñîñòîÿíèè, òî çíà÷åíèÿ ýòèõ
àòðèáóòíûõ âûðàæåíèé äî ïðèìåíåíèÿ ïðåîáðàçîâàíèÿ áóäóò ïðåäñòàâëåíû
ïåðåìåííûìè, âçàèìíî îäíîçíà÷íî ñîîòâåòñòâóþùèìè ýòèì âûðàæåíèÿì.
Ðàññìîòðèì ÷åòûðå îñíîâíûõ ìíîæåñòâà àòðèáóòíûõ âûðàæåíèé è ñîîòâåò-
ñòâóþùèõ èì ïåðåìåííûõ.
Ïåðâîå ìíîæåñòâî ïðåäñòàâëåíî ñïèñêîì r � ( , ,... )r r1 2 è ñîñòîèò èç ëåâûõ ÷àñ-
òåé îïåðàòîðîâ ïðèñâàèâàíèÿ èç êîíúþíêöèè R. Â íåãî âõîäÿò òå àòðèáóòíûå âûðàæå-
íèÿ, êîòîðûå èçìåíÿþò ñâîå çíà÷åíèå â ðåçóëüòàòå âûïîëíåíèÿ ïðèñâàèâàíèé.
Àòðèáóòíûå âûðàæåíèÿ èç ñïèñêà r èìåþò ïðîñòûå òèïû. Ñïèñîê ïåðåìåííûõ, âçàèì-
íî îäíîçíà÷íî ñîîòâåòñòâóþùèõ àòðèáóòàì èç ñïèñêà r, îáîçíà÷èì x � ( , ,... )x x1 2 .
Âòîðîå ìíîæåñòâî ïðåäñòàâëåíî ñïèñêîì g � ( , ,... )g g1 2 è ñîñòîèò èç àòðèáóò-
íûõ âûðàæåíèé, çíà÷åíèÿ êîòîðûõ îáíîâëÿþòñÿ îïåðàòîðàìè îáíîâëåíèÿ î÷åðåäåé
èç êîíúþíêöèè U. Ýëåìåíòû ýòîãî ñïèñêà èìåþò òèï î÷åðåäè. Ñïèñîê ïåðåìåí-
íûõ, âçàèìíî îäíîçíà÷íî ñîîòâåòñòâóþùèõ àòðèáóòàì èç ñïèñêà g, îáîçíà÷èì
w � ( , ,... )w w1 2 .
Òðåòüå ìíîæåñòâî ïðåäñòàâëåíî ñïèñêîì s � ( , ,... )s s1 2 è ñîñòîèò èç âíåøíèõ
âõîæäåíèé àòðèáóòíûõ âûðàæåíèé â ôîðìóëó C, îòëè÷íûõ îò àòðèáóòíûõ âûðàæå-
íèé èç r (àòðèáóòíûå âûðàæåíèÿ òèïà î÷åðåäè â ôîðìóëó C âõîäèòü íå ìîãóò).
Ýòèì àòðèáóòíûì âûðàæåíèÿì âçàèìíî îäíîçíà÷íî ñîîòâåòñòâóþò ïåðåìåííûå èç
ñïèñêà y � ( , ,... )y y1 2 .
×åòâåðòîå ìíîæåñòâî ïðåäñòàâëåíî ñïèñêîì z � ( , ,... )z z1 2 è ôîðìèðóåòñÿ äëÿ
èñïîëüçîâàíèÿ îïåðàòîðîì ïîñòóñëîâèÿ � âìåñòå ñ ôîðìóëîé � ñèìâîëüíîãî ñîñòî-
ÿíèÿ ñðåäû. Ñïèñîê âêëþ÷àåò âñå âíåøíèå âõîæäåíèÿ àòðèáóòíûõ âûðàæåíèé â
ôîðìóëó � è â ïðàâûå ÷àñòè ïðèñâàèâàíèé èç R, îòëè÷íûå îò ýëåìåíòîâ óæå
ïîñòðîåííûõ ñïèñêîâ.
 äàëüíåéøåì äëÿ îïåðàòîðà ïîñòóñëîâèÿ � � R U C áóäóò èñïîëüçîâàíû
ñëåäóþùèå ñîêðàùåíèÿ:
R r t r t t� � � � �( : : ... ) ( : )1 1 2 2 r , U p g h p g h p h� �1 1 1 2 2 2( , ) ( , ) ( , )� g .
6 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
ÊÎÍÊÐÅÒÍÛÅ ÌÎÄÅËÈ
Êîíêðåòíàÿ ìîäåëü ñðåäû — ýòî òðàíçèöèîííàÿ ñèñòåìà ñ êîíêðåòíûìè ñîñòîÿ-
íèÿìè. Êîíêðåòíûì ñîñòîÿíèåì � : A D
E
const � íàçûâàåòñÿ îòîáðàæåíèå èç ìíî-
æåñòâà êîíñòàíòíûõ òåðìîâ â îáëàñòü èõ çíà÷åíèé. Ïîñêîëüêó â ñèñòåìå VRS
òèïèçèðîâàíû è àòðèáóòíûå âûðàæåíèÿ, è èõ çíà÷åíèÿ, òî ýòî îòîáðàæåíèå
äîëæíî ñîãëàñîâûâàòüñÿ ñ îïèñàíèÿìè òèïîâ. Òàê, åñëè àòðèáóò f èìååò òèï
( , ,... )� � �1 2 � , òî f c c( , ,... )1 2 èìååò òèï � . Ìíîæåñòâî D âêëþ÷àåò â ñåáÿ âñå
öåëûå è âåùåñòâåííûå ÷èñëà, ñèìâîëüíûå çíà÷åíèÿ (ñâîáîäíûå òåðìû), âñå çíà-
÷åíèÿ ïåðå÷èñëèìûõ òèïîâ è âñå çíà÷åíèÿ òèïà î÷åðåäè. Ìíîæåñòâî âñåõ êîí-
êðåòíûõ ñîñòîÿíèé îáîçíà÷èì ÷åðåç CE .
Êîíêðåòíûå ñîñòîÿíèÿ — ýòî îòîáðàæåíèÿ, îïðåäåëåííûå íà êîíñòàíòíûõ òåð-
ìàõ. Ðàñïðîñòðàíèì ýòè îòîáðàæåíèÿ íà ïðîèçâîëüíûå òåðìû. Çàìåòèì, ÷òî òåð-
ìû — ýòî âûðàæåíèÿ, ïîñòðîåííûå èç êîíñòàíò, àòðèáóòíûõ âûðàæåíèé è ïåðå-
ìåííûõ. Ðàññìîòðèì ñèñòåìó ïåðåïèñûâàþùèõ ïðàâèë
S x x x A
E� �� �
{ }const( ) | .
Ïóñòü F — ýòî òåðì èëè ôîðìóëà. Òîãäà �( )F åñòü ðåçóëüòàò íîðìàëèçàöèè âû-
ðàæåíèÿ F ïóòåì ïðèìåíåíèÿ ñèñòåìû ïåðåïèñûâàþùèõ ïðàâèë S � ê ýòîìó âû-
ðàæåíèþ. Ïðèìåíåíèå ïðàâèë ïðîèñõîäèò ñ âûïîëíåíèåì âñåõ íåîáõîäèìûõ âû-
÷èñëåíèé äëÿ èíòåðïðåòèðîâàííûõ îïåðàöèé è îòíîøåíèé (íàïðèìåð, âûðàæåíèå
3 5� óïðîùàåòñÿ äî 8, âûðàæåíèå x � 0 — äî x, à 3 5� ïðåîáðàçóåòñÿ â èñòèííîñ-
òíîå çíà÷åíèå 1). Ñèñòåìà ïåðåïèñûâàþùèõ ïðàâèë êàíîíè÷íà, ïîýòîìó ðåçóëü-
òàò íîðìàëèçàöèè âñåãäà îïðåäåëåí è íå çàâèñèò îò ñòðàòåãèè. Ðåçóëüòàòîì ïðè-
ìåíåíèÿ ñèñòåìû S � ê âûðàæåíèþ F áóäåò êîíñòàíòà èëè âûðàæåíèå, íå ñîäåð-
æàùåå êîíñòàíòíûõ òåðìîâ, îòëè÷íûõ îò êîíñòàíòû.
Ïóñòü òåïåðü F — ýòî ôîðìóëà, íå ñîäåðæàùàÿ ñâîáîäíûõ ïåðåìåííûõ (ò.å.
âñå ïåðåìåííûå ñâÿçàíû êâàíòîðàìè). Ñîñòîÿíèå � ïîëíîñòüþ çàäàåò èíòåðïðåòà-
öèþ ñèãíàòóðû ôîðìóëû F, ïîýòîìó ìîæíî ãîâîðèòü îá èñòèííîñòè ôîðìóëû F íà
ýòîì ñîñòîÿíèè. Òîò ôàêò, ÷òî ôîðìóëà F èñòèííà, áóäåì çàïèñûâàòü êàê � | � F.
Âíåøíÿÿ ïîäñòàíîâêà.  îòëè÷èå îò ïîëíîé ïîäñòàíîâêè �( )F ïðè âíåøíåé
ïîäñòàíîâêå out F( , )� ïîëíîñòüþ âû÷èñëÿþòñÿ òîëüêî âíåøíèå âõîæäåíèÿ àòðè-
áóòíûõ âûðàæåíèé â F (ôîðìóëà èëè òåðì). Ýòà ïîäñòàíîâêà îïðåäåëÿåòñÿ ñëåäóþ-
ùåé ñèñòåìîé ïðàâèë:
out xp x x out p x( , ( )) ( , ( ))� �� � � ,
out f t f t( , ( )) ( ( ))� �� ,
out t out t( , ( )) ( ( , ))� � � �� ,
out f f( , )� � ,
out ( , )� � �� .
 ýòèõ ïðàâèëàõ x x x� ( , ,... )1 2 — ñïèñîê ïåðåìåííûõ, t t t� ( , ,... )1 2 — ñïèñîê
àðãóìåíòîâ àòðèáóòíîãî âûðàæåíèÿ f t( ) , f — àòðèáóò, � — ñèìâîë èíòåðïðå-
òèðîâàííîé ôóíêöèè ëèáî ëîãè÷åñêàÿ ñâÿçêà, ëèáî ïðåäèêàòíûé ñèìâîë, ëèáî
ïåðåìåííàÿ.
Äàëåå îïðåäåëèì îòíîøåíèå ïåðåõîäîâ íà ìíîæåñòâå CE êîíêðåòíûõ ñîñòîÿ-
íèé ñðåäû E. Äåéñòâèÿìè òðàíçèöèîííîé ñèñòåìû CE ÿâëÿþòñÿ îïåðàòîðû ïîñòóñ-
ëîâèé. Ïóñòü � � R U C — îïåðàòîð ïîñòóñëîâèÿ, à � è �� — êîíêðåòíûå ñî-
ñòîÿíèÿ. Ïåðåõîä
� �
�
�
�
âîçìîæåí, åñëè âûïîëíÿþòñÿ ñëåäóþùèå óñëîâèÿ:
1) � � �� �( ( , )) ( )out tr ;
2) � � � �� �( ( , )) ( ( ), ( ))out p hg g ;
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 7
3) î÷åðåäè, ê êîòîðûì ïðèìåíÿþòñÿ îïåðàòîðû óäàëåíèÿ ýëåìåíòîâ, äîëæíû
áûòü íåïóñòûìè;
4) � �� � �| ( )C ;
5) x out y y x x x A
E
�
� � � � �
{ { } { } { }} const( , )| ( ) ( ),� � �r g s .
 ýòèõ îïðåäåëåíèÿõ ñïèñêè òåðìîâ ðàññìàòðèâàþòñÿ êàê ñèìâîëüíûå ñòðóêòóðû
äàííûõ. Òàê, íàïðèìåð, ïåðâîå óñëîâèå ìîæíî ïðåäñòàâèòü ñëåäóþùèì îáðàçîì:
� � � � � � �� � � � �( ( , )) ( ( ( , )), ( ( , )) , ... ) ( (out out r out rr 1 2 t t1 2), ( ),... )� �
� � � � �� � � � � �( ( , )) ( ), ( ( , )) ( ),...out r t out r t1 1 2 2
Åñëè x x x� ( , ,... )1 2 , òî { } { }x x x� 1 2, ,... îáîçíà÷àåò ìíîæåñòâî åãî ýëåìåíòîâ. Íà
îñíîâàíèè óñëîâèÿ 5 â íîâîì ñîñòîÿíèè ìîãóò ïîëó÷èòü íîâûå çíà÷åíèÿ òîëüêî
àòðèáóòíûå âûðàæåíèÿ èç ìíîæåñòâà { } { } { }r g s� � .
Ñèñòåìà CE ìîæåò áûòü íåäåòåðìèíèðîâàííîé. Îäíàêî ýòîò íåäåòåðìèíèçì
îïðåäåëÿåòñÿ òîëüêî íàëè÷èåì ôîðìóëû C â ïîñòóñëîâèè. Åñëè C � 1, òî ñèñòåìà
CE äåòåðìèíèðîâàíà.
ÑÈÌÂÎËÜÍÛÅ ÌÎÄÅËÈ
Ñèìâîëüíûå ìîäåëè ñðåäû ðàññìàòðèâàþòñÿ êàê àáñòðàêöèè êîíêðåòíûõ ìîäåëåé,
à èõ ñîñòîÿíèÿ — êàê àáñòðàêöèè êîíêðåòíûõ ñîñòîÿíèé. Ñîñòîÿíèÿìè ñèìâîëü-
íûõ ìîäåëåé ÿâëÿþòñÿ ôîðìóëû âèäà � � � v L v F v( ( ) ( )) , ãäå v v v� ( , ,... )1 2 —
ñïèñîê ïåðåìåííûõ, L v l L l L( ) ( ... )� � � 1 1 2 2 — ñïèñîê îïðåäåëÿþùèõ ðà-
âåíñòâ äëÿ î÷åðåäåé, à F v( ) — ôîðìóëà, íå ñîäåðæàùàÿ àòðèáóòíûõ âûðàæåíèé
òèïà î÷åðåäè. Àòðèáóòíûå âûðàæåíèÿ l l1 2, ,... èìåþò òèï î÷åðåäè, à L L1 2, ,... —
àáñòðàêòíûå î÷åðåäè, òèïû êîòîðûõ ñîãëàñóþòñÿ ñ òèïàìè àòðèáóòíûõ âûðàæå-
íèé l l1 2, ,... ñîîòâåòñòâåííî. Àáñòðàêòíàÿ î÷åðåäü òèïà � — ýòî ëèáî òåðìèíàëü-
íûé ñïèñîê òåðìîâ òèïà �, ëèáî âûðàæåíèå âèäà ( ; )P Q , ãäå P è Q — òåðìè-
íàëüíûå ñïèñêè òåðìîâ òèïà � . Àáñòðàêòíàÿ î÷åðåäü L ñîãëàñóåòñÿ ñ òèïîì
queue of � , åñëè âñå ñîñòàâëÿþùèå åå ýëåìåíòû èìåþò òèï � .
Ñåìàíòèêà àáñòðàêòíûõ î÷åðåäåé âûðàæàåòñÿ ÷åðåç êîíêàòåíàöèþ è êâàíòîðû
ïî ïåðåìåííûì òèïà î÷åðåäè ñëåäóþùèì îáðàçîì: ðàâåíñòâî ( ; )P Q R� ýêâèâà-
ëåíòíî ôîðìóëå � � � �w R P w Q( ) , ãäå � îáîçíà÷àåò êîíêàòåíàöèþ òåðìèíàëüíûõ
ñïèñêîâ
( , , ) ( , , ) ( , , ,a a a b b b a a a b bn n n1 2 1 2 1 2 1� � � � � � � �� � �Nil Nil 2 � �� bn , )Nil ,
Nil Nil* *P P P� � .
Åñëè R — àòðèáóòíûé òåðì, òî ðàâåíñòâî ÿâëÿåòñÿ îïðåäåëÿþùèì ðàâåíñòâîì
äëÿ ýòîãî òåðìà. Åñëè R — àáñòðàêòíàÿ î÷åðåäü, òî ðàâåíñòâî ñâîäèòñÿ ê ôîðìóëå
áåç î÷åðåäåé. Äåéñòâèòåëüíî, ( ; ) ( ; ) ( , ) ( )P Q P Q w w P w Q P w Q� � � � � � � � � �� �� � �
� R S , ãäå R íå ñîäåðæèò î÷åðåäåé, S w w p w w q� � � � � � �( , )( ) èëè
S w w w q p w� � � � � � �( , )( ) .  îáîèõ ñëó÷àÿõ S � 1.
Ìíîæåñòâî âñåõ ñîñòîÿíèé ñèìâîëüíîé ìîäåëè, îïðåäåëåííîé îïèñàíèåì ñðå-
äû E, îáîçíà÷èì S E . Ýòî ìíîæåñòâî ñòàíîâèòñÿ òðàíçèöèîííîé ñèñòåìîé ïóòåì
îïðåäåëåíèÿ îòíîøåíèÿ ïåðåõîäîâ ïî ïðàâèëó
� �
�
�
�
pt ( ) .
Ôóíêöèÿ pt pt� � � �( ) ( , )� (ïðåäèêàòíûé òðàíñôîðìåð) áóäåò îïðåäåëåíà íèæå. Åñëè
pt � �( ) � 0, ïåðåõîä ñ÷èòàåòñÿ íåîïðåäåëåííûì. Ñèñòåìà S E äåòåðìèíèðîâàíà.
Ñèìâîëüíûå ïîäñòàíîâêè. Ïóñòü �: A TE E� — îòîáðàæåíèå ìíîæåñòâà
âñåõ (ñèìâîëüíûõ è êîíñòàíòíûõ) àòðèáóòíûõ òåðìîâ â ìíîæåñòâî âñåõ òåðìîâ
(äëÿ çàäàííîãî îïèñàíèÿ ñðåäû E). Îïðåäåëèì ñèìâîëüíóþ ïîäñòàíîâêó �( )F ñ ïî-
ìîùüþ ñèñòåìû ïåðåïèñûâàþùèõ ïðàâèë { }x x x AE�
�( )| .  îòëè÷èå îò êîíêðåò-
íûõ ñîñòîÿíèé ðåçóëüòàò ïåðåïèñûâàíèÿ çàâèñèò îò ñòðàòåãèè. Ïðèìåì ñòðàòåãèþ
8 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
îäíîêðàòíîãî ïåðåïèñûâàíèÿ âíåøíèõ âõîæäåíèé àòðèáóòíûõ òåðìîâ. Îíà îïðåäå-
ëÿåòñÿ ñëåäóþùèìè ïðàâèëàìè, êîòîðûå äîáàâëÿþòñÿ ê ïðàâèëàì ïåðåïèñûâàíèÿ:
� �( ( )) ( ( ))� � �xp x x p x ,
� � � �( ( )) ( ( ))t t� ,
� � �( ) � .
Çíà÷åíèÿ ñèìâîëîâ, èñïîëüçóåìûõ â ýòèõ ïðàâèëàõ, òàêèå æå, êàê è â îïðåäåëå-
íèè âíåøíåé ïîäñòàíîâêè äëÿ êîíêðåòíûõ ñîñòîÿíèé. Äëÿ îïðåäåëåíèÿ âíåøíåé
ñèìâîëüíîé ïîäñòàíîâêè èñïîëüçóåì ïðàâèëà, êîòîðûå ïðèìåíÿëèñü âûøå äëÿ
êîíêðåòíûõ ñîñòîÿíèé �.
ÎÏÐÅÄÅËÅÍÈÅ ÏÐÅÄÈÊÀÒÍÎÃÎ ÒÐÀÍÑÔÎÐÌÅÐÀ
Ðàññìîòðèì ñëó÷àé, êîãäà âñå àòðèáóòíûå âûðàæåíèÿ, êîòîðûå íàõîäÿòñÿ â ïîñò-
óñëîâèè, èìåþò àðíîñòü 0, à îáíîâëåíèå ñïèñêîâ è ëîãè÷åñêàÿ ôîðìóëà C îòñóò-
ñòâóþò (C � 1).  ýòîì ñëó÷àå ïðåäïîëàãàåòñÿ, ÷òî ñâîè çíà÷åíèÿ ìîãóò èçìåíèòü
òîëüêî àòðèáóòû èç ñïèñêà r ëåâûõ ÷àñòåé ïðèñâàèâàíèé. Ïðåäèêàòíûé òðàíñ-
ôîðìåð îïðåäåëÿåòñÿ ïðîñòîé ôîðìóëîé
pt ( , ) ( ( ) ( ))� � � � �� � �x r t ,
ãäå � — ïîäñòàíîâêà ïåðåìåííûõ èç ñïèñêà x âìåñòî ïåðåìåííûõ èç ñïèñêà r, ò.å.
�( )r x� , t — ñïèñîê ïðàâûõ ÷àñòåé, x — ñïèñîê ïåðåìåííûõ, ñîîòâåòñòâóþùèõ
ëåâûì ÷àñòÿì, êàê áûëî îïðåäåëåíî âûøå. Ñîäåðæàòåëüíî ýòà ôîðìóëà óòâåðæäàåò,
÷òî ïîñëå âûïîëíåíèÿ îïåðàöèé ïðèñâàèâàíèÿ çíà÷åíèÿ ëåâûõ ÷àñòåé ïðèñâàèâàíèé
ðàâíû çíà÷åíèÿì ïðàâûõ ÷àñòåé, êîòîðûå îíè èìåëè äî âûïîëíåíèÿ ïðèñâàèâàíèé.
 ñëó÷àå C � 1ïðåäïîëàãàåòñÿ, ÷òî èçìåíèòü ñâîè çíà÷åíèÿ ìîãóò âñå àòðèáóò-
íûå âûðàæåíèÿ èç ñïèñêà s (âíåøíèå âõîæäåíèÿ â ôîðìóëó C). Ïîäñòàíîâêà � ðàñ-
ïðîñòðàíÿåòñÿ íà àòðèáóòíûå âûðàæåíèÿ s òàêèì îáðàçîì, ÷òî �( )s y� , è ñïèñîê
ïåðåìåííûõ y äîáàâëÿåòñÿ ïîä êâàíòîð ñóùåñòâîâàíèÿ. Åñëè â ïîñòóñëîâèÿ âõîäÿò
îïåðàòîðû îáíîâëåíèÿ î÷åðåäåé, òî ïîäñòàíîâêà � ðàñïðîñòðàíÿåòñÿ íà àòðèáóòíûå
âûðàæåíèÿ g òàêèì îáðàçîì, ÷òî �( )g w� , ñïèñîê ïåðåìåííûõ w çàíîñèòñÿ ïîä
êâàíòîð ñóùåñòâîâàíèÿ è äîáàâëÿþòñÿ ðàâåíñòâà äëÿ î÷åðåäåé
pt( , ) ( , , )( ( ) ( ( )) ( ( , ( ))))� � � � � �� � � � x w y r g wt p h C .
Îïåðàòîðû îáíîâëåíèÿ î÷åðåäåé îïðåäåëÿþòñÿ ñëåäóþùèì îáðàçîì:
g w� � � � p h g p w h g p w h( , ( )) (( ( , ( ))) ( ( , ( ))) .� � �1 1 1 1 2 2 2 2 .. ) ;
g w g w� � � �add_ to_ head ( , ( )) ( ( ), )� �h h Nil ;
g w g w� � � �add_ to_ tail ( , ( )) ( ( ), )� �h h Nil ;
g w w g� � � � � �remove_ from_ head ( , ) ( , )(( ( , ) )Nil Nilu v u v v) ;
g w w g� � � � �remove_ from_ tail ( , ) ( , )(( * ( , ))Nil Nilu v v u v) .
Ïåðåìåííàÿ u â äâóõ ïîñëåäíèõ îïðåäåëåíèÿõ èìååò òèï � , åñëè w èìååò òèï
queue of � , à ïåðåìåííàÿ v èìååò òîò æå òèï, ÷òî è w. Îïåðàöèÿ êîíêàòåíàöèè, êàê è
êâàíòîðû ïî ïåðåìåííûì òèïà î÷åðåäè, íå âõîäèò â ñèãíàòóðó ëîãè÷åñêîãî ÿçûêà
ìîäåëåé. Îïðåäåëåíèå ïðåäèêàòíîãî òðàíñôîðìåðà äàíî â ðàñøèðåííîì ÿçûêå. Íî
ýòî ðàñøèðåíèå ëåãêî ýëèìèíèðóåòñÿ ñëåäóþùèì îáðàçîì. Åñëè ñðåäè îïðåäåëÿþ-
ùèõ ðàâåíñòâ äëÿ ñïèñêîâ â ôîðìóëå � èìååòñÿ ðàâåíñòâî g L� , òî êâàíòîð ïî ïå-
ðåìåííîé �( )g ýëèìèíèðóåòñÿ ïîñëå ïîäñòàíîâêè àáñòðàêòíîãî ñïèñêà L âìåñòî
âñåõ âõîæäåíèé ïåðåìåííîé �( )g è ýëèìèíàöèè êîíêàòåíàöèè.
Îòîæäåñòâëåíèå àòðèáóòíûõ òåðìîâ. Ïîÿâëåíèå àòðèáóòíûõ òåðìîâ àðíî-
ñòè áîëüøå íóëÿ ïðèâîäèò ê íåîáõîäèìîñòè îòîæäåñòâëåíèé: åñëè u v� , òî
f u f v( ) ( )� (ïîäñòàíîâî÷íîñòü ðàâåíñòâà). Äëÿ òîãî ÷òîáû îïèñàòü âñå âîçìîæíûå
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 9
ñïîñîáû îòîæäåñòâëåíèé, êîòîðûå ñëåäóåò ó÷èòûâàòü ïðè ïîñòðîåíèè ïðåäèêàòíî-
ãî òðàíñôîðìåðà â îáùåì ñëó÷àå, ïðîèíäåêñèðóåì âñå àòðèáóòíûå âûðàæåíèÿ, êî-
òîðûå âõîäÿò â ïîñòóñëîâèå è ñèìâîëüíîå ñîñòîÿíèå, ìíîæåñòâîì èíäåêñîâ I. Åñëè
àòðèáóòíîå âûðàæåíèå f u( ) èìååò èíäåêñ k, òî åãî àòðèáóòíûé ñèìâîë f îáîçíà÷èì
÷åðåç fk , à ñïèñîê àðãóìåíòîâ u — ÷åðåç u k( ) . Òàêèì îáðàçîì, k-é àòðèáóòíûé
ñèìâîë â ýòîé èíäåêñàöèè èìååò âèä f uk
k( )( ) . Ïóñòü Q r g s� � �{ } { } { }. Ðàññìîò-
ðèì ìíîæåñòâî
M f u f v k I f u f vk
k
k
k
k
k
k
k� �
{ { }}( ) ( )| , ( ) , ( )( ) ( ) ( ) ( )
Q z ,
ñîñòîÿùåå èç âñåõ ðàâåíñòâ àòðèáóòíûõ âûðàæåíèé, êîòîðûå ìîãóò ïîÿâèòüñÿ â
ðåçóëüòàòå îòîæäåñòâëåíèÿ àðãóìåíòîâ àòðèáóòíûõ âûðàæåíèé èç ìíîæåñòâà {z}
ñ àðãóìåíòàìè àòðèáóòíûõ âûðàæåíèé èç ìíîæåñòâà Q. Åñëè àðãóìåíòû àòðèáóò-
íîãî âûðàæåíèÿ èç {z} íå îòîæäåñòâëÿþòñÿ ñ àðãóìåíòàìè àòðèáóòíûõ âûðàæå-
íèé èç Q, òî àòðèáóòíîå âûðàæåíèå èç {z} íå ìåíÿåò ñâîåãî çíà÷åíèÿ â ðåçóëü-
òàòå ïðèìåíåíèÿ òðàíñôîðìåðà. Åñëè æå èìååò ìåñòî îòîæäåñòâëåíèå
u vk k( ) ( )� , èç êîòîðîãî ñëåäóåò f u f vk
k
k
k( ) ( )( ) ( )� , òî àòðèáóòíîå âûðàæåíèå
f vk
k( )( ) â ôîðìóëå äëÿ ïðåäèêàòíîãî òðàíñôîðìåðà ñëåäóåò çàìåíèòü íà ïåðå-
ìåííóþ, ñîîòâåòñòâóþùóþ àòðèáóòíîìó âûðàæåíèþ f uk
k( )( ) .
×òîáû ïîëó÷èòü ôîðìàëüíîå îïðåäåëåíèå ýòîé ïðîöåäóðû, ïåðåíóìåðóåì âñå
ïîäìíîæåñòâà J J I ii i, , , , ...� � 1 2 , ìíîæåñòâà I, âêëþ÷àÿ ïóñòîå ìíîæåñòâî, è
ïóñòü ïðè ýòîì
N f u f v k J J I ii k
k
k
k
i i� �
� �{ }( ) ( )| , , , , ...( ) ( ) 1 2 .
Îáîçíà÷èì
E u v u vi
k J
k k
k I J
k k
i i
� � �
( ) ( )( ) ( )
\
( ) ( ) .
Êàæäàÿ ôîðìóëà îïðåäåëÿåò îäèí èç âîçìîæíûõ ñïîñîáîâ îòîæäåñòâëåíèÿ.
Ïóñòü òåïåðü i i i� ( , ,... )1 2 , ãäå �ij k
kf u� ( ( ))( ) , åñëè z f vj k
k� ( )( ) , k J i
,
à ij jz� â ïðîòèâíîì ñëó÷àå. Îïðåäåëèì ñèìâîëüíóþ ïîäñòàíîâêó �i òàêèì
îáðàçîì, ÷òî íà ìíîæåñòâå Q îíà äåéñòâóåò êàê � , à � i i( )z � . Òåïåðü ìîæíî
îïðåäåëèòü îáùóþ ôîðìóëó äëÿ ïðåäèêàòíîãî òðàíñôîðìåðà
pt( , )� � � � �q q1 2 � ,
q , , R U E Ci i i i i� � � � � � ( )( )x w y � ,
ãäå � �� � �i i ( ) , � � �R out ti i i( ( , ) ( ))� �r , � � �U out p hi i i i( ( , ) ( ( ), ( )))� � �g g ,
� �E Ei i i� ( ) .
Êâàíòîðû ïî ïåðåìåííûì òèïà î÷åðåäè ýëèìèíèðóþòñÿ òàê æå, êàê è â ñëó÷àå
ïðîñòûõ àòðèáóòîâ. Îäíàêî â ðåçóëüòàòå îòîæäåñòâëåíèé ìîãóò ïîÿâèòüñÿ ðàâåí-
ñòâà äâóõ àáñòðàêòíûõ î÷åðåäåé. Òàêèå ðàâåíñòâà ýëèìèíèðóþòñÿ àíàëîãè÷íî ïî-
êàçàííûì âûøå. Ïåðåä âûïîëíåíèåì ýòèõ ïðåîáðàçîâàíèé êâàíòîðû â ôîðìóëå �
äîëæíû áûòü âûíåñåíû â íà÷àëî ôîðìóëû.
Íåêîòîðûå èç ôîðìóë q q1 2, ,... ìîãóò áûòü íåâûïîëíèìû, à çíà÷èò, îíè íå ïî-
êðûâàþò íè îäíîãî êîíêðåòíîãî ñîñòîÿíèÿ. Åñëè âñå ôîðìóëû íåâûïîëíèìû, òî
ïåðåõîä íå îïðåäåëåí. Ñëåäîâàòåëüíî, âñå êîíêðåòíûå ñîñòîÿíèÿ, êîòîðûå ïîêðû-
âàþòñÿ ôîðìóëîé � , ÿâëÿþòñÿ òóïèêîâûìè.
ÑÂÎÉÑÒÂÀ ÏÐÅÄÈÊÀÒÍÎÃÎ ÒÐÀÍÑÔÎÐÌÅÐÀ
Çàäà÷à ñèìâîëüíîãî ìîäåëèðîâàíèÿ ñîñòîèò â èññëåäîâàíèè ñâîéñòâà êîíêðåò-
íûõ ñèñòåì íà èõ ñèìâîëüíûõ ìîäåëÿõ. Ìåæäó ñîñòîÿíèÿìè ñèìâîëüíûõ è êîí-
êðåòíûõ ñèñòåì îïðåäåëåíî îòíîøåíèå � �|� , êîòîðîå áóäåì ðàññìàòðèâàòü êàê
îòíîøåíèå ïîêðûòèÿ: ñèìâîëüíîå ñîñòîÿíèå � «ïîêðûâàåò» ñîñòîÿíèå � êîíêðåò-
10 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
íîé ñèñòåìû. Äëÿ òîãî ÷òîáû ìîäåëèðîâàíèå áûëî êîððåêòíûì, ïåðåõîäû êîíê-
ðåòíîé ñèñòåìû äîëæíû òàêæå «ïîêðûâàòüñÿ» ïåðåõîäàìè ñèìâîëüíîé ñèñòåìû:
åñëè � �
�
�
� â êîíêðåòíîé ñèñòåìå è � �|� , òî � �� � �| ( , )pt . ×òîáû óñëîâèå
pt( , )� � áûëî ñèëüíåéøèì ïîñòóñëîâèåì äëÿ ïðåäóñëîâèÿ � è îïåðàòîðà � , íåîá-
õîäèìî âûïîëíåíèå îáðàòíîãî óñëîâèÿ: åñëè � � �� �| ( , )pt è � �
�
�
�, òî � �|� .
Ââåäåì ñëåäóþùèå îáîçíà÷åíèÿ:
State { }( ) | |� � � ��
�CE ,
Nstate {( , ) | ( )S S� � �� � �
( )� �
�
�
� } , S CE� .
Òåïåðü îñíîâíîå ñâîéñòâî ïðåäèêàòíîãî òðàíñôîðìåðà, îïðåäåëåííîãî â ïðåä-
ûäóùåì ðàçäåëå, ìîæåò áûòü ñôîðìóëèðîâàíî â âèäå ñëåäóþùåé òåîðåìû.
Òåîðåìà 1. Äëÿ ïðåäèêàòíîãî òðàíôîðìåðà pt âûïîëíÿåòñÿ State (pt( , ))� � �
� Nstate State( ( ), )� � .
Ýêâèâàëåíòíàÿ ôîðìóëèðîâêà ýòîé òåîðåìû:
� � � � � � � � �
�
� � � �
�
�
� �
| ( , ) ( )( | ),pt C CE E .
Çäåñü âûðàæåíî íåîáõîäèìîå è äîñòàòî÷íîå óñëîâèå ïîêðûòèÿ êîíêðåòíîãî ñî-
ñòîÿíèÿ �� ñîñòîÿíèåì pt( , )� � .
Äîñòàòî÷íîñòü. Äîêàæåì, ÷òî � � � � � � �
�
| | ( , )�
�
� � � � pt . Ïðåäïîëî-
æèì, ÷òî ïîñûëêà èñòèííà. Èìååì
pt( , )� � � � �q q1 2 �
Ïóñòü N f u f v M u v� �
� � �{ }( ( ) ( )) | ( ) ( )� � , à J k f u f v Nk
k
k
k� �
{ }|( ( ) ( ))( ) ( ) .
Ïîñêîëüêó J i , i � 1 2, , ... , ïðîáåãàåò âñå ïîäìíîæåñòâà ìíîæåñòâà M, òî íàéäåòñÿ òà-
êîå i, ÷òî J Ji � , N Ni � . Ïîêàæåì, ÷òî �� � �| qi � � � � � ( ) ( )x,w, y � i i i iR U E C .
Èìååì �� �| C ïî îïðåäåëåíèþ îïåðàòîðà � . Äëÿ äîêàçàòåëüñòâà èñòèííîñòè ïåð-
âîãî êîíúþíêòèâíîãî ÷ëåíà íåîáõîäèìî íàéòè òàêèå çíà÷åíèÿ ïåðåìåííûõ x, w
è y, äëÿ êîòîðûõ ïîäêâàíòîðíàÿ ôîðìóëà èñòèííà. Ïîëîæèì x r� �� ( ) ,
w g� �� ( ) , y s� �� ( ) . Ñîîòâåòñòâóþùóþ ïîäñòàíîâêó îáîçíà÷èì
. Ïîêàæåì,
÷òî
�
�
�
� � � � � � � � � � �| ( ) ( ) ( ) ( ) ( )i i i i i i i iR U E R U E .
Âíà÷àëå äîêàæåì, ÷òî �� �| Ei . Äëÿ ýòîãî âû÷èñëèì
�( ) ( ( ))� � �E Ei i i � i iE( ) ,
ãäå ÷åðåç � i îáîçíà÷åíà êîìïîçèöèÿ ïîäñòàíîâîê �i è
. Èìååì � i ( )r �
� �� ( )r , � �i ( ) ( )s s� � , � �i i( )z � , ãäå � � �i i i� ( , ,... )1 2 , � �ij k
kf u� ( ( ))( ) , åñëè
z f vj k
k� ( )( ) , k J i
, à � �ij jz� ( ) â ïðîòèâíîì ñëó÷àå. Èç îïðåäåëåíèÿ ìíî-
æåñòâ N i è J i íåïîñðåäñòâåííî ñëåäóåò � �i i iE E( ) ( )� � è �� �| Ei . Èç ýòîãî ñî-
îòíîøåíèÿ è ñêàçàííîãî âûøå âûòåêàåò �
� � �| ( )Ei . Äîêàæåì ëåììó.
Ëåììà 1. Äëÿ ëþáîãî òåðìà t TE
èìååò ìåñòî � � � �� � � � � � �| | ( ) ( )E t ti i .
Äåéñòâèòåëüíî, åñëè t — àòðèáóòíîå âûðàæåíèå è t
Q , òî � �i t t( ) ( )� � , åñëè
æå t
{ }z è t z f v k Jj k
k
i� �
( ),( ) , òî � �i k
kt f u( ) ( ( ))( )� . Îäíàêî èç ïîñûëêè
ëåììû ñëåäóåò, ÷òî � � �� � � � �( ( )) ( ( )) ( )( ) ( )f u f v tk
k
k
k è, çíà÷èò, � � �� � � �| ( ) ( )i t t .
Åñëè æå t f vk
k� ( )( ) è k J i� , òî èç òîé æå ïîñûëêè ñëåäóåò, ÷òî � �i t t( ) ( )� � . Òà-
êèì îáðàçîì, ëåììà èìååò ìåñòî äëÿ àòðèáóòíûõ âûðàæåíèé è ñòàíäàðòíûì îáðà-
çîì (èíäóêöèåé ïî ñòðóêòóðå âûðàæåíèÿ) ðàñïðîñòðàíÿåòñÿ íà âñå òåðìû.
Ñëåäñòâèå. Äëÿ ëþáîé ôîðìóëû F èìååò ìåñòî � � � �� � � � � � �| | ( ) ( )E F Fi i .
Ýòî î÷åâèäíî. Àíàëîãè÷íî ñòðóêòóðíîé èíäóêöèåé äîêàçûâàåòñÿ ëåììà 2.
Ëåììà 2. Âûïîëíÿåòñÿ � � � � �� � � � � � � �| | ( , ) ( , ), ( , )E out out outi i ir r g
� �out ( , )� g .
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 11
Òåïåðü íå ðàññìîòðåííûå ôðàãìåíòû �
� �
�
� � � � � � � � �| ), | ), | )i i iR u óòâåð-
æäåíèÿ î äîñòàòî÷íîñòè óñëîâèÿ òåîðåìû ñëåäóþò èç îïðåäåëåíèÿ îòíîøåíèÿ ïå-
ðåõîäîâ êîíêðåòíîé ìîäåëè.
Íåîáõîäèìîñòü. Äîêàæåì, ÷òî � � � � � � � �
�
� � � �
�
�
�| ( , ) ( )( | )pt CE .
Ïóñòü èñòèííà ïîñûëêà. Ïîñòðîèì � òàêîå, ÷òî ( | )� � � �
�
�
�
� . Äëÿ ýòîãî
âûáåðåì i òàêîå, ÷òî � �� � � � � � � � | ( , )( )q R U E Ci i i i ix y . Îòñþäà ñëåäó-
å ò ñ ó ù å ñ ò â î â à í è å ñ ï è ñ ê î â ê î í ñ ò à í ò c è d ò à ê è õ , ÷ ò î �� �|
| ( )� � � � �
� i i i iR U E , ãäå
( )x c� ,
( )y d� . Ïîëîæèì �( )r c� , �( )s d� ,
� �( )z � i , ãäå � � �i i i� ( , , ... )1 2 , � �ij k
kf u� ( ( ))( ) , åñëè z f vj k
k� ( )( ) è k J i
, à
� �ij jz� � ( ) â ïðîòèâíîì ñëó÷àå. ×åðåç � i , êàê è ðàíåå, îáîçíà÷èì êîìïîçèöèþ
ïîäñòàíîâîê �i è
. Äëÿ ñîñòîÿíèÿ � ñïðàâåäëèâû àíàëîãè ëåìì 1 è 2. Èìååì
� � �i i i iE E E( ) ( ) |� � � � �1 . Èñïîëüçóÿ ëåììó 1, ïîëó÷àåì � �|� . Äîêàæåì, ÷òî
� �
�
�
� . Äëÿ ýòîãî íåîáõîäèìî äîêàçàòü óñëîâèÿ 1–5 îïðåäåëåíèÿ îòíîøåíèÿ
ïåðåõîäîâ êîíêðåòíîé ìîäåëè. Óñëîâèÿ 1–2 äîêàçûâàþòñÿ ñ ïîìîùüþ ëåììû 1,
óñëîâèå 3 ñëåäóåò èç òîãî, ÷òî ïðåäèêàòíûé òðàíñôîðìåð îòëè÷åí îò íóëÿ, óñëîâèå
4 î÷åâèäíî, à óñëîâèå 5 ñëåäóåò èç îïðåäåëåíèÿ âåêòîðà � .
ÏÐÈÌÅÍÅÍÈß ÏÐÅÄÈÊÀÒÍÎÃÎ ÒÐÀÍÑÔÎÐÌÅÐÀ
Îäíî èç ïðèìåíåíèé ïðåäèêàòíîãî òðàíñôîðìåðà çàêëþ÷àåòñÿ â ïîñòðîåíèè
òðàíçèöèîííîé ñèñòåìû äëÿ áàçîâûõ ïðîòîêîëîâ.
Ðàññìîòðèì ñïåöèôèêàöèþ � � � �B E, ñèñòåìû, ñîñòîÿùóþ èç ìíîæåñòâà áà-
çîâûõ ïðîòîêîëîâ B è îïèñàíèÿ ñðåäû E. Ïóñòü b B
— áàçîâûé ïðîòîêîë
è b x r x P r x r x� � � � �( ( , ) ( , ) ( , ))� � . Ïðîòîêîë b p r p P r p r p( ) ( , ) ( , ) ( , )� � � �� � ,
ãäå p p p� ( , ,... )1 2 — íàáîð çíà÷åíèé ïàðàìåòðîâ x x x� ( , ,... )1 2 , ñîãëàñîâàííûé
ñ èõ òèïàìè, íàçûâàåòñÿ êîíêðåòèçàöèåé ïðîòîêîëà b. Ñîñòîÿíèÿìè êîíêðåòíîé ñèñ-
òåìû C� ÿâëÿþòñÿ ýëåìåíòû ìíîæåñòâà CE , äåéñòâèÿìè — êîíêðåòèçèðîâàííûå áà-
çîâûå ïðîòîêîëû, à îòíîøåíèå ïåðåõîäîâ îïðåäåëÿåòñÿ ñëåäóþùèì îáðàçîì:
� � � � � �
�b p r p
r p
( ) ( , )
| ( , ),
�
� � �
�
�.
Ñîñòîÿíèÿìè ñèìâîëüíîé ìîäåëè C� ÿâëÿþòñÿ ýëåìåíòû ìíîæåñòâà S E , ò.å.
ôîðìóëû áàçîâîãî (ëîãè÷åñêîãî) ÿçûêà ñèñòåìû VRS. Êîíêðåòèçàöèÿ ïðîòîêîëà
äëÿ ñèìâîëüíîé ìîäåëè íå òðåáóåò çàäàíèÿ êîíêðåòíûõ çíà÷åíèé ïàðàìåòðîâ ïðî-
òîêîëà. Îíè äîáàâëÿþòñÿ ê îïèñàíèþ ñðåäû êàê ïðîñòûå åå àòðèáóòû, à ïîñëå ïðè-
ìåíåíèÿ ïðîòîêîëà ïðåîáðàçóþòñÿ â ïåðåìåííûå, ñâÿçàííûå êâàíòîðîì ñóùåñòâî-
âàíèÿ. Îòíîøåíèå ïåðåõîäîâ ñèìâîëüíîé ìîäåëè îïðåäåëÿåòñÿ ñëåäóþùèì îáðà-
çîì. Âíà÷àëå îïðåäåëÿåòñÿ òèï ñèìâîëüíîé ìîäåëè: óíèâåðñàëüíàÿ èëè
ýêçèñòåíöèàëüíàÿ (â ðàáîòå [5] èñïîëüçîâàëèñü òåðìèíû «ïðÿìàÿ» è «èíâåðñíàÿ»).
Ýòè ìîäåëè îòëè÷àþòñÿ ñïîñîáîì ïðèìåíèìîñòè áàçîâîãî ïðîòîêîëà. Îòíîøåíèå
ïåðåõîäîâ äëÿ óíèâåðñàëüíîé ìîäåëè îïðåäåëÿåòñÿ êàê
� � � � � �
�b p r p
p r,p
( ) ( , )
| ( ) ,
�
� � � �
�
�,
à äëÿ ýêçèñòåíöèàëüíîé ìîäåëè êàê
� � � � � �
� � �
�b p r p
p r, p r p
( ) ( , )
( | ( )),
�
� � � � � �
�
�.
Óñëîâèå ïðèìåíèìîñòè äëÿ óíèâåðñàëüíîé ìîäåëè ýêâèâàëåíòíî îáùåçíà÷èìîñòè
èìïëèêàöèè � �� ( , )r p . Ïðèìåíèìîå ïðåäóñëîâèå ïîêðûâàåò âñå êîíêðåòíûå ñîñòîÿ-
íèÿ, êîòîðûå ïîêðûâàþòñÿ ñîñòîÿíèåì � . Äëÿ ýêçèñòåíöèàëüíîé ìîäåëè óñëîâèå ïðèìå-
íèìîñòè ýêâèâàëåíòíî âûïîëíèìîñòè êîíúþíêöèè � � ( , )r p . Ïåðåñå÷åíèå ìíîæåñòâ
ñîñòîÿíèé, ïîêðûòûõ ïðèìåíèìûì ïðåäóñëîâèåì è ñîñòîÿíèåì �, íå ïóñòî.
Áàçîâûå ïðîòîêîëû ñèñòåìû VRS. Ñðåäà â ñèñòåìå ïðåäñòàâëÿåòñÿ â âèäå
êîìïîçèöèè ÿäðà ñðåäû è ñèñòåìû àãåíòîâ, ïîãðóæåííûõ â ñðåäó. Ôîðìàëüíî ñî-
12 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
ñòîÿíèå òàêîé ñðåäû ìîæíî ïðåäñòàâèòü â âèäå s m u m u[ : , : ,... ]1 1 2 2 , ãäå ÿäðî ñî-
ñòîÿíèÿ ñðåäû s åñòü îòîáðàæåíèå ìíîæåñòâà êîíñòàíòíûõ àòðèáóòíûõ âûðàæåíèé
â èõ çíà÷åíèÿ äëÿ êîíêðåòíûõ ìîäåëåé èëè ôîðìóë áàçîâîãî ÿçûêà äëÿ ñèìâîëüíûõ
ìîäåëåé. Âûðàæåíèÿ u u1 2, ,... ïðåäñòàâëÿþò ñîñòîÿíèÿ àãåíòîâ, m m1 2, ,... — èõ
èìåíà. È òî, è äðóãîå îòíîñèòåëüíî áàçîâîãî ÿçûêà — ýòî ñèìâîëüíûå âûðàæåíèÿ,
à àãåíòíàÿ êîìïîíåíòà [ : , : ,... ]m u m u1 1 2 2 ñîñòîÿíèÿ ñðåäû ðàññìàòðèâàåòñÿ êàê çíà-
÷åíèå àòðèáóòà state òèïà ñèìâîëüíîé ôóíêöèè èç èìåí àãåíòîâ â èõ ñîñòîÿíèÿ. Ýòè
ñîñòîÿíèÿ îòîæäåñòâëÿþòñÿ ñ ïîâåäåíèÿìè àãåíòîâ (âûðàæåíèÿìè â àëãåáðå ïîâå-
äåíèé) ëèáî ñèìâîëüíûìè çíà÷åíèÿìè àòðèáóòà state, êîòîðûé âû÷èñëÿåòñÿ îïåðà-
òîðàìè ïîñòóñëîâèé áàçîâûõ ïðîòîêîëîâ. Áàçîâûå ïðîòîêîëû îïðåäåëÿþò ôóíê-
öèþ ïîãðóæåíèÿ è îòíîøåíèå ïåðåõîäîâ íà ìíîæåñòâå ñîñòîÿíèé ñðåäû.
Ñèñòåìà VRS ïîçâîëÿåò ðàáîòàòü êàê ñ êîíêðåòíûìè, òàê è ñ ñèìâîëüíûìè ìîäå-
ëÿìè. Âåðèôèêàöèþ êîíêðåòíûõ ìîäåëåé ïîääåðæèâàåò ãåíåðàòîð òðàññ CTG
(Concrete State Generator), à âåðèôèêàöèþ ñèìâîëüíûõ ìîäåëåé — ãåíåðàòîð ñèìâîëü-
íûõ òðàññ STG (Symbolic Trace Generator). Îñíîâíîå îòëè÷èå êîíêðåòíûõ ìîäåëåé îò
ñèìâîëüíûõ ñîñòîèò â äåòåðìèíèðîâàííîì ïîâåäåíèè. Ýòî îçíà÷àåò, ÷òî ïîñëå âûáîðà
áàçîâîãî ïðîòîêîëà (êîòîðûé ìîæåò áûòü íåäåòåðìèíèðîâàííûì) ïðåîáðàçîâàíèå ñî-
ñòîÿíèÿ ñðåäû äîëæíî îïðåäåëÿòüñÿ îäíîçíà÷íî. Ïîýòîìó â êîíêðåòíûõ ìîäåëÿõ çà-
ïðåùàåòñÿ èñïîëüçîâàòü ïðåäèêàòíûå ôîðìóëû â ïîñòóñëîâèÿõ. Òàêèå ïîñòóñëîâèÿ ñî-
ñòîÿò òîëüêî èç îïåðàòîðîâ ïðèñâàèâàíèÿ è îïåðàòîðîâ îáíîâëåíèÿ î÷åðåäåé.
Îáà òðàññîâûõ ãåíåðàòîðà îñóùåñòâëÿþò ãåíåðàöèþ è èññëåäîâàíèå òðàññ â
ïðîñòðàíñòâå ñîñòîÿíèé ìîäåëè, îäíîâðåìåííî ïðîâåðÿÿ öåëîñòíîñòü è áåçîïàñ-
íîñòü ìîäåëè (safety conditions) è îñóùåñòâëÿÿ ïîèñê öåëåâûõ ñîñòîÿíèé (ïðîâåðêà
äîñòèæèìîñòè). Òðàññîâûå ãåíåðàòîðû òàêæå îïðåäåëÿþò âîçìîæíîñòü òóïèêîâûõ
ñîñòîÿíèé è íåäåòåðìèíèçìà, âîçíèêàþùåãî ïðè âûáîðå îäíîãî èç íåñêîëüêèõ
áàçîâûõ ïðîòîêîëîâ.
Óïðàâëåíèå ãåíåðàöèåé òðàññ îñóùåñòâëÿåòñÿ îáùèì ãåíåðèðóþùèì ìåõàíèç-
ìîì (generating engine), êîòîðûé èñïîëüçóåò è èçìåíÿåò àòðèáóò state, îñóùåñòâëÿåò
âûáîð áàçîâîãî ïðîòîêîëà è àãåíòîâ, êîòîðûå ìîãóò áûòü çàäåéñòâîâàíû â åãî ïðèìå-
íåíèè. Ñàì àòðèáóò state ñêðûò îò áàçîâûõ ïðîòîêîëîâ, êîòîðûì äîñòóïíî ëèøü îïðå-
äåëåíèå â ïðåäóñëîâèè ñîñòîÿíèÿ, ãäå ìîæåò íàõîäèòüñÿ îäèí èç ó÷àñòíèêîâ áàçîâîãî
ïðîòîêîëà (êëþ÷åâîé àãåíò).  ïîñòóñëîâèè áàçîâîãî ïðîòîêîëà ìîæåò ïðèñóòñòâîâàòü
îïåðàòîð èçìåíåíèÿ ñîñòîÿíèÿ êëþ÷åâîãî àãåíòà. Èìÿ êëþ÷åâîãî àãåíòà, êàê ïðàâèëî,
ÿâëÿåòñÿ îäíèì èç ïàðàìåòðîâ ïðîòîêîëà, çíà÷åíèå êîòîðîãî îïðåäåëÿåòñÿ ãåíåðèðóþ-
ùèì ìåõàíèçìîì. Ãåíåðèðóþùèé ìåõàíèçì îáëàäàåò ðÿäîì ðàçëè÷íûõ ìåòîäîâ è ýâ-
ðèñòèê äëÿ ñîêðàùåíèÿ ïðîñòðàíñòâà ïîèñêà è îòáðàñûâàíèÿ òåõ íàïðàâëåíèé, ãäå íå
îæèäàåòñÿ íàðóøåíèé èññëåäóåìûõ óñëîâèé.
Àáñòðàêöèè. Âñëåäñòâèå äåòåðìèíèðîâàííîñòè êîíêðåòíîãî òðàññîâîãî ãåíå-
ðàòîðà íåäåòåðìèíèçì âíåøíèõ âîçäåéñòâèé íà ñèñòåìó ìîæåò áûòü ïðîìîäåëèðî-
âàí òîëüêî íåäåòåðìèíèçìîì âûáîðà áàçîâûõ ïðîòîêîëîâ. Íåêîòîðûå èç íèõ ìîãóò
ïðåäíàçíà÷àòüñÿ äëÿ ïðåäñòàâëåíèÿ ìîäåëè âíåøíåé ñðåäû.  ñèìâîëüíûõ ìîäåëÿõ
òàêîé íåäåòåðìèíèçì ìîäåëèðóåòñÿ áîëåå ïðîñòî. Îí ìîæåò áûòü ïðåäñòàâëåí àò-
ðèáóòàìè, íå èìåþùèìè êîíêðåòíûõ çíà÷åíèé, íî óäîâëåòâîðÿþùèìè îïðåäåëåí-
íûì îãðàíè÷åíèÿì. Èíà÷å ãîâîðÿ, ñèìâîëüíàÿ ìîäåëü ïðåäñòàâëÿåò ñîáîé àáñòðàê-
öèþ íåêîòîðîãî êëàññà êîíêðåòíûõ ìîäåëåé è ìîæåò áûòü ïîëó÷åíà ñëåäóþùèì
îáðàçîì. Ðàññìîòðèì êîíêðåòíóþ ìîäåëü è â êà÷åñòâå íà÷àëüíîãî ñîñòîÿíèÿ
îïðåäåëèì ôîðìóëó, êîòîðàÿ ïîêðûâàåò íåêîòîðûé êëàññ êîíêðåòíûõ ñîñòîÿíèé.
Ìîäåëèðóÿ ñèñòåìó èç ýòèõ íà÷àëüíûõ ñîñòîÿíèé, ïîëó÷àåì ïîêðûòèå öåëîãî êëàñ-
ñà êîíêðåòíûõ òðàññ. Äðóãèå ôîðìû àáñòðàêöèè ìîæíî ïîëó÷èòü, ìîäèôèöèðóÿ áà-
çîâûå ïðîòîêîëû, íàïðèìåð çàìåíÿÿ â ïîñòóñëîâèÿõ êîíêðåòíûå îïåðàòîðû ïðè-
ñâàèâàíèé èëè ìîäèôèêàöèè î÷åðåäåé ôîðìóëàìè, îãðàíè÷èâàþùèìè âîçìîæíûå
ïðîèçâîëüíûå èçìåíåíèÿ àòðèáóòîâ. Ðàçëè÷íîãî ðîäà àáñòðàêöèè øèðîêî ïðèìåíÿ-
þòñÿ â ñîâðåìåííûõ ñèñòåìàõ âåðèôèêàöèè [15–18]. Òå èç íèõ, êîòîðûå ñâÿçàíû ñ
îáùåé òåîðèåé áàçîâûõ ïðîòîêîëîâ, èññëåäîâàíû â [4, 5].
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 13
Ñòàòè÷åñêàÿ âåðèôèêàöèÿ.  íåêîòîðûõ ñëó÷àÿõ âåðèôèêàöèþ ìîäåëè ìîæ-
íî îñóùåñòâèòü áåç ÿâíîãî ïîðîæäåíèÿ òðàññ, èññëåäóÿ ëèøü âçàèìîîòíîøåíèÿ
ìåæäó óñëîâèÿìè âåðèôèêàöèè è áàçîâûìè ïðîòîêîëàìè.  ÷àñòíîñòè, ïðèìåíÿÿ
áàçîâûå ïðîòîêîëû ê çàäàííûì óñëîâèÿì, ìîæíî ïðîâåðÿòü èíâàðèàíòíîñòü ýòèõ
óñëîâèé. Ñòàòè÷åñêè ìîæíî òàêæå äîêàçûâàòü äåòåðìèíèðîâàííîñòü ïîâåäåíèÿ
ñèñòåìû è îòñóòñòâèå òóïèêîâ.
Ñèñòåìà, îïèñàííàÿ â ÿçûêå áàçîâûõ ïðîòîêîëîâ ñèñòåìû VRS, âêëþ÷àåò àãåí-
òû, ðàáîòàþùèå ïàðàëëåëüíî è àñèíõðîííî, à êàæäûé áàçîâûé ïðîòîêîë äîïóñêàåò
èçìåíåíèå ñîñòîÿíèÿ (àòðèáóòà state) òîëüêî îäíîãî àãåíòà (íàçûâàåìîãî êëþ÷åâûì
äëÿ ýòîãî ïðîòîêîëà). Ïîýòîìó ïðàêòè÷åñêóþ öåííîñòü èìååò ïîèñê
íåäåòåðìèíèðîâàííîãî ïîâåäåíèÿ äëÿ êàæäîãî àãåíòà îòäåëüíî.
Ñîñòîÿíèå s êàêîãî-ëèáî àãåíòà à íàçûâàåòñÿ íåäåòåðìèíèðîâàííûì, åñëè èç
íåãî ñóùåñòâóåò áîëåå îäíîãî ïåðåõîäà, ò.å. ïðèìåíèìî áîëåå îäíîãî ïðîòîêîëà ñ
êëþ÷åâûì àãåíòîì à. Ââåäåì ïîíÿòèå íåïðîòèâîðå÷èâîñòè äëÿ ñèñòåì áàçîâûõ
ïðîòîêîëîâ. Îíî îïðåäåëÿåòñÿ îòñóòñòâèåì ïåðåñå÷åíèé ïðåäóñëîâèé áàçîâûõ ïðî-
òîêîëîâ äëÿ îäíîãî êëþ÷åâîãî àãåíòà. Ïóñòü �( , , )a x r è �� ( , , )a y r — ïðåäóñëîâèÿ
äâóõ ðàçëè÷íûõ áàçîâûõ ïðîòîêîëîâ b è b� ñ êëþ÷åâûìè àãåíòàìè îäíîãî è òîãî æå
òèïà, êîíêðåòèçèðîâàííûå îäíèì è òåì æå èìåíåì êëþ÷åâîãî àãåíòà (â ñëó÷àå,
åñëè ýòî èìÿ ÿâëÿåòñÿ ïàðàìåòðîì), x è y — ñïèñêè ïàðàìåòðîâ, r — ñïèñîê àòðè-
áóòíûõ âûðàæåíèé. Ïðîòîêîëû b è b� íåïðîòèâîðå÷èâû, åñëè ôîðìóëà
� � � �( ( , , ) ( , , ))x a x r y a y r� �
òîæäåñòâåííî èñòèííà (îòðèöàíèå íåâûïîëíèìî). Ñèñòåìà áàçîâûõ ïðîòîêîëîâ
íàçûâàåòñÿ íåïðîòèâîðå÷èâîé, åñëè ëþáàÿ ïàðà ïðîòîêîëîâ ñ îäíîòèïíûìè êëþ-
÷åâûìè àãåíòàìè íåïðîòèâîðå÷èâà. Äëÿ ðàñïîçíàâàíèÿ íåïðîòèâîðå÷èâîñòè ñèñ-
òåìû áàçîâûõ ïðîòîêîëîâ â ñðåäå, èìåþùåé n òèïîâ àãåíòîâ, ïîâåäåíèå êàæäîãî
èç êîòîðûõ îïèñàíî ki (i n� �, ,1 ) áàçîâûìè ïðîòîêîëàìè, òðåáóåò C
k
i n
i
2
1�
�
, ,�ïðîâåðîê íåïðîòèâîðå÷èâîñòè ïàð ïðîòîêîëîâ.
Åñëè ñèñòåìà áàçîâûõ ïðîòîêîëîâ íåïðîòèâîðå÷èâà, òî â êàæäîì ñîñòîÿíèè
ñóùåñòâóåò íå áîëåå îäíîãî ïðèìåíèìîãî áàçîâîãî ïðîòîêîëà, à ñëåäîâàòåëüíî, âñå
àãåíòû òàêîé ñèñòåìû èìåþò äåòåðìèíèðîâàííîå ïîâåäåíèå. Ìíîãîàãåíòíàÿ ñèñòå-
ìà áàçîâûõ ïðîòîêîëîâ, êàê ïðàâèëî, èìååò ñîñòîÿíèÿ, èç êîòîðûõ âîçìîæíû íå-
ñêîëüêî ïåðåõîäîâ ïîä äåéñòâèÿìè ðàçíûõ ïðîòîêîëîâ. Îäíàêî ïðè äîêàçàííîì
ñâîéñòâå íåïðîòèâîðå÷èâîñòè âñå òàêèå ïåðåõîäû îñóùåñòâëÿþòñÿ ðàçíûìè àãåí-
òàìè.  ýòîì ñëó÷àå äàííûå ñîñòîÿíèÿ íå ÿâëÿþòñÿ íåäåòåðìèíèðîâàííûìè, à íà-
ëè÷èå ìíîæåñòâà âîçìîæíûõ ïåðåõîäîâ âûçâàíî ïåðåñòàíîâî÷íîñòüþ (interleaving)
ïàðàëëåëüíî âûïîëíÿåìûõ áàçîâûõ ïðîòîêîëîâ.
Ïîìèìî óñëîâèÿ äåòåðìèíèçìà, êðèòè÷åñêèì òðåáîâàíèåì ê ìîäåëèðóåìîé
ñèñòåìå ÿâëÿåòñÿ îòñóòñòâèå òóïèêîâ. Ââåäåì ïîíÿòèå ïîëíîòû äëÿ ñèñòåì áàçîâûõ
ïðîòîêîëîâ. Îíî îïðåäåëÿåòñÿ ñëåäóþùèì óñëîâèåì: äèçúþíêöèÿ ïðåäóñëîâèé
âñåõ áàçîâûõ ïðîòîêîëîâ (òî÷íåå, óñëîâèé ïðèìåíèìîñòè)
� � � �x x r x x r1 1 1 1 2 2 2 2� �( , ) ( , ) �
äîëæíà áûòü òîæäåñòâåííî èñòèííîé (îòðèöàíèå íåâûïîëíèìî). Çäåñü
� i i ix r( , ) — ïðåäóñëîâèå áàçîâîãî ïðîòîêîëà, êîòîðûé ïàðàìåòðèçèðîâàí ñïèñ-
êîì ïåðåìåííûõ xi è èñïîëüçóåò ñïèñîê ri àòðèáóòíûõ âûðàæåíèé. Â íåêîòîðûõ
ðåàëèçàöèÿõ ïîëüçîâàòåëþ ïðåäîñòàâëÿåòñÿ âîçìîæíîñòü ñôîðìóëèðîâàòü ñâîè
îãðàíè÷åíèÿ âî èçáåæàíèå ëîæíûõ îòðèöàòåëüíûõ ðåçóëüòàòîâ. Ïîëíîòà ñ ó÷å-
òîì ïîëüçîâàòåëüñêèõ îãðàíè÷åíèé îïðåäåëÿåòñÿ ôîðìóëîé
R r x x r x x r( ) ( , ) ( , )� � � � �1 1 1 1 2 2 2 2� � � ,
ãäå R — ôîðìóëà áàçîâîãî ÿçûêà, çàäàþùàÿ ïîëüçîâàòåëüñêèå îãðàíè÷åíèÿ.
14 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
Åñëè âûïîëíÿåòñÿ óñëîâèå ïîëíîòû è â ëþáîé ìîìåíò âðåìåíè äëÿ êàæäîãî
òèïà àãåíòîâ â ñèñòåìå ñóùåñòâóåò õîòÿ áû îäèí àãåíò, òî â êàæäîì ñîñòîÿíèè ñèñ-
òåìû íàéäåòñÿ õîòÿ áû îäèí ïðèìåíèìûé ïðîòîêîë. Òàêèì îáðàçîì, â ïîëíîé ñèñ-
òåìå îòñóòñòâóþò òóïèêè.
Äëÿ ìíîãîàãåíòíûõ ñèñòåì, â êîòîðûõ çàäàíî ðàçáèåíèå áàçîâûõ ïðîòîêîëîâ ïî
òèïàì êëþ÷åâûõ àãåíòîâ, ìîæíî ñíà÷àëà ïðîâåðÿòü ïîëíîòó äëÿ êàæäîãî àãåíòà (òèïà
àãåíòîâ) èíäèâèäóàëüíî, ÷òî ñóùåñòâåííî ñîêðàùàåò ðàçìåð ôîðìóë â äîêàçà-
òåëüñòâàõ. Åñëè íåïîëíîòà íàéäåíà äëÿ âñåõ òèïîâ àãåíòîâ, òî ìîæíî ïåðåéòè ê èññëå-
äîâàíèþ ïîëíîòû ñèñòåìû â öåëîì ñ ïîìîùüþ ôîðìóë, ïðåäñòàâëåííûõ âûøå. Åñëè â
ñèñòåìå ñóùåñòâóåò õîòÿ áû îäèí òèï àãåíòîâ, äëÿ êîòîðîãî äîêàçàíà ïîëíîòà, è â ñèñ-
òåìå âñåãäà åñòü ïî êðàéíåé ìåðå îäèí àãåíò äàííîãî òèïà, òî òàêàÿ ñèñòåìà íå èìååò
òóïèêîâ, òàê êàê àãåíòû ýòîãî òèïà âñåãäà ñìîãóò îñóùåñòâëÿòü ïåðåõîäû.
Êðîìå ïîëíîòû è íåïðîòèâîðå÷èâîñòè ñèñòåìû ñóùåñòâóåò ðÿä äðóãèõ ñâîéñòâ,
îáóñëîâëåííûõ òðåáîâàíèÿìè ê æèâó÷åñòè (liveness), íàäåæíîñòè, ïðîèçâîäèòåëüíîñòè
ìîäåëèðóåìîé ñèñòåìû è ò.ä. Òàêèå ñâîéñòâà ôîðìóëèðóþòñÿ äëÿ êàæäîé ñèñòåìû èí-
äèâèäóàëüíî è ïðåäñòàâëÿþòñÿ â ôîðìàëèçìå êîíêðåòíîé ìîäåëè.
Ðàññìîòðèì ñâîéñòâà, êîòîðûå ìîæíî çàïèñàòü â âèäå ôîðìóë áàçîâîãî ÿçûêà,
è ïîñòàâèì òðåáîâàíèå èñòèííîñòè ýòèõ ôîðìóë íà âñåõ ñîñòîÿíèÿõ ñèñòåìû. Íàçî-
âåì èõ óñëîâèÿìè öåëîñòíîñòè. Ïîñòðîèì àëãîðèòì ïðîâåðêè óñëîâèÿ öåëîñòíîñòè
äëÿ ñèñòåìû áàçîâûõ ïðîòîêîëîâ. Ïóñòü Q(r) — ôîðìóëà áàçîâîãî ÿçûêà, çàäàþùàÿ
óñëîâèå öåëîñòíîñòè, s r0 ( ) — ôîðìóëà áàçîâîãî ÿçûêà, õàðàêòåðèçóþùàÿ íà÷àëü-
íîå ñîñòîÿíèå ñèñòåìû (r — ñïèñîê àòðèáóòíûõ âûðàæåíèé).  ïåðâóþ î÷åðåäü, íå-
îáõîäèìî ïðîâåðèòü öåëîñòíîñòü íà÷àëüíûõ ñîñòîÿíèé ñèñòåìû: s r Q r0 ( ) ( )� . Ýòà
ôîðìóëà äîëæíà áûòü îáùåçíà÷èìîé, èíà÷å íà÷àëüíîå ñîñòîÿíèå íàðóøàåò óñëî-
âèå öåëîñòíîñòè è íåò ñìûñëà ïðîäîëæàòü ïðîâåðêè, à àëãîðèòì äîëæåí çàâåðøèòü
ðàáîòó. Äàëåå ñëåäóåò ïðîâåðèòü èíâàðèàíòíîñòü óñëîâèÿ öåëîñòíîñòè. Â ýòîì
ñëó÷àå äîñòàòî÷íî ïðîâåðèòü äëÿ êàæäîãî ïðîòîêîëà ñëåäóþùåå óñëîâèå: åñëè ïðî-
òîêîë ïðèìåíèì è óñëîâèå öåëîñòíîñòè èñòèííî, òî ïîñëå âûïîëíåíèÿ ïðîòîêîëà
îíî òàêæå áóäåò èñòèííûì. Ôîðìàëüíî ýòî óñëîâèå âûðàæàåòñÿ â âèäå
òîæäåñòâåííîé èñòèííîñòè ôîðìóëû
� �x x r Q r x r Q r( ( ( , ) ( ), ( , )) ( ))pt � � ,
ãäå �( , )x r è �( , )x r — ïðåä- è ïîñòóñëîâèÿ ðàññìàòðèâàåìîãî ïðîòîêîëà.
Ñòàòè÷åñêè íàéäåííûå íåäåòåðìèíèçìû, òóïèêè è íàðóøåíèÿ óñëîâèé öåëîñò-
íîñòè ÿâëÿþòñÿ ëèøü ïðåäïîëîæèòåëüíûìè îøèáêàìè. Ñîñòîÿíèÿ ñðåäû ñ îøèáêà-
ìè ìîæíî ïîëó÷èòü, àíàëèçèðóÿ ôîðìóëû, êîòîðûå âûðàæàþò íåïðîòèâîðå÷èâîñòü,
ïîëíîòó èëè óñëîâèÿ öåëîñòíîñòè. Äîñòèæèìîñòü ýòèõ ñîñòîÿíèé ìîæíî îïðîâåðãàòü
ñòàòè÷åñêèìè ìåòîäàìè, ñôîðìóëèðîâàâ ñîîòâåòñòâóþùèå óñëîâèÿ öåëîñòíîñòè, èëè
äîêàçûâàòü ñ ïîìîùüþ ãåíåðàöèè òðàññ è ïîèñêà â ïðîñòðàíñòâå ñîñòîÿíèé.
Äåäóêòèâíûå ñðåäñòâà ñèñòåìû VRS. Èñïîëüçóåìàÿ â VRS òåîðèÿ (ëèíåéíàÿ
àðèôìåòèêà, ñèìâîëüíûå òèïû, ïåðå÷èñëèìûå òèïû è î÷åðåäè) àëãîðèòìè÷åñêè íå-
ðàçðåøèìà, ïîñêîëüêó ÷èñëîâûå ôóíêöèè ïîçâîëÿþò ìîäåëèðîâàòü âñþ àðèôìåòè-
êó. Îäíàêî îãðàíè÷åíèå òåîðèè òîëüêî ýêçèñòåíöèàëüíûìè ôîðìóëàìè ñ îãðàíè-
÷åííûì èñïîëüçîâàíèåì êâàíòîðîâ îáùíîñòè ïîçâîëèëî ïîëó÷èòü ðàçðåøèìûé
ôðàãìåíò, êîòîðûé ïðèìåíÿåòñÿ äëÿ âû÷èñëåíèÿ ïðåäèêàòíûõ òðàíñôîðìåðîâ. Äå-
äóêòèâíàÿ ñèñòåìà ðåøàåò äâå îñíîâíûå çàäà÷è: ïðîâåðêó âûïîëíèìîñòè ôîðìóë è
èõ óïðîùåíèå. Ïåðâàÿ çàäà÷à ðåøàåòñÿ íåïîñðåäñòâåíî ïîñëå ïîëó÷åíèÿ ðåçóëüòà-
òà ïðèìåíåíèÿ ïðåäèêàòíîãî òðàíñôîðìåðà ñ öåëüþ èñêëþ÷åíèÿ íåâûïîëíèìûõ
äèçúþíêòèâíûõ ÷ëåíîâ; âòîðàÿ çàäà÷à ðåøàåòñÿ ñ öåëüþ ïîëó÷åíèÿ îêîí÷àòåëüíîãî
ðåçóëüòàòà ïðèìåíåíèÿ òðàíñôîðìåðà.
Àëãîðèòì ïðîâåðêè âûïîëíèìîñòè îñíîâàí íà ýëèìèíàöèè íåèíòåðïðåòèðî-
âàííûõ ôóíêöèîíàëüíûõ ñèìâîëîâ ìåòîäîì Øîñòàêà [19]. Óïðîùåíèå ôîðìóë çà-
êëþ÷àåòñÿ â ýëèìèíàöèè êâàíòîðîâ, êîãäà ýòî âîçìîæíî, à òàêæå â óïðîùåíèè ñèñ-
òåì ëèíåéíûõ íåðàâåíñòâ.
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 15
ÇÀÊËÞ×ÅÍÈÅ
Ïîñòðîåííûå àëãîðèòìû ïðåîáðàçîâàíèé ôîðìóë ðåàëèçîâàíû â âèäå ïðåäèêàò-
íîãî òðàíñôîðìåðà â ñèñòåìå âåðèôèêàöèè òðåáîâàíèé VRS. Ïðåäèêàòíûé
òðàíñôîðìåð èñïîëüçóåòñÿ êàê äëÿ ïîñòðîåíèÿ ïðîñòðàíñòâà ñîñòîÿíèé ñ ïîñëå-
äóþùåé ãåíåðàöèåé òðàññ, òàê è äëÿ ñòàòè÷åñêîãî àíàëèçà ìîäåëåé. Ýòè ìåòîäû
ïîçâîëÿþò èñïîëüçîâàòü VRS äëÿ ïîèñêà íàðóøåíèé äèíàìè÷åñêèõ è ñòàòè÷åñ-
êèõ ñâîéñòâ ñèñòåì.
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. B a r a n o v S . , J e r v i s Ñ . , K o t l y a r o v V . , L e t i c h e v s k y A . , a n d W e i g e r t T . Leveraging UML
to deliver correct telecom applications / L. Lavagno, G. Martin, and B.Selic, eds // UML for Real: Design
of Embedded Real-Time Systems. — Amsterdam: Kluwer Academic Publishers, 2003. — Ð. 323–342.
2. L e t i c h e v s k y A . , K a p i t o n o v a J . , L e t i c h e v s k y A . ( j r . ) , V o l k o v V . , B a r a n o v S . ,
K o t l y a r o v V . , a n d W e i g e r t T . Basic protocols, message sequence charts, and the verification of re-
quirements specifications // Computer Networks. — 2005. — N 47. — P. 662–675.
3. K a p i t o n o v a J . , L e t i c h e v s k y À . , V o l k o v V . , a n d W e i g e r t T . Validation of embedded sys-
tems / R. Zurawski, ed. // The Embedded Systems Handbook. — Miami: CRC Press. – 2005. — 51 ð.
4. Ë å ò è ÷ å â ñ ê è é À . À ä . , Ê à ï è ò î í î â à Þ . Â . , Â î ë ê î â Â . À . , Ë å ò è ÷ å â ñ ê è é À . À . ,
Á à ð à í î â Ñ . Í . , Ê î ò ë ÿ ð î â Â . Ï . , Â å é ã å ð ò Ò . Ñïåöèôèêàöèÿ ñèñòåì ñ ïîìîùüþ áàçîâûõ
ïðîòîêîëîâ // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 2005. — ¹ 4. — C. 3–21.
5. L e t i c h e v s k y A . , K a p i t o n o v a J . , K o t l y a r o v V . , L e t i c h e v s k y A . ( j r . ) , N i k i t c h e n -
k o N . , V o l k o v V . , a n d W e i g e r t T . Insertion modeling in distributed system design // Problems in
Programming (ISSN 1727-4907). — 2008. — N 4. — P. 13–39.
6. D i j k s t r a E . W . A discipline of programming // Prentice-Hall, Englewood Cliffs, N.J., 1976. — 217 ð.
7. L a m p o r t L e s l i e . Win and sin: predicate transformer for concurrency // ACM Translation on Program-
ming Language and System (TOPLAS), New York: ACM. — 1990. — 12, Issue 3 (July 1990). —
P. 396–428.
8. Ã î ä ë å â ñ ê è é À . Á . Ïðåäèêàòíûå ïðåîáðàçîâàòåëè â êîíòåêñòå ñèìâîëüíîãî ìîäåëèðîâàíèÿ
òðàíçèöèîííûõ ñèñòåì // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 2010. — ¹ 4. — Ñ..
9. L e t i c h e v s k y A . a n d G i l b e r t D . A model for interaction of agents and environments / D. Bert,
C. Choppy, P. Moses, eds. // Recent Trends in Algebraic Development Techniques. Lecture Notes in Com-
puter Science 1827, Springe, 1999. — Ð. 311–328.
10. L e t i c h e v s k y A . Algebra of behavior transformations and its applications. In V.B. Kudryavtsev and
I.G. Rosenberg, eds. // Structural theory of Automata, Semigroups, and Universal Algebra, NATO Science
Series II. Mathematics, Physics and Chemistry, Springer. — 2005. — 207. — P. 241–272.
11. R e n i e r s M . Message sequence chart: Syntax and semantics // Ph.D. Thesis. Eindhoven University of
Technology, 1998.
12. I n t e r n a t i o n a l Telecommunications Union. ITU-T Recommendation Z.120: Message Sequence Charts //
Geneva: ITU–T, 2002.
13. L e t i c h e v s k i i A . A . , K a p i t o n o v a Y u . V . , K o t l y a r o v V . P . , L e t i c h e v -
s k i i A . A . J r . , V o l k o v V . A . Semantics of timed Message Sequence Charts / Êèáåðíåòèêà è
ñèñòåìíûé àíàëèç. — 2002. — ¹ 4. — Ñ. 3–14.
14. L e t i c h e v s k y A . , K a p i t o n o v a J . , K o t l y a r o v V . , V o l k o v V . , L e t i c h e v s k y A . ( j r . ) , and
W e i g e r t T . Semantics of message sequence charts // SDL Forum. — 2005. — P. 117–132.
15. Q u i e l l e J . a n d S i f a k i s J . Specification and verification of concurrent systems in CESAR // Proc.
5th Intern. Symposium on Programming, 1981. — P. 142–158.
16. B u r c h J . , C l a r k e E . , M c M i l l a n K . , D i l l D . , a n d H w a n g L . Symbolic model checking:
1020 states and beyond // Information and Computation. — 1992. — N 98(2). — P. 142–170.
17. L a m p o r t L . The temporal logic of actions // ACM Transactions on Programming Languages and Sys-
tems, 1994. — P. 872–923.
18. B u l t a n T . a n d Y a v u z - K a h v e c i T . Action language verifier // Proc. of ASE 2001, 2001. —
P. 382–386.
19. S h o s t a k R . A practical decision procedure for arithmetic with function symbols // J. of the Assoñiation
for Computing Machinery. — 1979. – 26, N 2. — P. 351–360.
Ïîñòóïèëà 15.04.2010
16 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
|
| id | nasplib_isofts_kiev_ua-123456789-45239 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0023-1274 |
| language | Russian |
| last_indexed | 2025-12-07T13:14:25Z |
| publishDate | 2010 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| record_format | dspace |
| spelling | Летичевский, А.А. Годлевский, А.Б. Летичевский, А.А. (мл.) Потиенко, С.В. Песчаненко, В.С. 2013-06-10T16:10:12Z 2013-06-10T16:10:12Z 2010 Свойства предикатного трансформера системы VRS / А.А. Летичевский, А.Б. Годлевский, А.А. Летичевский (мл.), С.В. Потиенко, В.С. Песчаненко // Кибернетика и системный анализ. — 2010. — № 4. — С. 3-16. — Бібліогр.: 19 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/45239 519.686.2 Розглянуто моделі, записані в мові базових протоколів. Вони є атрибутними транзиційними системами, а їх стани задаються формулами багатосортного числення предикатів першого порядку над атрибутами системи. Допускаються атрибути простих числових символьних типів, функціональних типів, а також черги. В постумовах базових протоколів використовуються оператори присвоювання, оновлення черг та довільні формули. Для здійснення переходу із одного стану в інший побудовано предикатний трансформер як функцію перетворення формул. Доведено основну властивість предикатного трансформера, згідно якій він обчислює найсильнішу постумову для символьних станів. The paper considers models specified in basic protocol language. They are attribute transition systems and their states are defined by formulas of first-order multisort predicate calculus over system attributes. Attributes of simple numeric and symbolic types, functional types, and queues are allowed. Assignment operators, queue update operators, and arbitrary formulas are used in postconditions of basic protocols. To pass from one state to another, a predicate transformer has been set up as a function of formula transformation. The main property of the predicate transformer has been proved: it calculates the strongest postcondition for symbolic states. ru Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Кибернетика Свойства предикатного трансформера системы VRS Властивості предикатного трансформера системи VRS Properties of a predicate transformer of VRS system Article published earlier |
| spellingShingle | Свойства предикатного трансформера системы VRS Летичевский, А.А. Годлевский, А.Б. Летичевский, А.А. (мл.) Потиенко, С.В. Песчаненко, В.С. Кибернетика |
| title | Свойства предикатного трансформера системы VRS |
| title_alt | Властивості предикатного трансформера системи VRS Properties of a predicate transformer of VRS system |
| title_full | Свойства предикатного трансформера системы VRS |
| title_fullStr | Свойства предикатного трансформера системы VRS |
| title_full_unstemmed | Свойства предикатного трансформера системы VRS |
| title_short | Свойства предикатного трансформера системы VRS |
| title_sort | свойства предикатного трансформера системы vrs |
| topic | Кибернетика |
| topic_facet | Кибернетика |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/45239 |
| work_keys_str_mv | AT letičevskiiaa svoistvapredikatnogotransformerasistemyvrs AT godlevskiiab svoistvapredikatnogotransformerasistemyvrs AT letičevskiiaaml svoistvapredikatnogotransformerasistemyvrs AT potienkosv svoistvapredikatnogotransformerasistemyvrs AT pesčanenkovs svoistvapredikatnogotransformerasistemyvrs AT letičevskiiaa vlastivostípredikatnogotransformerasistemivrs AT godlevskiiab vlastivostípredikatnogotransformerasistemivrs AT letičevskiiaaml vlastivostípredikatnogotransformerasistemivrs AT potienkosv vlastivostípredikatnogotransformerasistemivrs AT pesčanenkovs vlastivostípredikatnogotransformerasistemivrs AT letičevskiiaa propertiesofapredicatetransformerofvrssystem AT godlevskiiab propertiesofapredicatetransformerofvrssystem AT letičevskiiaaml propertiesofapredicatetransformerofvrssystem AT potienkosv propertiesofapredicatetransformerofvrssystem AT pesčanenkovs propertiesofapredicatetransformerofvrssystem |