Предикатные преобразователи в контексте символьного моделирования транзиционных систем
При моделюванні атрибутних транзиційних систем класи їх станів описуються за допомогою формул логіки в заданій сигнатурі функціональних та предикатних символів. Побудовано процедуру перетворення таких формул під дією операторів присвоювання та доведено, що трансформовані формули відповідають найсиль...
Saved in:
| Published in: | Кибернетика и системный анализ |
|---|---|
| Date: | 2010 |
| Main Author: | |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут кібернетики ім. В.М. Глушкова НАН України
2010
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/45246 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Предикатные преобразователи в контексте символьного моделирования транзиционных систем / А.Б. Годлевский // Кибернетика и системный анализ. — 2010. — № 4. — С. 91-99. — Бібліогр.: 7 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859984467131629568 |
|---|---|
| author | Годлевский, А.Б. |
| author_facet | Годлевский, А.Б. |
| citation_txt | Предикатные преобразователи в контексте символьного моделирования транзиционных систем / А.Б. Годлевский // Кибернетика и системный анализ. — 2010. — № 4. — С. 91-99. — Бібліогр.: 7 назв. — рос. |
| collection | DSpace DC |
| container_title | Кибернетика и системный анализ |
| description | При моделюванні атрибутних транзиційних систем класи їх станів описуються за допомогою формул логіки в заданій сигнатурі функціональних та предикатних символів. Побудовано процедуру перетворення таких формул під дією операторів присвоювання та доведено, що трансформовані формули відповідають найсильнішим післяумовам. Особливістю роботи є можливість використання атрибутів функціонального типу в описах транзиційних систем, зокрема імен масивів.
For modelling, the classes of states of attribute transition system can be described in a given signature of functional and predicate symbols. A procedure of transforming such formulas by assignment operators is developed and the resulted formulas are proved to correspond to strongest postconditions. A peculiarity of the paper is that functional-type attributes can be used in the specification of transition systems, especially array-type attributes.
|
| first_indexed | 2025-12-07T16:27:32Z |
| format | Article |
| fulltext |
ÓÄÊ 519.172
À.Á. ÃÎÄËÅÂÑÊÈÉ
ÏÐÅÄÈÊÀÒÍÛÅ ÏÐÅÎÁÐÀÇÎÂÀÒÅËÈ Â ÊÎÍÒÅÊÑÒÅ
ÑÈÌÂÎËÜÍÎÃÎ ÌÎÄÅËÈÐÎÂÀÍÈß ÒÐÀÍÇÈÖÈÎÍÍÛÕ ÑÈÑÒÅÌ
Êëþ÷åâûå ñëîâà: àòðèáóòíûå òðàíçèöèîííûå ñèñòåìû, ñèìâîëüíîå ìîäåëèðî-
âàíèå, ïðåäèêàòíûé ïðåîáðàçîâàòåëü, áàçîâûé ïðîòîêîë.
ÂÂÅÄÅÍÈÅ
Îäíèì èç îñíîâíûõ íàïðàâëåíèé íà ñòûêå èíôîðìàòèêè è ïðîãðàììíîé èíæåíå-
ðèè ÿâëÿþòñÿ ôîðìàëüíûå ìåòîäû êàê ìàòåìàòè÷åñêèé áàçèñ ïîñòðîåíèÿ êà÷åñò-
âåííûõ ïðîãðàììíûõ ïðîäóêòîâ. Ôîðìàëüíûå ìåòîäû ïðåäïîëàãàþò ðàññìîòðå-
íèå ïðîãðàìì íà óðîâíå ìîäåëåé, ÿçûêîâ ñïåöèôèêàöèé è îðèåíòèðîâàíû íà âû-
ÿâëåíèå â ïðîãðàììàõ îøèáîê, èõ âåðèôèêàöèþ íà ðàííèõ ýòàïàõ ðàçðàáîòêè.
Âåðèôèêàöèîííûé ïîäõîä â ïðîãðàììèðîâàíèè çàëîæåí â ðàáîòàõ Ð. Ôëîéäà [1]
è Ò. Õîàðà [2], â êîòîðûõ ïîä÷åðêèâàëàñü ðîëü ñïåöèôèêàöèé êàê äëÿ ñîñòîÿíèé
ïðîãðàìì (ïîíÿòèå assertions ó Ð. Ôëîéäà), òàê è äëÿ ïåðåõîäîâ ìåæäó ñîñòîÿíè-
ÿìè («òðîéêè Õîàðà»). Â ðàìêàõ ýòîãî íàïðàâëåíèÿ áûëè ââåäåíû ïîíÿòèÿ ñëà-
áåéøåãî ïðåäóñëîâèÿ è ñèëüíåéøåãî ïîñòóñëîâèÿ, êîòîðûå íà óðîâíå ÿçûêà ëî-
ãèêè è ñèìâîëüíûõ èñ÷èñëåíèé ïîçâîëÿëè õàðàêòåðèçîâàòü ñîñòîÿíèÿ ïðîãðàììû
êàê ïðåäøåñòâóþùåãî äàííîìó, òàê è ñëåäóþùåìó çà íèì, èñõîäÿ èç õàðàêòå-
ðèñòèêè òåêóùåãî ñîñòîÿíèÿ è ñïåöèôèêàöèè ïåðåõîäà. Ïîçäíåå Ë. Ëýìïîðò [3]
èñïîëüçîâàë ýòè ïîíÿòèÿ äëÿ âåðèôèêàöèè ïàðàëëåëüíûõ ïðîãðàìì è ïîñòðîåíèÿ
äëÿ íèõ èíâàðèàíòîâ, îñíîâàííûõ íà ïðåäóñëîâèÿõ è ïîñòóñëîâèÿõ.
Íîâûì òîë÷êîì â ðàçâèòèè ôîðìàëüíûõ ìåòîäîâ ñòàë ïîäõîä, ïîëó÷èâøèé íà-
çâàíèå ïðîâåðêè íà ìîäåëÿõ (model checking), êîãäà â ðàìêàõ ìîäåëè ðàçðàáàòûâàå-
ìîé ïðîãðàììû àíàëèçèðóþòñÿ âñåâîçìîæíûå ïóòè åå èñïîëíåíèÿ è ïðîâåðÿåòñÿ
âûïîëíèìîñòü àíàëèçèðóåìûõ ñâîéñòâ. Ýòîò ïîäõîä, êîòîðûé âïåðâûå, ïî-âèäèìî-
ìó, áûë èçëîæåí â [4], ïðåäïîëàãàåò èñïîëüçîâàíèå ðàçëè÷íûõ ôîðì àáñòðàêöèè
äëÿ ìîäåëèðîâàíèÿ ïðîãðàìì è ïðîèñõîäÿùèõ â íèõ ïðîöåññîâ. Ïðîãðàììû
è êîìïëåêñû âçàèìîäåéñòâóþùèõ ïðîãðàìì ðàññìàòðèâàþòñÿ òàêæå â ðàìêàõ ìî-
äåëè òðàíçèöèîííûõ ñèñòåì, ãäå îñíîâíûìè ïîíÿòèÿìè ÿâëÿþòñÿ ïîíÿòèå ñîñòîÿ-
íèÿ ñèñòåìû, ïðàâèëà ïåðåõîäîâ íà ïðîñòðàíñòâå ñîñòîÿíèé, îïèñàíèå ñâîéñòâ
ïðîöåññîâ, êîòîðûå ïðîèñõîäÿò â ñèñòåìå.
 äàííîé ðàáîòå èññëåäóåòñÿ ìîäåëü âçàèìîäåéñòâóþùèõ àãåíòîâ è ñðåä, ââå-
äåííàÿ À.À. Ëåòè÷åâñêèì [5] è ðàçâèòàÿ çàòåì â ðàìêàõ ïàðàäèãìû èíñåðöèîííîãî
ïðîãðàììèðîâàíèÿ [6], êîãäà àêòèâàöèÿ è ôóíêöèîíèðîâàíèå àãåíòà (ïðîãðàììû)
âî âçàèìîäåéñòâèè ñ äðóãèìè àãåíòàìè è èõ îáùåé ñðåäîé ðàññìàòðèâàåòñÿ êàê
ôóíêöèÿ ïîãðóæåíèÿ àãåíòîâ â ñðåäó. Ýòà èäåÿ âçàèìîäåéñòâóþùèõ àãåíòîâ íàøëà
çàòåì âîïëîùåíèå â ðåàëèçàöèè ñèñòåìû VRS (Verification Requirement System),
ðàçðàáàòûâàåìîé ïîä ðóêîâîäñòâîì À.À. Ëåòè÷åâñêîãî è â ñîòðóäíè÷åñòâå ñ êîì-
ïàíèåé Motorola. Ìîäåëèðóåìûå ïðèëîæåíèÿ ïðåäñòàâëÿþòñÿ àòðèáóòíûìè òðàí-
çèöèîííûìè ñèñòåìàìè, ñîñòîÿíèÿ ýòèõ ñèñòåì — ôîðìóëàìè ëîãèêè, ïîñòðîåííû-
ìè íàä ìíîæåñòâîì àòðèáóòîâ. Ïðàâèëà ïåðåõîäîâ â ìîäåëèðóåìûõ ñèñòåìàõ ïðåä-
ñòàâëåíû áàçîâûìè ïðîòîêîëàìè, êîòîðûå ïîäîáíî òðîéêàì Õîàðà ñîñòîÿò èç
ïðåäóñëîâèÿ, îáóñëàâëèâàþùåãî ïðèìåíèìîñòü ïðîòîêîëà, ñïåöèôèöèðóåìîãî äåé-
ñòâèÿ è ïîñòóñëîâèÿ, îïèñûâàþùåãî ïðåîáðàçîâàíèå ïðè äàííîì ïåðåõîäå. Ïðè
ñèìâîëüíîì ìîäåëèðîâàíèè àòðèáóòíûõ òðàíçèöèîííûõ ñèñòåì êëþ÷åâóþ ðîëü èã-
ðàåò ìåõàíèçì ïðåîáðàçîâàíèÿ ôîðìóë, ïðåäñòàâëÿþùèõ êëàññû ñîñòîÿíèé ñèñòå-
ìû, ïî ñóòè, ìåõàíèçì ïîñòðîåíèÿ ñèëüíåéøåãî ïîñòóñëîâèÿ. Â ðàáîòå ýòîò ìåõà-
íèçì, íàçûâàåìûé ïðåäèêàòíûì ïðåîáðàçîâàòåëåì (predicate transformer), îïèñûâà-
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 91
© À.Á. Ãîäëåâñêèé, 2010
åòñÿ äëÿ ñëó÷àÿ, êîãäà äîïóñêàþòñÿ àòðèáóòû ôóíêöèîíàëüíîãî òèïà, ê êîòîðûì,
â ÷àñòíîñòè, îòíîñÿòñÿ ìàññèâû. Ðàññìàòðèâàåòñÿ ñëó÷àé ñóïåðïîçèöèè àòðèáóòîâ,
êîãäà àðãóìåíòàìè îäíèõ àòðèáóòîâ ìîãóò áûòü äðóãèå, ñêàëÿðíîãî èëè
ôóíêöèîíàëüíîãî òèïà. Îñíîâíîé ðåçóëüòàò ñîñòîèò â äîêàçàòåëüñòâå ñâîéñòâà äëÿ
îïèñûâàåìîãî ïðåäèêàòíîãî ïðåîáðàçîâàòåëÿ ñòðîèòü ñèëüíåéøåå ïîñòóñëîâèå.
1. ÏÐÎÑÒÛÅ ÀÒÐÈÁÓÒÍÛÅ ÒÐÀÍÇÈÖÈÎÍÍÛÅ ÑÈÑÒÅÌÛ
Ïóñòü çàäàíû êîíå÷íàÿ ñèãíàòóðà � � �� ( , ) ôóíêöèîíàëüíûõ è ïðåäèêàòíûõ
ñèìâîëîâ, êîíå÷íîå ìíîæåñòâî ïðîñòûõ (ñêàëÿðíûõ) àòðèáóòîâ A . Ñèìâîëû èç
� õàðàêòåðèçóþòñÿ àðíîñòüþ, òèïàìè àðãóìåíòîâ è òèïîì çíà÷åíèÿ. Àòðèáóòó
a A� ñîîòâåòñòâóåò îïðåäåëåííûé òèï � è äîìåí D
�
âîçìîæíûõ çíà÷åíèé. Ïîíÿ-
òèå òåðìà îïðåäåëÿåòñÿ äâóìÿ ïðàâèëàìè. Âî-ïåðâûõ, òåðìàìè ÿâëÿþòñÿ ñèìâî-
ëû àòðèáóòîâ è êîíñòàíòû èç äîìåíîâ, êîòîðûå ñîîòâåòñòâóþò àòðèáóòàì èç A.
Òèï òàêîãî òåðìà îïðåäåëÿåòñÿ êàê òèï àòðèáóòà èëè äîìåíà. Âî-âòîðûõ, äëÿ
âñÿêîãî n-àðíîãî ôóíêöèîíàëüíîãî ñèìâîëà f è òåðìîâ t t n1 , ,� , òèïû êîòîðûõ
ñîîòâåòñòâóþò òèïàì àðãóìåíòîâ f , òåðìîì áóäåò f t t n( , , )1 � , è òèï ýòîãî òåð-
ìà ñîîòâåòñòâóåò òèïó çíà÷åíèé f . Âûðàæåíèå âèäà �( , , )t t n1 � íàçîâåì ïðåäè-
êàòíûì òåðìîì, åñëè � — n-àðíûé ïðåäèêàòíûé ñèìâîë, t t n1 , ,� — òåðìû ñî-
îòâåòñòâóþùèõ òèïîâ. Ôîðìóëà — ýòî âûðàæåíèå, ïîñòðîåííîå ïîñðåäñòâîì
ïðîïîçèöèîíàëüíûõ ñâÿçîê èç ïðåäèêàòíûõ òåðìîâ. Èíòåðïðåòàöèåé ôóíêöèî-
íàëüíûõ è ïðåäèêàòíûõ ñèìâîëîâ îòíîñèòåëüíî ñåìåéñòâà äîìåíîâ { }D T� �� íà-
çîâåì îòîáðàæåíèåì I, êîòîðîå êàæäîìó ôóíêöèîíàëüíîìó ñèìâîëó f ñîïîñòàâëÿåò
(÷àñòè÷íîå) îòîáðàæåíèå òèïà D D Dn1 � � �� , ãäå äîìåíû D Dn1 , , ,� D ñîîòâåò-
ñòâóþò òèïó f , à êàæäîìó ïðåäèêàòíîìó ñèìâîëó � — îòîáðàæåíèå òèïà
D Dn1 0 1� � �� { }, .
Ïðîñòàÿ àòðèáóòíàÿ òðàíçèöèîííàÿ ñèñòåìà (ATS) — ýòî ÷åòâåðêà
S S BP� ( , , , )Init Final , ãäå S — ìíîæåñòâî ñîñòîÿíèé ñèñòåìû, BP — êîíå÷íîå
ìíîæåñòâî åå ïðàâèë ïåðåõîäà (íàçûâàåìûõ íèæå áàçîâûìè ïðîòîêîëàìè, èëè ïðî-
ñòî ïðîòîêîëàìè), Init è Final — ñîîòâåòñòâåííî ìíîæåñòâà íà÷àëüíûõ è ôèíàëü-
íûõ ñîñòîÿíèé. Ñîñòîÿíèå s — ýòî îòîáðàæåíèå A D Dk� 1 � , êîòîðîå êàæäî-
ìó àòðèáóòó a ñîïîñòàâëÿåò çíà÷åíèå èç äîìåíà, ñîîòâåòñòâóþùåãî òèïó ýòîãî àò-
ðèáóòà. Åñëè s — ñîñòîÿíèå ñèñòåìû, t è F — òåðì è ôîðìóëà íàä ìíîæåñòâîì
àòðèáóòîâ A, òî âûðàæåíèÿìè s t( ) è s F( ) áóäóò îáîçíà÷àòüñÿ çíà÷åíèÿ ýòèõ òåðìà è
ôîðìóëû â ñîñòîÿíèè s. Áàçîâûé ïðîòîêîë — ýòî êîíñòðóêöèÿ âèäà
u a a bp a an n( , , ) ( , , )1 1� ��
� � , ãäå a an1 , ,� — íåêîòîðîå ìíîæåñòâî àòðèáó-
òîâ èç A, bp — èìÿ ïðîòîêîëà, u a an( , , )1 � — ïðåäóñëîâèå è �( , , )a an1 � — ïî-
ñòóñëîâèå ïðîòîêîëà. Ïðåäóñëîâèå — ýòî ôîðìóëà íàä ìíîæåñòâîì àòðèáóòîâ
{ }a an1 , , ,� ïîñòóñëîâèå — ãðóïïîâîé îïåðàòîð ïðèñâàèâàíèÿ, ñîñòîÿùèé èç íå-
ñêîëüêèõ ïðîñòûõ ïðèñâàèâàíèé âèäà a ti i:� . Òåðìû â ïðàâûõ ÷àñòÿõ ïðèñâàèâàíèé
ìîãóò çàâèñåòü îò àòðèáóòîâ a an1 , ,� , ïåðå÷èñëåííûõ â ïðåäóñëîâèè, íî íå îò
èíûõ àòðèáóòîâ èç ìíîæåñòâà A. Ñåìàíòèêà ãðóïïîâûõ ïðèñâàèâàíèé ïðåäïîëàãà-
åò, ÷òî äëÿ çàäàííîãî ñîñòîÿíèÿ s òðàíçèöèîííîé ñèñòåìû âíà÷àëå âû÷èñëÿþòñÿ
çíà÷åíèÿ âñåõ ïðàâûõ ÷àñòåé ïðèñâàèâàíèé. Çàòåì îíè îáúÿâëÿþòñÿ íîâûìè çíà÷å-
íèÿìè ñîîòâåòñòâóþùèõ àòðèáóòîâ èç ëåâûõ ÷àñòåé ïðèñâàèâàíèé, â ðåçóëüòàòå
ñèñòåìà ïåðåõîäèò â íîâîå ñîñòîÿíèå s�. Ïðîòîêîë bp ïðèìåíèì ê ñîñòîÿíèþ s, åñëè
åãî ïðåäóñëîâèå âûïîëíèìî íà s è ðåçóëüòàòîì ïðèìåíåíèÿ ïðîòîêîëà áóäåò
ñîñòîÿíèå s�, ïîëó÷åííîå èç s ïîä äåéñòâèåì ïðèñâàèâàíèé ïîñòóñëîâèÿ.
Òðàññîé â ñèñòåìå S áóäåì íàçûâàòü ïîñëåäîâàòåëüíîñòü s s
bp bp
0 1
0 1
�
�
...
... s sk
bp
k
k
�
�1� ñîñòîÿíèé, â êîòîðîé êàæäîå ïîñëåäóþùåå ñîñòîÿíèå ïîëó÷àåò-
ñÿ èç ïðåäûäóùåãî â ðåçóëüòàòå ïðèìåíåíèÿ ê íåìó ñîîòâåòñòâóþùåãî áàçîâîãî
ïðîòîêîëà. Áóäåì ãîâîðèòü, ÷òî ìíîæåñòâî Final äîñòèæèìî èç Init, åñëè ñóùåñòâó-
åò òðàññà, âåäóùàÿ îò îäíîãî èç íà÷àëüíûõ ñîñòîÿíèé ê îäíîìó èç ôèíàëüíûõ.
 òåðìèíàõ äîñòèæèìîñòè ñîñòîÿíèé ôîðìóëèðóåòñÿ îäíî èç îñíîâíûõ ñâîéñòâ
92 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
òðàíçèöèîííûõ ñèñòåì — ñâîéñòâî áåçîïàñíîñòè: ñèñòåìà S íàçûâàåòñÿ áåçîïàñ-
íîé, åñëè Final íåäîñòèæèìî èç Init. Ñîäåðæàòåëüíî ýòî ñâîéñòâî îçíà÷àåò, ÷òî ñèñ-
òåìà íå ìîæåò äîñòè÷ü «ïëîõèõ» ñîñòîÿíèé ñ òî÷êè çðåíèÿ ïðèëîæåíèé. Ïðîâåðêà
ñâîéñòâà áåçîïàñíîñòè ÿâëÿåòñÿ òðóäíîé çàäà÷åé, ïîñêîëüêó ìíîæåñòâî S ìîæåò
áûòü áåñêîíå÷íûì èëè î÷åíü áîëüøèì. Ñ ýòîé öåëüþ ïðèìåíÿåòñÿ ñèìâîëüíîå ìî-
äåëèðîâàíèå, êîãäà ñîñòîÿíèÿ ñèñòåìû ðàçáèâàþòñÿ íà êëàññû è ðàññìàòðèâàþòñÿ
ïåðåõîäû ìåæäó ýòèìè êëàññàìè, èíäóöèðîâàííûå ïðîòîêîëàìè èñõîäíîé ñèñòå-
ìû. Çàòåì ïðîâåðêà ñâîéñòâà áåçîïàñíîñòè ìîæåò îñóùåñòâëÿòüñÿ äâóìÿ ïóòÿìè.
Åñëè èìååòñÿ ïðåäïîëîæåíèå î íåäîñòèæèìîñòè ìíîæåñòâà Final, òî ñòàâèòñÿ
öåëü — äîêàçàòü èíâàðèàíòíîñòü ìíîæåñòâà ñîñòîÿíèé, äîïîëíÿþùèõ Final äî óíè-
âåðñóìà ñîñòîÿíèé. Åñëè æå èìååòñÿ îáðàòíîå ïðåäïîëîæåíèå, òî îñóùåñòâëÿåòñÿ
ïðîâåðêà äîñòèæèìîñòè íà ìîäåëè (model checking), ò.å. â ìîäåëèðóþùåé ñèñòåìå,
ãäå ñîñòîÿíèÿìè ÿâëÿþòñÿ êëàññû èñõîäíûõ ñîñòîÿíèé è ðàññìàòðèâàþòñÿ îáîáùå-
íèÿ ïðàâèë ïåðåõîäà.  îáîèõ ýòèõ ïîäõîäàõ êëþ÷åâûìè ïóíêòàìè ñîîòâåòñòâåííî
ÿâëÿþòñÿ ïîñòðîåíèå ìîäåëè òðàíçèöèîííîé ñèñòåìû è ïîñòðîåíèå âíóòðè íåå ïðà-
âèë ïåðåõîäà, àäåêâàòíûõ ïðàâèëàì â èñõîäíîé ñèñòåìå.
Çäåñü â êà÷åñòâå ñîñòîÿíèé ìîäåëè ðàññìàòðèâàþòñÿ ôîðìóëû ñèãíàòóðû �
íàä ìíîæåñòâîì àòðèáóòîâ A, à ïðàâèëà ïåðåõîäîâ ñòðîÿòñÿ ïîñðåäñòâîì ïðåäèêàò-
íîãî ïðåîáðàçîâàòåëÿ (predicate transformer), îáîçíà÷àåìîãî pt F bp( , ) , àðãóìåíòû
êîòîðîãî — ýòî ôîðìóëà F è áàçîâûé ïðîòîêîë bp. Èíîãäà ïðåäèêàòíûé ïðåîáðà-
çîâàòåëü áóäåì îáîçíà÷àòü òàêæå pt F u( & , )� , óòî÷íÿÿ, ÷òî îïåðàòîð ïîñòóñëîâèÿ �
òðàíñôîðìèðóåò êàê èñõîäíóþ ôîðìóëó F, òàê è ïðåäóñëîâèå u áàçîâîãî ïðîòîêî-
ëà. Ïðåîáðàçîâàòåëü pt äåéñòâóåò â òðè øàãà:
• ïðîâåðÿåòñÿ, âûïîëíèìà ëè ôîðìóëà F a a u a ak k( , , )& ( , , )1 1� � ; åñëè íå
âûïîëíèìà, òî ýòî çíà÷èò, ÷òî ïðîòîêîë bp íå ïðèìåíèì êî âñåì ñîñòîÿíè-
ÿì, ãäå èñòèííà F, è, ñëåäîâàòåëüíî, íà ìîäåëè ýòîò ïåðåõîä òàêæå íå ïðè-
ìåíèì ê ôîðìóëå;
• åñëè ôîðìóëà F a a u a ak k( , , )& ( , , )1 1� � âûïîëíèìà, òî îíà ïðåîáðàçóåòñÿ
ïîä äåéñòâèåì ïîñòóñëîâèÿ �( , , )a ak1 � ;
• ïðåîáðàçîâàííàÿ íà ïðåäûäóùåì øàãå ôîðìóëà ïðîâåðÿåòñÿ íà âûïîëíè-
ìîñòü è óïðîùàåòñÿ, åñëè ýòî âîçìîæíî.
 ðàáîòå àêöåíò äåëàåòñÿ íà âòîðîì øàãå, ðàññìàòðèâàåòñÿ àëãîðèòì ïîñòðîå-
íèÿ ôîðìóëû pt F bp( , ) è äîêàçûâàþòñÿ åå ñâîéñòâà, äåìîíñòðèðóþùèå àäåêâàò-
íîñòü ôîðìóëüíîé ìîäåëè. Îòíîñèòåëüíî ïåðâîãî øàãà ìû àáñòðàãèðóåìñÿ îò äåòà-
ëåé êîíêðåòíûõ òðàíçèöèîííûõ ñèñòåì, îò îñîáåííîñòåé, îáóñëîâëåííûõ ñèãíàòó-
ðîé àëãåáðàè÷åñêîé ñèñòåìû, íî ïðåäïîëàãàåì, ÷òî èìååòñÿ àëãîðèòì äëÿ ïðîâåðêè
âûïîëíèìîñòè ôîðìóë èç êëàññà ñ äàííîé ñèãíàòóðîé. Èíûìè ñëîâàìè, ìû ïðåäïî-
ëàãàåì, ÷òî èìååòñÿ íåêèé ðåøàòåëü (off-the-shelf solver), îñóùåñòâëÿþùèé ýòó ïðî-
âåðêó. Çàìåòèì ëèøü, ÷òî ïðèìåíåíèþ ðåøàòåëÿ ïðåäøåñòâóåò çàìåíà àòðèáóòîâ
a ak1 , ,� ñâÿçàííûìè ïåðåìåííûìè x xk1 , ,� , çàòåì ïðîâåðÿåòñÿ âûïîëíèìîñòü
ëîãè÷åñêîé �-ôîðìóëû ( , , ) ( , , )& ( , , )�x x F x x u x xk k k1 1 1� � � .
Òðåòèé øàã, óïðîùåíèå ôîðìóëû, òàêæå íàõîäèòñÿ çà ðàìêàìè äàííîé ðàáîòû
è óïîìèíàåòñÿ çäåñü ëèøü äëÿ òîãî, ÷òîáû ïîä÷åðêíóòü, ÷òî â ïðàêòè÷åñêîé ñèñòå-
ìå ýêâèâàëåíòíûå ïðåîáðàçîâàíèÿ ïî óïðîùåíèþ ôîðìóëû âàæíû, â ÷àñòíîñòè
åñëè ðàññìàòðèâàåòñÿ öåëàÿ öåïî÷êà ïîñëåäîâàòåëüíûõ ïðåîáðàçîâàíèé.  ÷àñòíîñ-
òè, ýòî ìîãóò áûòü äåéñòâèÿ ïî ýëèìèíàöèè ýêçèñòåíöèàëüíûõ êâàíòîðîâ, êîòîðûå
ïîÿâëÿþòñÿ ïðè ïðåîáðàçîâàíèè ôîðìóë.
Ïîñêîëüêó â ïðîöåññå ïðåîáðàçîâàíèé ôîðìóë áóäóò ïîÿâëÿòüñÿ êâàíòîðû,
ðàñøèðèì êëàññ ðàññìàòðèâàåìûõ ôîðìóë. Ðàñøèðåííûé êëàññ âêëþ÷àåò â ñåáÿ
�-ôîðìóëû, êîòîðûå ïîëó÷àþòñÿ â ðåçóëüòàòå çàìåíû íåêîòîðûõ àòðèáóòîâ, âõîäÿ-
ùèõ â ôîðìóëó F, ñèìâîëàìè ïåðåìåííûõ èç íåêîòîðîãî àëôàâèòà X . Ïðåäïîëàãà-
åòñÿ, ÷òî ñâÿçàííûå ïåðåìåííûå òèïèçèðîâàíû è ïðèíèìàþò çíà÷åíèÿ âíóòðè ñîîò-
âåòñòâóþùèõ äîìåíîâ Di . Ôîðìóëà ( , , ) ( , , , , , )�x x F x x a ak k k1 1 1� � � íàçûâàåòñÿ
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 93
âûïîëíèìîé íà ñîñòîÿíèè s, åñëè ñóùåñòâóåò ïîäñòàíîâêà �: ,X D� D D Dn� 1 � ,
òàêàÿ, ÷òî ïðè çàìåíå ñâÿçàííûõ ïåðåìåííûõ èç X èõ çíà÷åíèÿìè �( )x ïîëó÷àåòñÿ
ôîðìóëà, âûïîëíèìàÿ íà ñîñòîÿíèè s. Çàìåòèì, ÷òî ñâÿçàííûå ïåðåìåííûå ìîãóò
ïîÿâëÿòüñÿ âíóòðè ôîðìóë, îïèñûâàþùèõ êëàññû ñîñòîÿíèé, íî íå âíóòðè òåðìîâ,
÷òî íàõîäÿòñÿ â ïðàâûõ ÷àñòÿõ ïðèñâàèâàíèé.
Ïðåîáðàçîâàíèå ôîðìóë äîëæíî óäîâëåòâîðÿòü íè-
æåñëåäóþùåé äèàãðàììå (ðèñ. 1), êîòîðàÿ îïèñûâàåò
èäåàëüíîå ìîäåëèðîâàíèå èñõîäíîé ATS ñèìâîëüíîé
(ôîðìóëüíîé) ìîäåëüþ.
Çäåñü F — ïðåîáðàçóåìàÿ ôîðìóëà, u bp�
� � —
áàçîâûé ïðîòîêîë, F� — ðåçóëüòèðóþùàÿ ôîðìóëà, s� —
ñîñòîÿíèå ñèñòåìû S , â êîòîðîå îíà ïåðåõîäèò ïîä äåé-
ñòâèåì ïðîòîêîëà bp èç ñîñòîÿíèÿ s. Âåðòèêàëüíûå ñòðåë-
êè íà äèàãðàììå îòðàæàþò âûïîëíèìîñòü ôîðìóë F u& è
F� â ñîñòîÿíèÿõ s è s�. Äèàãðàììà îòðàæàåò ñëåäóþùèå
ñâîéñòâà îïèñûâàåìîãî ïðåîáðàçîâàòåëÿ:
a) åñëè s bp s� � ( ) è F u& âûïîëíèìà â s, òî F pt F u� � ( & , )� äîëæíà áûòü âûïîë-
íèìà â s�;
á) åñëè F pt F u� � ( & , )� è F� âûïîëíèìà â íåêîòîðîì s�, òî ñóùåñòâóåò s òàêîå,
÷òî s bp s� � ( ) è F u& âûïîëíèìà â s.
Ïðåäèêàòíûé ïðåîáðàçîâàòåëü, îáëàäàþùèé òàêèìè ñâîéñòâàìè, íàçîâåì èäå-
àëüíûì è îòìåòèì, ÷òî ýòî ïîíÿòèå ïðåîáðàçîâàòåëÿ ñîîòâåòñòâóåò ïîíÿòèþ ñèëü-
íåéøåãî ïîñòóñëîâèÿ (strongest precondition) èç [2].
Ïîñòðîåíèå ôîðìóëû pt F u( & , )� îñóùåñòâëÿåòñÿ ñëåäóþùèì îáðàçîì:
• ïóñòü { }a an1 , ,� — ìíîæåñòâî âñåõ àòðèáóòîâ, íàõîäÿùèåñÿ â ëåâûõ ÷àñòÿõ
ïðèñâàèâàíèÿ �, è ïóñòü a a m nm1 , , ,� � , — âñå òå èç íèõ, âõîæäåíèÿ êîòîðûõ
âñòðå÷àþòñÿ êàê â ôîðìóëå F u& , òàê è â òåðìàõ ïðàâûõ ÷àñòåé ïðèñâàèâàíèé;
• ïóñòü x xm1 , ,� — ñèìâîëû ïåðåìåííûõ, êîòîðûå íå âñòðå÷àëèñü â ôîðìóëå
F u& , òîãäà ïîñòðîèì ïîäñòàíîâêó Sub
a a
x x
m
m
1
1
, ,
, ,
�
�
, êîòîðàÿ, áóäó÷è ïðèìåíåííîé
ê ôîðìóëå èëè òåðìó, çàìåíÿåò â íåé âñå âõîæäåíèÿ ñèìâîëà ai íà ñèìâîë xi ;
• òîãäà pt F u x x G a t a tm m m( & , ) ( , , ) ( & &...& )� � � � � � �1 1 1� , ãäå G — ðå-
çóëüòàò ïðèìåíåíèÿ ïîäñòàíîâêè ê ôîðìóëå F u& , êîãäà ÷àñòü àòðèáóòîâ çàìåíåíà
ïåðåìåííûìè, è �t i — ðåçóëüòàò ïðèìåíåíèÿ ýòîé æå ïîäñòàíîâêè ê òåðìó t i èç ïðà-
âîé ÷àñòè ïðèñâàèâàíèÿ.
Òåîðåìà 1. Ïðåîáðàçîâàòåëü pt (*,*) ÿâëÿåòñÿ èäåàëüíûì. Äîêàæåì ñâîéñòâà
à) è á), îïðåäåëÿþùèå ñâîéñòâî èäåàëüíîñòè ïðåîáðàçîâàòåëåé. Ôîðìóëà F u& ìî-
æåò ñîäåðæàòü ñâÿçàííûå ïåðåìåííûå, íî ïðè ðàññóæäåíèÿõ èõ ìîæíî îïóñòèòü,
åñëè ïîëàãàòü, ÷òî ýòè ïåðåìåííûå çàìåíÿþòñÿ îäíèìè è òåìè æå çíà÷åíèÿìè êàê â
ñîñòîÿíèè s, òàê è â s�, à âíîâü ââîäèìûå ñâÿçàííûå ïåðåìåííûå x xm1 , ,� îòëè÷à-
þòñÿ îò óæå ñóùåñòâóþùèõ â ôîðìóëå.
Ïóñòü ñîñòîÿíèå s òàêîâî, ÷òî s F u( & ) . Ýòî çíà÷èò, ÷òî çàìåíà êàæäîãî àòðè-
áóòà a, âõîäÿùåãî â ôîðìóëó F u& , íà s a( ) , ýëåìåíò èç D, îáðàùàåò ýòó ôîðìóëó â
áóëåâñêîå çíà÷åíèå 1. Çàôèêñèðóåì ýòè çíà÷åíèÿ è ñ ó÷åòîì ïîäñòàíîâêè
Sub
a a
x x
m
m
1
1
, ,
, ,
�
�
âûáåðåì èõ äëÿ ñâÿçàííûõ ïåðåìåííûõ è äëÿ òåõ àòðèáóòîâ, çíà÷åíèÿ
êîòîðûõ íå èçìåíèëèñü. Äëÿ òåõ æå àòðèáóòîâ, çíà÷åíèÿ êîòîðûõ èçìåíèëèñü îïå-
ðàòîðîì ïðèñâàèâàíèÿ, â êà÷åñòâå íîâûõ çíà÷åíèé âûáåðåì çíà÷åíèÿ s t i( ) , êîòî-
ðûå ñîâïàäàþò ñ èõ çíà÷åíèÿìè â ñîñòîÿíèè s bp s� � ( ) . Òåïåðü î÷åâèäíî, ÷òî
ôîðìóëà G áóäåò âûïîëíèìà â ñîñòîÿíèè s� è òåì ñàìûì ñâîéñòâî à) âûïîëíåíî.
Ïóñòü òåïåðü s� — íåêîòîðîå ñîñòîÿíèå, äëÿ êîòîðîãî ôîðìóëà G âûïîëíèìà. Ýòî
çíà÷èò, ÷òî ñóùåñòâóåò îòîáðàæåíèå, ñîïîñòàâëÿþùåå ýëåìåíòû äîìåíîâ êàê àòðèáó-
òàì ýòîé ôîðìóëû, òàê è ñâÿçàííûì ïåðåìåííûì, ïîÿâèâøèìñÿ â G ïðè òðàíñôîðìà-
öèè F u& . Åñëè ýëåìåíò di ñîïîñòàâëÿåòñÿ ñâÿçàííîé ïåðåìåííîé xi , òî ïðè ïîñòðîåíèè
94 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
pt
bp
F u F
s s
(*, )
&
�
�
� �
�
�
�
Ðèñ. 1
ñîñòîÿíèÿ s áóäåì ðàññìàòðèâàòü åãî êàê çíà÷åíèå àòðèáóòà ai , âñòðå÷àþùåãîñÿ â ëåâîé
÷àñòè îäíîãî èç ïðèñâàèâàíèé. Åñëè æå di — çíà÷åíèå àòðèáóòà ai , êîòîðûé íå âñòðå÷àë-
ñÿ â ëåâûõ ÷àñòÿõ ïðèñâàèâàíèé èç �, òî çàôèêñèðóåì ýòî åãî çíà÷åíèå äëÿ ñîñòîÿíèÿ s. Ïî
ïîñòðîåíèþ s è ïî òîìó, êàê ñòðîèòñÿ ôîðìóëà G ïî F u& , î÷åâèäíî, ÷òî F u& áóäåò âû-
ïîëíèìà íà s è s bp s� � ( ) . Òàêèì îáðàçîì, äîêàçàíî è âòîðîå ñâîéñòâî èäåàëüíîñòè ïðåä-
èêàòíîãî ïðåîáðàçîâàòåëÿ pt (*,*) .
Òåîðåìà 1 íå ÿâëÿåòñÿ íîâîé è ïðèâîäèòñÿ çäåñü äëÿ òîãî, ÷òîáû åå èäåþ èñ-
ïîëüçîâàòü äëÿ áîëåå ñëîæíûõ ïðåäèêàòíûõ ïðåîáðàçîâàòåëåé, äåéñòâóþùèõ íå
òîëüêî â ïðîñòûõ àòðèáóòíûõ òðàíçèöèîííûõ ñèñòåìàõ.
2. ÎÁÎÁÙÅÍÈß ÏÐÎÑÒÛÕ ÀÒÐÈÁÓÒÍÛÕ ÒÐÀÍÇÈÖÈÎÍÍÛÕ ÑÈÑÒÅÌ
Ïðîáëåìà ïîñòðîåíèÿ áîëåå ñëîæíûõ ïðåäèêàòíûõ ïðåîáðàçîâàòåëåé èìååò
íåñêîëüêî èçìåðåíèé, âëèÿþùèõ íà âîçìîæíîñòü èõ ïîñòðîåíèÿ:
i) èñïîëüçîâàíèå àòðèáóòîâ áîëåå ñëîæíîãî òèïà — ôóíêöèîíàëüíûõ àòðèáó-
òîâ, ÷àñòíûì ñëó÷àåì êîòîðûõ ÿâëÿþòñÿ àòðèáóòíûå ìàññèâû;
ii) ñïåöèôèêàöèÿ ïîñòóñëîâèé — èçìåíåíèå àòðèáóòîâ ìîæåò çàäàâàòüñÿ íå
ÿâíî â âèäå ïðèñâàèâàíèÿ, íî íåÿâíî â âèäå êîíñòðåéíòà (ôîðìóëû, îãðàíè÷èâàþ-
ùåé âîçìîæíûå çíà÷åíèÿ àòðèáóòà), îïðåäåëÿþùåãî öåëûé ñïåêòð âñåõ òàêèõ èçìå-
íåíèé. Âîçìîæíà òàêæå êîìáèíèðîâàííàÿ ñïåöèôèêàöèÿ, êîãäà èçìåíåíèå îäíîé
÷àñòè àòðèáóòîâ çàäàåòñÿ ïðèñâàèâàíèÿìè, à äðóãîé — ïîñðåäñòâîì êîíñòðåéíòîâ;
iii) èñïîëüçîâàíèå êîíñòðóêòîðîâ ñòðóêòóð äàííûõ, ïîçâîëÿþùèõ ñòðîèòü
ñïèñêè, î÷åðåäè, äåðåâüÿ íàä çíà÷åíèÿìè àòðèáóòîâ;
iv) ïàðàìåòðèçàöèÿ ïðàâèë ïåðåõîäîâ (ïàðàìåòðèçîâàííûå ïðàâèëà ïîçâîëÿ-
þò ââîäèòü â ôîðìóëó ñèìâîëüíîãî ñîñòîÿíèÿ ñâÿçàííûå ïåðåìåííûå, êîòîðûå áó-
äóò ó÷èòûâàòü îïðåäåëåííûå îãðàíè÷åíèÿ íà çíà÷åíèÿ àòðèáóòîâ è ñòðîèòü áîëåå
ñëîæíûå ôîðìóëû ñîñòîÿíèé).
Íèæå äåòàëüíåå ðàññìîòðèì ïðåäèêàòíûå ïðåîáðàçîâàòåëè äëÿ ATS, â îïèñà-
íèè êîòîðûõ èñïîëüçóþòñÿ àòðèáóòû ôóíêöèîíàëüíîãî òèïà, íî ïðåæäå ñäåëàåì
íåñêîëüêî çàìå÷àíèé îá îáîáùåíèÿõ äðóãèõ òèïîâ.  ñëó÷àå (ii), êîãäà ôîðìóëû
ïîÿâëÿþòñÿ â ïîñòóñëîâèè, ìîæíî âûäåëèòü èçìåíÿåìûå íåÿâíûì îáðàçîì àòðèáó-
òû è ñîîòâåòñòâåííî ñêîððåêòèðîâàòü ïðåîáðàçóåìóþ ôîðìóëó ïóòåì çàìåíû òàêèõ
àòðèáóòîâ ñâÿçàííûìè ïåðåìåííûìè, à äàëåå ðàññìàòðèâàòü êîíúþíêöèþ ïðåîáðà-
çóåìîé ôîðìóëû è ôîðìóëû èç ïîñòóñëîâèÿ. Ñëó÷àé (iii) èíòåðåñåí òåì, ÷òî çíà÷å-
íèÿ àòðèáóòîâ ìîãóò êîïèðîâàòüñÿ, êîãäà «ñòàðûå» (èçìåíåííûå) çíà÷åíèÿ àòðèáó-
òîâ ìîãóò ïîìåùàòüñÿ â ñïèñêè èëè î÷åðåäè è ñóùåñòâîâàòü îäíîâðåìåííî ñ âíîâü
ïðèñâîåííûìè ýòèì àòðèáóòàì çíà÷åíèÿìè. Ïðè ýòîì âîçìîæíûå êîëëèçèè, ó÷èòû-
âàþùèå ïîâòîðíîå âû÷èñëåíèå çíà÷åíèé, äîëæíû îòðàæàòüñÿ â ïðåîáðàçîâàííîì
ôîðìóëüíîì ñîñòîÿíèè òðàíçèöèîííîé ñèñòåìû.  ñëó÷àå (iv) èñïîëüçóþòñÿ áàçî-
âûå ïðîòîêîëû âèäà
( , , ) ( , , , , , ) ( , , , , ,� �
�x x u a a x x bp a a x xk m k m k1 1 1 1 1� � � � �� ) ,
ãäå ïåðåìåííûå x xk1 , ,� — ïàðàìåòðû ïðîòîêîëà. Èõ çíà÷åíèÿ çàâèñèìû îò çíà-
÷åíèé àòðèáóòîâ, âõîäÿùèõ â ôîðìóëó ïðåäóñëîâèÿ u, è çàòåì îò çíà÷åíèé ýòèõ ïà-
ðàìåòðîâ áóäóò çàâèñåòü íîâûå çíà÷åíèÿ àòðèáóòîâ, îïðåäåëÿåìûå ïîñòóñëîâèåì �.
Îòìåòèì åùå îäíî èçìåðåíèå, â êîòîðîì ðàññìàòðèâàåòñÿ çàäà÷à ñèìâîëüíîãî ìî-
äåëèðîâàíèÿ: ïðåäèêàòíûå ïðåîáðàçîâàòåëè ìîãóò èñïîëüçîâàòüñÿ íå òîëüêî ïðè ìîäå-
ëèðîâàíèè ïåðåõîäîâ îò òåêóùåãî ñîñòîÿíèÿ ê ïîñëåäóþùåìó (forward simulation), íî è
ïðè ìîäåëèðîâàíèè îáðàòíûõ ïåðåõîäîâ — îò òåêóùåãî ñîñòîÿíèÿ ê ïðåäøåñòâóþùåìó
(backward simulation). È åñëè ðàññìàòðèâàåìûå çäåñü ïðåîáðàçîâàòåëè ñîîòâåòñòâóþò
âû÷èñëåíèþ ñèëüíåéøåãî ïîñòóñëîâèÿ, òî ïðåîáðàçîâàòåëè, ìîäåëèðóþùèå îáðàò-
íûå ïåðåõîäû, ñîîòâåòñòâóþò ïîñòðîåíèþ ñëàáåéøåãî ïðåäóñëîâèÿ.1
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 95
1Çäåñü ïîíÿòèÿ ïîñòóñëîâèÿ è ïðåäóñëîâèÿ îòëè÷àþòñÿ îò, ôèãóðèðóþùèõ â îïðåäåëåíèè áàçîâûõ
ïðîòîêîëîâ, è ñîîòâåòñòâóþò ðåçóëüòàòàì ïðÿìîãî è îáðàòíîãî ïðåîáðàçîâàíèé ôîðìóë.
3. ATS Ñ ÀÒÐÈÁÓÒÀÌÈ ÔÓÍÊÖÈÎÍÀËÜÍÎÃÎ ÒÈÏÀ
Àòðèáóòû ýòîãî òèïà õàðàêòåðèçóþòñÿ àðíîñòüþ, òèïàìè àðãóìåíòîâ (èíäåêñîâ)
è òèïîì çíà÷åíèé. Åñëè àòðèáóò a èìååò àðíîñòü n, åãî àðãóìåíòû ïðèíèìàþò
çíà÷åíèÿ â äîìåíàõ D Dn1 , ,� , çíà÷åíèÿ ñàìîãî àòðèáóòà äëÿ íàáîðîâ èç
D Dn1 � �� îòíîñÿòñÿ ê äîìåíó D, òî çíà÷åíèÿìè àòðèáóòà ÿâëÿþòñÿ ôóíêöèè èç
D
D Dn1� ��
. Îáúåêòû ýòîãî âèäà ñîîòâåòñòâóþò òàêæå ôóíêöèîíàëüíûì ñèìâîëàì
ñèãíàòóðû � è ñîïîñòàâëÿþòñÿ èì èíòåðïðåòàöèåé I. Îäíàêî èìååòñÿ ðàçëè÷èå
ìåæäó ôóíêöèîíàëüíûìè àòðèáóòàìè è ôóíêöèîíàëüíûìè ñèìâîëàìè ñèãíàòó-
ðû, êîòîðîå ñîñòîèò â òîì, ÷òî èíòåðïðåòàöèÿ ôóíêöèîíàëüíûõ ñèìâîëîâ îñòà-
åòñÿ íåèçìåííîé ïðè âûïîëíåíèè ïåðåõîäîâ â òðàíçèöèîííîé ñèñòåìå, à çíà÷å-
íèÿ ôóíêöèîíàëüíûõ àòðèáóòîâ ìîãóò èçìåíÿòüñÿ ïîñðåäñòâîì ïðèìåíåíèÿ
áàçîâûõ ïðîòîêîëîâ.
Èñïîëüçîâàíèå ôóíêöèîíàëüíûõ àòðèáóòîâ ïðè ñïåöèôèêàöèè áàçîâûõ ïðîòî-
êîëîâ ìîæåò âûçâàòü ïðîòèâîðå÷èÿ â ïðèìåíåíèè ñàìèõ ïðîòîêîëîâ èç-çà âîçìîæ-
íûõ êîëëèçèé ìåæäó ëåâûìè ÷àñòÿìè ïðèñâàèâàíèé â ïîñòóñëîâèè ïðîòîêîëà.
Åñëè ëåâûå ÷àñòè äâóõ îïåðàòîðîâ ïðèñâàèâàíèÿ îòíîñÿòñÿ ê îäíîìó è òîìó æå
ôóíêöèîíàëüíîìó àòðèáóòó è îòëè÷àþòñÿ ëèøü ðàçíûìè àðãóìåíòàìè, íàïðèìåð
a t ak( , , )1 � è a t ak( , , )� �1 � , òî ñëåäóåò áûòü óâåðåííûì, ÷òî äëÿ ëþáîãî äîñòèæè-
ìîãî ñîñòîÿíèÿ òðàíçèöèîííîé ñèñòåìû âåêòîðû çíà÷åíèé àðãóìåíòîâ áóäóò
ðàçëè÷íûìè. Àòðèáóòíûå òåðìû, ó êîòîðûõ ñîâïàäàåò ñèìâîë ãëàâíîãî àòðèáóòà,
áóäåì íàçûâàòü ïîäîáíûìè.
Ïðåäïîëîæèì, ÷òî êîëëèçèè, ñâÿçàííûå ñ ïîäîáèåì àòðèáóòíûõ òåðìîâ â ëå-
âûõ ÷àñòÿõ ïðèñâàèâàíèé, èñêëþ÷åíû. Ýòî ñâÿçàíî ñ òåì, ÷òî ïðè ñèìâîëüíîì ìî-
äåëèðîâàíèè ïðîöåññîâ â ATS ïðèìåíåíèå ïðåäèêàòíûõ ïðåîáðàçîâàòåëåé êàê ðàç
è íàöåëåíî íà ïðîâåðêó äîñòèæèìîñòè âñÿêîãî ðîäà ïðîòèâîðå÷èâûõ ñîñòîÿíèé,
è ýòà ïðîâåðêà îïðåäåëåííûì îáðàçîì âñòðàèâàåòñÿ â ïðîöåññ ïîðîæäåíèÿ ôîð-
ìóëüíûõ ñîñòîÿíèé ìîäåëè. Ïðîâåðêà âûïîëíèìîñòè äëÿ ôîðìóë ñ ôóíêöèîíàëü-
íûìè àòðèáóòàìè îòëè÷àåòñÿ òåì, ÷òî ïðè âû÷èñëåíèè çíà÷åíèÿ ôîðìóë äîëæåí
ñîáëþäàòüñÿ ïðèíöèï ôóíêöèîíàëüíîñòè, êîòîðûé âûðàæàåòñÿ ñîîòíîøåíèÿìè
âèäà t t a t a t1 2 1 2� � �( ) ( ) , ðàññìàòðèâàåìûõ Ð. Øîñòàêîì [7]. Ñ ýòîé öåëüþ
ê ôîðìóëå, ïðîâåðÿåìîé íà âûïîëíèìîñòü, äîáàâëÿþò òàêèå ñîîòíîøåíèÿ äëÿ êàæ-
äîé ïàðû âõîäÿùèõ â íåå ïîäîáíûõ àòðèáóòíûõ òåðìîâ. Êàê è ðàíåå, äëÿ ñëó÷àÿ
ïðîñòûõ òðàíçèöèîííûõ àòðèáóòíûõ ñèñòåì áóäåì ïðåäïîëàãàòü, ÷òî ïðîáëåìà
ïðîâåðêè ôîðìóë íà âûïîëíèìîñòü ðàçðåøèìà.
Ïóñòü çàäàíû ôîðìóëà F a am( , , )1 � è áàçîâûé ïðîòîêîë u a am( , , )1 � �
�
�bp a am�( , , )1 � , çàâèñÿùèå îò àòðèáóòîâ èç ìíîæåñòâà A. Ïóñòü
a t a tk k1 1( ) , , ( )� — âñå ëåâûå ÷àñòè îïåðàòîðîâ ïðèñâàèâàíèÿ â ïðîòîêîëå bp, è
t t k1 , ,� — âåêòîðû àðãóìåíòîâ ïðè ñîîòâåòñòâóþùèõ ôóíêöèîíàëüíûõ àòðèáóòàõ.
 ôîðìóëå ïðåäèêàòíîãî ïðåîáðàçîâàòåëÿ pt F u( & , )� , ðàññìîòðåííîé âûøå äëÿ
ñëó÷àÿ ñêàëÿðíûõ àòðèáóòîâ, àòðèáóòíûå òåðìû, ïîäîáíûå òåðìàì èç ñïèñêà
a t a tk k1 1( ) , , ( )� , ìîãëè âñòðå÷àòüñÿ â ôîðìóëå F u& , à òàêæå â ïðàâûõ ÷àñòÿõ
ïðèñâàèâàíèé.  ñëó÷àå ñ ïðèìåíåíèåì ôóíêöèîíàëüíûõ àòðèáóòîâ àòðèáóò, ïî-
äîáíûé äàííîìó, ìîæåò âñòðå÷àòüñÿ òàêæå è â òåðìàõ t t k1 , ,� , êîòîðûå ÿâëÿþòñÿ
àðãóìåíòàìè ëåâûõ ÷àñòåé.
Ïóñòü a t( )� — òåðì, ïîäîáíûé òåðìó a t( ) , îäíîé èç ëåâûõ ÷àñòåé ïðèñâàèâà-
íèÿ �, è òàêîé, ÷òî îí âõîäèò ëèáî â F u& , ëèáî â ïðàâóþ ÷àñòü îäíîãî èç ïðèñâàè-
âàíèé, ëèáî â îäèí èç àðãóìåíòîâ îäíîãî èç òåðìîâ â ëåâîé ÷àñòè ïðèñâàèâàíèÿ.
Òîãäà çíà÷åíèå ýòîãî òåðìà a t( )� ïîä äåéñòâèåì ïðèñâàèâàíèÿ a t tt( ):� ìîæåò èçìå-
íèòüñÿ èëè îñòàòüñÿ íåèçìåííûì â çàâèñèìîñòè îò òîãî, èìåëî ëè ìåñòî ðàâåíñòâî
t t� � ïåðåä âûïîëíåíèåì áàçîâîãî ïðîòîêîëà. ×òîáû ðàçäåëèòü ýòè äâà ñëó÷àÿ, ââå-
äåì ôîðìóëó ( )t t t t� � � � � , êîòîðàÿ, ñ îäíîé ñòîðîíû, òîæäåñòâåííî ðàâíà åäèíè-
öå, à ñ äðóãîé, ïîçâîëèò ðàññìàòðèâàòü îòäåëüíî òðàíñôîðìàöèþ ôîðìóë F t t&( )� �
è F t t&( )� � .
96 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
Ïîñòðîèì êîíúþíêöèþ èç âñåõ ôîðìóë âèäà ( )t t t t� � � � � , îáðàçóåìûõ äëÿ
âñåõ ïàð ïîäîáíûõ àòðèáóòíûõ òåðìîâ, îäèí èç êîòîðûõ îòíîñèòñÿ ê ëåâîé ÷àñòè
ïðèñâàèâàíèÿ, à äðóãîé ÿâëÿåòñÿ âõîæäåíèåì â îäèí èç âû÷èñëÿåìûõ òåðìîâ. Ïî
ïîñòðîåíèþ ýòà êîíúþíêöèÿ ðàâíà åäèíèöå. Ðàñêðîåì ñêîáêè è ïîñòðîèì ä.í.ô.,
äèçúþíêòû êîòîðîé ñîäåðæàò ïîäôîðìóëû âèäà ( )&...&( )&� � � � � �t t t ti i im im1 1
&( )&...&( )� � � � � �t t t tj j jk jk1 1 , íàçûâàåìûå çäåñü êëàññèôèêàòîðàìè è îáîçíà÷àå-
ìûå clfi , ãäå i — íîìåð êëàññèôèêàòîðà. Íàñ áóäóò èíòåðåñîâàòü òîëüêî âûïîëíè-
ìûå êëàññèôèêàòîðû, à íåâûïîëíèìûå, ñîäåðæàùèå êîíúþíêòèâíûå âçàèìíî ïðî-
òèâîðå÷èâûå ñîìíîæèòåëè, áóäåì èñêëþ÷àòü. Ýòî âîçìîæíî â ñèëó ïðåäïîëîæåíèÿ
î òîì, ÷òî äëÿ ôîðìóë ñ äàííîé ñèãíàòóðîé èìååòñÿ ðàçðåøèìàÿ ïðîöåäóðà ïðîâåð-
êè âûïîëíèìîñòè.  êëàññèôèêàòîðå áóäåì ðàçëè÷àòü ïîçèòèâíóþ ÷àñòü
( )&...&( )� � � � � �t t t ti i im im1 1 , ñîñòîÿùóþ èç ðàâåíñòâ, è îãðàíè÷èòåëüíóþ
( )&...&( )� � � � � �t t t tj j jk jk1 1 , ñîñòîÿùóþ èç îòðèöàíèé ðàâåíñòâ.
Ïîñêîëüêó êëàññèôèêàòîðû ïîïàðíî íå ñîâìåñòèìû è â ñîâîêóïíîñòè ïðåä-
ñòàâëÿþò òîæäåñòâåííóþ ôîðìóëó, ïðåîáðàçîâàíèå ôîðìóëû F áóäåì ñâîäèòü ê
ïðåîáðàçîâàíèþ ôîðìóë âèäà F clfi& . Îïèøåì ïîñòðîåíèå ôîðìóëû
pt F clf ui( & & , )� , ïðè ýòîì àêöåíò ñäåëàåì íà ôóíêöèîíàëüíûõ àòðèáóòàõ, ïî-
ñêîëüêó ýôôåêò îò ïðèñâàèâàíèé ñî ñêàëÿðíûìè àòðèáóòàìè â ëåâîé ÷àñòè áóäåò
òàêèì æå êàê è â ðàçäåëå âûøå.
Ïîñòðîåíèå ôîðìóëû pt F t t t t t ti i im im j j( &( )&...&( )&( )&...� � � � � �1 1 1 1
...&( )& , )� �t t ujk jk � , êàê è ðàíåå, äëÿ ôîðìóë ñî ñêàëÿðíûìè àòðèáóòàìè ïðîâî-
äèòñÿ â äâà ýòàïà:
• äëÿ òåðìîâ îáðàçóåòñÿ ñïèñîê ñâåæèõ (fresh) ïåðåìåííûõ, ñâÿçûâàåìûõ çà-
òåì êâàíòîðàìè ñóùåñòâîâàíèÿ, è ñòðîèòñÿ ïîäñòàíîâêà, ãäå êàæäîìó òåðìó a t( ) ,
ÿâëÿþùåìóñÿ ëåâîé ÷àñòüþ îäíîãî èç ïðèñâàèâàíèé, ñîïîñòàâëÿåòñÿ ïåðåìåííàÿ x ;
• â ïðåîáðàçóåìîé ôîðìóëå âûäåëÿþòñÿ ôóíêöèîíàëüíûå àòðèáóòû, çíà÷åíèÿ
êîòîðûõ ñîãëàñíî ðàâåíñòâàì èç ïîçèòèâíîé ÷àñòè êëàññèôèêàòîðà áóäóò èçìåíå-
íû. Ñîãëàñíî ñåìàíòèêå âû÷èñëåíèå çíà÷åíèé ôóíêöèé ïðîèñõîäèò â òàêîì ïîðÿä-
êå: ñíà÷àëà âû÷èñëÿþòñÿ çíà÷åíèÿ âñåõ åå àðãóìåíòîâ, à çàòåì, èñõîäÿ èç ýòèõ çíà-
÷åíèé, âû÷èñëÿåòñÿ çíà÷åíèå ñàìîé ôóíêöèè. Ïîýòîìó îáõîä ïðåîáðàçóåìîé ôîð-
ìóëû íà÷èíàåì ñâåðõó âíèç, îòûñêèâàÿ àòðèáóòíûå òåðìû, ïîäîáíûå òåðìàì â
ëåâûõ ÷àñòÿõ ïðèñâàèâàíèÿ. Åñëè íàõîäèòñÿ àòðèáóòíûé òåðì a t( )� , òî åãî ñïèñîê
àðãóìåíòîâ ëèáî óäîâëåòâîðÿåò t t� � , îäíîìó èç ðàâåíñòâ â ïîçèòèâíîé ÷àñòè êëàñ-
ñèôèêàòîðà, ëèáî îòðèöàíèþ t t� � îäíîãî èç ðàâåíñòâ îãðàíè÷èòåëüíîé ÷àñòè ïî-
ñëåäíåãî.  ïåðâîì ñëó÷àå òåðì a t( )� çàìåíÿåì ñâÿçàííîé ïåðåìåííîé, ñîîòâåòñòâó-
þùåé òåðìó a t( ) , âî âòîðîì îáõîä ïðåîáðàçóåìîé ôîðìóëû ïðîäîëæàåòñÿ, íà÷èíàÿ
ñ àðãóìåíòîâ òåðìà a t( )� .
Òàêèì îáðàçîì, ïîëó÷àåì ôîðìóëó äëÿ ïðåäèêàòíîãî ïðåîáðàçîâàòåëÿ:
pt F u x x F clf u a t
clf
k i i i
i
( & , ) ( , , ) ( & & &( ( )� �� � � � � � �� 1 1 1� t i1 )&...
...&( ( ) )a ttik ik ik� � � , (1)
ãäå F clf ui� � �, , — ôîðìóëû, ïîëó÷åííûå èç F clfi, è u â ðåçóëüòàòå çàìåíû íåêî-
òîðûõ àòðèáóòíûõ òåðìîâ ñâÿçàííûìè ïåðåìåííûìè èç ìíîæåñòâà { }x xk1 , ,� .
Ïðèìåíåíèå ýòîé æå ïðîöåäóðû ê t ti ik1 , ,� , íàáîðàì àðãóìåíòîâ â ëåâûõ ÷àñ-
òÿõ îïåðàòîðà �, ïðåîáðàçóåò èõ ê íàáîðàì � �i ik1 , ,� , âîçìîæíî, ñîäåðæàùèì
ñâÿçàííûå ïåðåìåííûå, è íàêîíåö, tt tti ik� �1 , ,� — ýòî òðàíñôîðìèðîâàííûå ïðà-
âûå ÷àñòè îïåðàòîðîâ ïðèñâàèâàíèÿ.
Òåîðåìà 2. Ïðåîáðàçîâàòåëü pt (*,*) èäåàëüíûé äëÿ òðàíçèöèîííûõ ñèñòåì ñ
ôóíêöèîíàëüíûìè àòðèáóòàìè.
Êàê è ðàíåå, â ñëó÷àå òåîðåìû 1, áóäåì äîêàçûâàòü êîììóòàòèâíîñòü äèàãðàì-
ìû, ïðåäñòàâëåííîé íà ðèñ. 1, ò.å. äîêàæåì ñëåäóþùèå äâà óòâåðæäåíèÿ:
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 97
à) åñëè s bp s� � ( ) è F u clf& & âûïîëíèìà íà s, òî F pt F u� � ( & , )� äîëæíà áûòü
âûïîëíèìà íà s�;
á) åñëè F pt F u� � ( & , )� è F� âûïîëíèìà íà íåêîòîðîì s�, òî ñóùåñòâóåò s òàêîå,
÷òî s bp s� � ( ) è F u& âûïîëíèìà íà s.
Äîêàæåì à). Ïóñòü s F u( & ) è clf — òîò åäèíñòâåííûé êëàññèôèêàòîð, êîòîðûé
âûïîëíèì íà s, ò.å. òàêîé, ÷òî s clf( ) . Äëÿ êàæäîãî ïðèñâàèâàíèÿ a t ti i( ):� � , âõîäÿ-
ùåãî â �, îïðåäåëèì c s t i� ( ) , íàáîð àðãóìåíòîâ ôóíêöèîíàëüíîãî àòðèáóòíîãî òåð-
ìà a t i( ) , êîíêðåòèçèðîâàííûõ â ñîñòîÿíèè s, è d s t i� �( ) — êîíêðåòèçèðîâàííîå
çíà÷åíèå ïðàâîé ÷àñòè ýòîãî ïðèñâàèâàíèÿ. Ïóñòü xi — ñèìâîë ïåðåìåííîé, èñ-
ïîëüçóåìûé ïðè ïîñòðîåíèè ôîðìóëû pt F u( & , )� äëÿ çàìåíû òåðìîâ âèäà a t( ) ,
íàáîð àðãóìåíòîâ êîòîðûõ âõîäèò â âèäå ðàâåíñòâà t t i� â êëàññèôèêàòîð clf .
Ïî ïîñòðîåíèþ pt F u( & , )� äåéñòâèå êëàññèôèêàòîðà clf , èñòèííîãî â ñîñòîÿ-
íèè s, òàêîâî, ÷òî âñÿêèé àòðèáóòíûé ïîäòåðì a t( ) , òàêîé ÷òî ðàâåíñòâî t t i� êîíú-
þíêòèâíî âõîäèò â clf , áóäåò çàìåíåí ñèìâîëîì xi , ñîîòâåòñòâóþùèì àòðèáóòíîìó
òåðìó a t i( ) èç ëåâîé ÷àñòè îäíîãî èç ïðèñâàèâàíèé â �. Ïóñòü
( , , ) ( & & &( ( ) )&...&( ( )� � � � � � � �x x F clf u a tt a tk k k1 1 1 1� � � t k )) (2)
— äèçúþíêò èç (1), êëàññèôèêàòîð êîòîðîãî clf èñòèíåí â ñîñòîÿíèè s. Íà ìíî-
æåñòâå X x xk� { }1 , ,� ñâÿçàííûõ ïåðåìåííûõ îïðåäåëèì îòîáðàæåíèå �: X D�
òàêîå, ÷òî �( ) ( ( ))x d s a ti i i� � . Çàìåíèì â (2) ïåðåìåííûå èç X çíà÷åíèÿìè, êî-
òîðûå èì ñîïîñòàâëÿåò îòîáðàæåíèå �. Òîãäà ïî ïîñòðîåíèþ pt F u( & , )� âåðíî
ñëåäóþùåå:
• âñå àòðèáóòíûå ïîäòåðìû èç � � �( ), ( ), ( )F u clf� � � è � �( )ij , ïîäîáíûå òåð-
ìàì a ak k1 1( ), , ( )� �� , â ñîñòîÿíèè s áóäóò èìåòü äðóãèå íàáîðû êîíêðåòíûõ àðãó-
ìåíòîâ, ÷åì òåðìû a ak k1 1( ), , ( )� �� ;
• çíà÷åíèÿ s F( ) è s u( ) ñîâïàäàþò ñî çíà÷åíèÿìè s F( ( ))� � è s u( ( ))� � ñîîòâå-
òñòâåííî;
• s clf( ) âûïîëíèìî ñîãëàñíî âûáîðó êëàññèôèêàòîðà èç èõ ìíîæåñòâà;
• ðàâåíñòâà âèäà a ttj j j( ):� � � îïðåäåëÿþò íîâûå çíà÷åíèÿ ôóíêöèîíàëüíûõ
àòðèáóòîâ â ñîñòîÿíèè s è èõ êîððåêòíîñòü ñëåäóåò èç òîãî, ÷òî ðåêóðñèÿ â íèõ èñ-
êëþ÷åíà â ñèëó ïåðâîãî â ýòîì ïåðå÷èñëåíèè óòâåðæäåíèÿ.
 ñîâîêóïíîñòè ýòè ÷åòûðå óòâåðæäåíèÿ ïîçâîëÿþò çàêëþ÷èòü, ÷òî ôîðìó-
ëà (2), à òàêæå pt F u( & , )� , áóäåò âûïîëíèìà â ñîñòîÿíèè s�, êîòîðîå îòëè÷àåòñÿ îò
s òîëüêî çíà÷åíèÿìè ôóíêöèîíàëüíûõ àòðèáóòîâ a ai ik1 , ,� äëÿ íàáîðîâ êîíêðåò-
íûõ àðãóìåíòîâ, ñîîòâåòñòâåííî ðàâíûõ s s k( ( )), , ( ( ))� � � �1 � .
Äîêàæåì á). Ïóñòü s A D� �: è �: , ,{ }x x Dk1 � � òàêîâû, ÷òî ôîðìóëà
pt F u( & , )� âûïîëíèìà â ñîñòîÿíèè s�*�. Â ýòîé ôîðìóëå âûäåëèì òîò åäèíñòâåí-
íûé êëàññèôèêàòîð clf , êîòîðûé âûïîëíÿåòñÿ ïðè çàäàííûõ s� è �, à òàêæå ñîîòâåò-
ñòâóþùèé äèçúþíêò, ïðåäñòàâëÿåìûé ôîðìóëîé (2). Êàæäàÿ ïåðåìåííàÿ xi â (2) ïî
ïîñòðîåíèþ çàìåíÿåò çíà÷åíèå àòðèáóòíîãî òåðìà, ÷üè àðãóìåíòû ñîâïàäàþò ñî-
ãëàñíî âûáðàííîìó êëàññèôèêàòîðó ñ àðãóìåíòàìè òåðìà a t i( ). Ýòî çàìå÷àíèå ïî-
çâîëÿåò èíòåðïðåòèðîâàòü çíà÷åíèÿ d xi i� �( ) êàê çíà÷åíèÿ àòðèáóòà ai
â ñîñòîÿíèè ( * )s t i� � .
Åñëè â ôîðìóëå F u clf� � �& & èëè ñðåäè íàáîðîâ òåðìîâ � �1 , ,� k , àðãóìåíòîâ
ôóíêöèîíàëüíûõ àòðèáóòîâ èç ëåâûõ ÷àñòåé ïðèñâàèâàíèÿ �, âñòðå÷àåòñÿ àòðèáóò-
íûé òåðì a t( ) , òî çíà÷åíèå ( * )s t� � , êîíêðåòèçàöèÿ åãî àðãóìåíòîâ â s�*�, áóäåò îò-
ëè÷àòüñÿ îò çíà÷åíèé ( * )s t i� � äëÿ i k� 1, ,� . Äåéñòâèòåëüíî, ïî ïîñòðîåíèþ êëàñ-
ñèôèêàòîð clf äîëæåí ñîäåðæàòü ëèáî ðàâåíñòâî t t i� , ëèáî åãî îòðèöàíèå. Ïðîöå-
äóðà çàìåíû àòðèáóòíûõ ïîäòåðìîâ äëÿ òåðìîâ t è t i íà ïåðåìåííûå èç X
ñîõðàíÿåò îòíîøåíèÿ = èëè � ìåæäó òåðìàìè a t( ) è a t i( ) , ïîýòîìó âõîæäåíèÿ àò-
ðèáóòíîãî òåðìà a t( ) ïðè êîíêðåòèçàöèè s�*� íå ïðîòèâîðå÷èò ðàâåíñòâàì
a t tti i i( ) � � .
Ïîñëåäíåå çàìå÷àíèå ïîçâîëÿåò çàìåíèòü âõîæäåíèÿ ïåðåìåííûõ èç X èõ çíà-
÷åíèÿìè, îïðåäåëÿåìûìè îòîáðàæåíèåì �. Åñëè äàëåå îïðåäåëèòü çíà÷åíèÿ ôóíê-
98 ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4
öèîíàëüíûõ àòðèáóòîâ a i ki , , ,� 1 � , äëÿ íàáîðîâ àðãóìåíòîâ t i êàê ( * )s t i� � , òî ïî-
ëó÷èì íîâîå ñîñòîÿíèå s. Ýòî ñîñòîÿíèå îòëè÷àåòñÿ îò s� òîëüêî çíà÷åíèÿìè àòðè-
áóòîâ ai äëÿ êîíêðåòíûõ íàáîðîâ àðãóìåíòîâ ( * )s t i� � è, ñëåäîâàòåëüíî, ôîðìóëà
F u clf& & áóäåò âûïîëíèìîé â ñîñòîÿíèè s. Íåòðóäíî òàêæå ïîíÿòü, ÷òî ñîñòîÿíèÿ
s è s� óäîâëåòâîðÿþò ñîîòíîøåíèþ s bp s� � ( ) , ÷òî è äîêàçûâàåò òåîðåìó 2.
Òåîðåìà 2 óòâåðæäàåò, ÷òî ïðåîáðàçîâàòåëü pt ÿâëÿåòñÿ ñèëüíåéøèì ïîñòóñëî-
âèåì â ñìûñëå [2] äëÿ àòðèáóòíûõ òðàíçèöèîííûõ ñèñòåì ñ ôóíêöèîíàëüíûìè
àòðèáóòàìè.
Çàìåòèì, ÷òî ñîñòîÿíèå s� ìîæåò áûòü íå åäèíñòâåííûì, ãäå âûïîëíÿåòñÿ
pt F u( & , )� , è áîëåå òîãî, îíî çàâèñèò îò âûáîðà îòîáðàæåíèÿ �, äåéñòâóþùåãî íà
ìíîæåñòâå ñâÿçàííûõ ïåðåìåííûõ X . Åñëè òàêèõ ñîñòîÿíèé s�, óäîâëåòâîðÿþùèõ
ôîðìóëå pt F u( & , )� , íåñêîëüêî, òî ñîîòâåòñòâåííî áóäåò ñòîëüêî æå ñîñòîÿíèé s,
íà êîòîðûõ âûïîëíèìà ôîðìóëà F.
ÇÀÊËÞ×ÅÍÈÅ
Ñ òî÷êè çðåíèÿ êîìáèíàòîðíîé ñëîæíîñòè ôîðìóëà pt F u( & , )� ìîæåò îêàçàòüñÿ
ãðîìîçäêîé, ïîñêîëüêó êîëè÷åñòâî êëàññèôèêàòîðîâ ðàñòåò ýêñïîíåíöèàëüíî ïî
îòíîøåíèþ ê ÷èñëó ïàð ïîäîáíûõ àòðèáóòíûõ òåðìîâ. Îäíàêî â ïðàêòè÷åñêîì
ïëàíå òàêèõ ïàð ïîäîáíûõ àòðèáóòíûõ òåðìîâ, âî-ïåðâûõ, ìîæåò áûòü îòíîñè-
òåëüíî íåìíîãî è, âî-âòîðûõ, áîëüøèíñòâî êëàññèôèêàòîðîâ ìîæåò îêàçàòüñÿ
òîæäåñòâåííî íåâûïîëíèìûìè ôîðìóëàìè. Íàïðèìåð, êëàññèôèêàòîð ìîæåò ñî-
äåðæàòü ðàâåíñòâà ( , ) ( , )1 2 1 2� t t è ( , ) ( , )3 4 3 2� t t , êîòîðûå íåñîâìåñòèìû, òàê
êàê íå óäîâëåòâîðÿþòñÿ íè ïðè êàêîì çíà÷åíèè òåðìà t2 .
Äàæå ïðè âûñîêîé êîìáèíàòîðíîé ñëîæíîñòè ïðèìåíåíèå ïîäîáíîãî ïðåäè-
êàòíîãî ïðåîáðàçîâàòåëÿ äëÿ ñèìâîëüíîãî ìîäåëèðîâàíèÿ àòðèáóòíûõ òðàíçèöèîí-
íûõ ñèñòåì îïðàâäàíî, åñëè ðàññìàòðèâàòü ïðèëîæåíèÿ, ãäå ïðîöåññû â ñèñòåìå îò-
íîñèòåëüíî êîðîòêèå, íî â êàæäîé òî÷êå èìååòñÿ áîëüøîå ÷èñëî âàðèàíòîâ äëÿ
ïðîäîëæåíèÿ ïðîöåññà.  ýòîì ñëó÷àå ïðîöåññ ìîæåò ìîäåëèðîâàòüñÿ íà óðîâíå
ôîðìóë F Fn1 , ,� , êîòîðûå íà êàæäîì øàãå áóäóò ñîïîñòàâëÿòüñÿ ñ íåêîåé öåëåâîé
ôîðìóëîé G, ÷òî áóäåò âûðàæàòüñÿ â ïðîâåðêå âûïîëíèìîñòè êîíúþíêöèé ýòèõ
ôîðìóë ñ G. Åñëè íà êàêîì-òî øàãå òàêàÿ êîíúþíêöèÿ âûïîëíèìà, ò.å. ñóùåñòâóåò
ñîñòîÿíèå s* òàêîå, ÷òî s F Gn
* ( & ) , òî âñòàåò çàäà÷à îáðàòíîãî ìîäåëèðîâàíèÿ,
êîãäà êîíñòðóèðóåòñÿ òðàññà, âåäóùàÿ îò íåêîåãî äîïóñòèìîãî íà÷àëüíîãî
ñîñòîÿíèÿ ê íàéäåííîìó êðèòè÷åñêîìó ñîñòîÿíèþ s* .
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. F l o y d R . W . Assigning meaning to programs, in proceedings of symposium on applied mathematics /
J.T. Schwartz (Ed.), A.M.S. — 1967. — 19. — P. 19–32.
2. H o a r e C . A . R . An axiomatic basis for computer programming // Com. of the ACM. — 1969. — 12,
N 10. — P. 576–580,
3. L a m p o r t L . win and sin: predicate transformer for concurrency // ACM Transl. on Program. Language
and System (TOPLAS). — 1990. — 12, N 3. — P. 396–428.
4. C l a r k e E . M . , E m e r s o n E . A . Design and synthesis of synchronization skeletons using branching
time temporal logic // Logics of Programs: Workshop (Yoktown Heights, NY). — May 1981. — 131. —
P. 52–71.
5. L e t i c h e v s k y A . , G i l b e r t D . A model for interaction of agents and environments // Lecture Notes
In Comput. Scie. — 1999. — 1827. — P. 311–328.
6. Ñ ï å ö è ô è ê à ö è ÿ ñèñòåì ñ ïîìîùüþ áàçîâûõ ïðîòîêîëîâ / À.À. Ëåòè÷åâñêèé, Þ.Â. Êàïèòîíîâà,
Â.À. Âîëêîâ è äð. // Êèáåðíåòèêà è ñèñòåìíûé àíàëèç. — 2005. — ¹ 4. — C. 3–21.
7. S h o s t a k R . A practical decision procedure for arithmetic with function symbols // J. of the Assoñ. for
Comput. Machinery. — 1979. — 26, N 2. — P. 351–360.
Ïîñòóïèëà 09.04.2010
ISSN 0023-1274. Êèáåðíåòèêà è ñèñòåìíûé àíàëèç, 2010, ¹ 4 99
|
| id | nasplib_isofts_kiev_ua-123456789-45246 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0023-1274 |
| language | Russian |
| last_indexed | 2025-12-07T16:27:32Z |
| publishDate | 2010 |
| publisher | Інститут кібернетики ім. В.М. Глушкова НАН України |
| record_format | dspace |
| spelling | Годлевский, А.Б. 2013-06-10T16:28:43Z 2013-06-10T16:28:43Z 2010 Предикатные преобразователи в контексте символьного моделирования транзиционных систем / А.Б. Годлевский // Кибернетика и системный анализ. — 2010. — № 4. — С. 91-99. — Бібліогр.: 7 назв. — рос. 0023-1274 https://nasplib.isofts.kiev.ua/handle/123456789/45246 519.172 При моделюванні атрибутних транзиційних систем класи їх станів описуються за допомогою формул логіки в заданій сигнатурі функціональних та предикатних символів. Побудовано процедуру перетворення таких формул під дією операторів присвоювання та доведено, що трансформовані формули відповідають найсильнішим післяумовам. Особливістю роботи є можливість використання атрибутів функціонального типу в описах транзиційних систем, зокрема імен масивів. For modelling, the classes of states of attribute transition system can be described in a given signature of functional and predicate symbols. A procedure of transforming such formulas by assignment operators is developed and the resulted formulas are proved to correspond to strongest postconditions. A peculiarity of the paper is that functional-type attributes can be used in the specification of transition systems, especially array-type attributes. ru Інститут кібернетики ім. В.М. Глушкова НАН України Кибернетика и системный анализ Кибернетика Предикатные преобразователи в контексте символьного моделирования транзиционных систем Предикатні перетворювачі в контексті символьного моделювання транзиційних систем Predicate transformers in the context of symbolic modeling of transition systems Article published earlier |
| spellingShingle | Предикатные преобразователи в контексте символьного моделирования транзиционных систем Годлевский, А.Б. Кибернетика |
| title | Предикатные преобразователи в контексте символьного моделирования транзиционных систем |
| title_alt | Предикатні перетворювачі в контексті символьного моделювання транзиційних систем Predicate transformers in the context of symbolic modeling of transition systems |
| title_full | Предикатные преобразователи в контексте символьного моделирования транзиционных систем |
| title_fullStr | Предикатные преобразователи в контексте символьного моделирования транзиционных систем |
| title_full_unstemmed | Предикатные преобразователи в контексте символьного моделирования транзиционных систем |
| title_short | Предикатные преобразователи в контексте символьного моделирования транзиционных систем |
| title_sort | предикатные преобразователи в контексте символьного моделирования транзиционных систем |
| topic | Кибернетика |
| topic_facet | Кибернетика |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/45246 |
| work_keys_str_mv | AT godlevskiiab predikatnyepreobrazovatelivkontekstesimvolʹnogomodelirovaniâtranzicionnyhsistem AT godlevskiiab predikatníperetvorûvačívkontekstísimvolʹnogomodelûvannâtranzicíinihsistem AT godlevskiiab predicatetransformersinthecontextofsymbolicmodelingoftransitionsystems |