Инсерционное моделирование
Представлен обзор современного состояния инсерционного моделирования – направления, которое развивается на протяжении последнего десятилетия как подход к построению общей теории взаимодействия агентов и сред в сложных распределенных многоагентных системах. The review of the current state of insertio...
Збережено в:
| Опубліковано в: : | Управляющие системы и машины |
|---|---|
| Дата: | 2012 |
| Автор: | |
| Формат: | Стаття |
| Мова: | Російська |
| Опубліковано: |
Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
2012
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/83102 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Инсерционное моделирование / А.Ад. Летичевский // Управляющие системы и машины. — 2012. — № 6. — С. 3-14. — Бібліогр.: 32 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860168273464655872 |
|---|---|
| author | Летичевский, А.Ад. |
| author_facet | Летичевский, А.Ад. |
| citation_txt | Инсерционное моделирование / А.Ад. Летичевский // Управляющие системы и машины. — 2012. — № 6. — С. 3-14. — Бібліогр.: 32 назв. — рос. |
| collection | DSpace DC |
| container_title | Управляющие системы и машины |
| description | Представлен обзор современного состояния инсерционного моделирования – направления, которое развивается на протяжении последнего десятилетия как подход к построению общей теории взаимодействия агентов и сред в сложных распределенных многоагентных системах.
The review of the current state of insertion modeling, – the direction which developed over the last decade as an approach to the construction of a general theory of the interaction of agents and environments in complex distributed multi-agent systems is presented.
Подано огляд сучасного стану інсерційного моделювання – напрямку, який розвивається на протязі останнього десятиліття як підхід до побудови загальної теорії взаємодії агентів та середовищ у складних розподілених багатоагентних системах.
|
| first_indexed | 2025-12-07T17:57:20Z |
| format | Article |
| fulltext |
УСиМ, 2012, № 6 3
Теоретические основы инсерционного моделирования
УДК 519.686.2
А.Ад. Летичевский
Инсерционное моделирование
Представлен обзор современного состояния инсерционного моделирования – направления, которое развивается на протяже-
нии последнего десятилетия как подход к построению общей теории взаимодействия агентов и сред в сложных распределен-
ных многоагентных системах.
The review of the current state of insertion modeling, – the direction which developed over the last decade as an approach to the con-
struction of a general theory of the interaction of agents and environments in complex distributed multi-agent systems is presented.
Подано огляд сучасного стану інсерційного моделювання – напрямку, який розвивається на протязі останнього десятиліття як підхід
до побудови загальної теорії взаємодії агентів та середовищ у складних розподілених багатоагентних системах.
Введение. Инсерционное моделирование пред-
ставляет собой направление, развиваемое на
протяжении последнего десятилетия как подход
к построению общей теории взаимодействия
агентов и сред в сложных распределенных мно-
гоагентных системах. Основные понятия инсер-
ционного моделирования (среда, агенты, функ-
ция погружения) ведены в работах [1–3], опуб-
ликованных в 90-х годах. Идейным прототипом
инсерционного моделирования следует счи-
тать модель взаимодействующих управляюще-
го и операционного автоматов, предложенную
В.М. Глушковым еще в 60-х годах [4, 5] для
описания структур вычислительных машин, а
также ее развитие в теории дискретных преоб-
разователей 70-х годов. В этих моделях систе-
ма представляется в виде композиции двух ав-
томатов – управляющего и информационного.
Управляющий автомат играет роль агента, а
информационный – роль среды погружения это-
го агента. Модели макроконвейерных парал-
лельных вычислений, исследованные в 80-е го-
ды [6], еще больше приблизились к современ-
ной модели взаимодействия агентов и сред. В
этих моделях процессы, соответствующие па-
раллельно работающим процессорам, можно
рассматривать как агентов, взаимодействующих
в среде распределенных структур данных.
Другой источник инсерционного моделиро-
вания – общая теория взаимодействующих ин-
формационных процессов, сформированная в
70-х годах и служащая основой для современ-
ных исследований в этой области. Она включает
в себя CCS (Calculus of Communicated Processes)
[7, 8] и π-исчисление Р. Милнера [9], CSP (Com-
municated Sequential Processes) Т. Хоара [10], ACP
(Algebra of Communicated Processes) [11] и много
различных ответвлений этих базовых теорий.
Достаточно полный обзор классической теории
процессов представлен в справочнике по алгеб-
ре процессов [12], изданном в 2001 г. Модели,
исследуемые в этих теориях, можно эквивалент-
ным образом представить в виде композиции
среды и погруженных в нее агентов. Различные
предложения по унификации общей теории вза-
имодействия в распределенных системах актив-
но обсуждаются, начиная с 90-х годов. К ним
относятся чисто математические исследования
на основе коалгебр [13], подход, предложен-
ный Хоаром [14], логика условного переписы-
вания Месегера [15] и др.
В последние годы инсерционное моделиро-
вание становится инструментом разработки при-
кладных систем верификации требований и спе-
цификаций распределенных взаимодействующих
систем [16–19]. Система VRS, разработанная в
Украине по заказу фирмы Моторола с участи-
ем сотрудников Института кибернетики, успеш-
но применяется для верификации требований и
спецификаций в области телекоммуникацион-
ных систем, встроенных систем и систем ре-
ального времени.
Статья носит обзорный характер. Основные
понятия теории взаимодействия такие, как тран-
4 УСиМ, 2012, № 6
зиционная система, трассовая и бисимуляцион-
ная эквивалентность, алгебра процессов и по-
ведений, последовательная и параллельная
композиция транзиционных систем предпола-
гаются известными. Соответствующие опреде-
ления можно найти в [20] и в [21].
Агенты и среды
Инсерционное моделирование занимается
построением моделей и изучением взаимодей-
ствия агентов и сред в сложных распределенных
многоагентных системах. Основные положения
парадигмы инсерционного моделирования мож-
но сформулировать следующим образом.
Мир есть иерархия сред и агентов, погру-
женных в эти среды.
Агенты и среды есть сущности, эволю-
ционирующие во времени и обладающие на-
блюдаемым поведением.
Погружение агента в среду изменяет пове-
дение этой среды и порождает новую среду,
готовую к погружению в нее новых агентов
(если для них есть место в этой среде).
Среда, рассматриваемая как агент, может
быть погружена в среду верхнего уровня.
Агенты могут погружаться в среду из сре-
ды верхнего уровня, а также производиться
внутренними агентами, уже погруженными в
среду ранее.
Агенты и среды могут моделировать дру-
гие агенты и среды на различных уровнях аб-
стракции.
Говоря об агентах и средах, мы имеем в ви-
ду как технические, так и реальные системы –
физические, биологические и социальные, а
взаимодействия, интересующие нас – это в
первую очередь информационные взаимодей-
ствия, абстрагированные от физических про-
цессов, которыми они сопровождаются.
Переходя к математическим уточнениям, вы-
берем в качестве понятия агента наиболее аб-
страктное математическое понятие, моделиру-
ющее системы, эволюционирующие во време-
ни. Таким образом, агент – это размеченная
транзиционная система, состояния которой оп-
ределяются с точностью до бисимуляционной
или трассовой эквивалентности. Главным пре-
имуществом понятия транзиционной системы
в сравнении с другими моделями систем, эволю-
ционирующих во времени, является разделе-
ние наблюдаемой части системы, которая вы-
ражается в действиях, и скрытой части систе-
мы, определяемой ее внутренними состояниями.
Среда – это агент, обладающий функцией
погружения. Более точно, среда – это набор
<E, C, A, Ins>, где E – множество состояний
среды (отождествляемых с поведениями), С –
множество действий среды, А – множество
действий агентов, погружаемых в среду,
Ins : E F (A) E – функция погружения. Здесь
F (A) – полная алгебра поведений агентов с
множеством действий A. Таким образом, всякая
среда E допускает погружение любого агента с
множеством действий A. Поскольку состояния
транзиционных систем рассматриваются с точ-
ностью до бисимуляционной эквивалентности,
то их можно отождествлять с поведениями и
говорить о непрерывности функций. Основное
требование к среде – это непрерывность функ-
ции погружения. Из этого предположения вы-
текает ряд полезных следствий. Например, тот
факт, что функцию погружения можно зада-
вать как наименьшую неподвижную точку сис-
темы функциональных уравнений. Результат
Ins (e, u) погружения агента, находящегося в
состоянии u, в среду, находящуюся в состоя-
нии e, обозначается так же как e[u]. Полагая
e[u, v] = (e[u])[v], получаем возможность гово-
рить о совокупности агентов, погруженных в
среду и рассматривать состояния среды вида
e[u1, u2, , um] = (((e[u1]) [u2]))[um]. Прини-
мая во внимание, что среда есть агент, ее
можно погружать в среду верхнего уровня,
рассматривая многоуровневые среды вида
EEE uueuuee ,...],...],[,,...],[[
21 22212112111 , где обо-
значение e[u1, u2, ]E явно указывает среду E,
которой принадлежит состояние e. Поведение u
инициализированного агента определяет пре-
образование [u]: E E, определенное соотно-
шением [u] (e) = e[u] и инсерционную эквива-
лентность агентов E~ относительно среды Е, оп-
ределенную соотношением ~Eu v [ ] [ ]u v .
Эта эквивалентность обычно слабее, чем би-
симуляционная, играет основную роль в при-
УСиМ, 2012, № 6 5
ложениях, поскольку преобразования алгорит-
мических и программных реализаций агентов,
функционирующих в некоторой среде, следует
выполнять как преобразования, сохраняющие
инсерционную эквивалентность.
Расширенная алгебра поведений
Напомним, что алгебра поведений имеет две
основные операции: префиксинг ua. и неде-
терминированный выбор u + v, где a – дейст-
вие, u и v – поведения. Кроме того, в алгебре
поведений есть две терминальные константы –
успешное завершение и тупиковое поведе-
ние 0 (неопределенное поведение и отношение
аппроксимации, используемые при построении
полной алгебры поведений, сейчас не понадо-
бятся). Всякое поведение можно представить в
нормальной форме
. εi i u
i I
u a u
,
где u – терминальная константа (если I , то
u = , поскольку u + 0 = 0). Если все поведения
в правой части рекурсивно представлены в нор-
мальной форме, то для u получится представ-
ление в виде ориентированного дерева, воз-
можно бесконечного, с дугами, размеченными
действиями, и некоторыми вершинами, отме-
ченными символом . Любая конечная часть
такого дерева (т.е. конечное множество конеч-
ных путей, которые начинаются в корне) назы-
вается префиксом поведения.
Система поведений
)(
)(,,.
iJj
ijiji IiJIiuau
может рассматриваться как система рекурсив-
ных определений. Если она конечна, то пове-
дения называются конечно определенными. Та-
кие поведения могут быть отождествлены с
состояниями конечной транзиционной систе-
мы с отношением переходов , ,ija
i ju u i I
( )j J i I
и с множеством заключительных
состояний { | ε }i iU u .
Расширим алгебру поведений, добавив к ней
функции погружения, рассматриваемые как би-
нарные операции на соответствующих множе-
ствах. Формально мы должны рассмотреть мно-
гоосновную алгебру, которая получается, если
зафиксировать некоторое семейство сред (E)H
и алгебр поведений агентов ( )F A в каче-
стве основных множеств. Тогда функция погру-
жения будет определена как : ( )Ins E F A
E и выражения, рассмотренные в начале
этого раздела, можно будет рассматривать как
алгебраические выражения соответствующей
многоосновной алгебры. Среда, определенная
с помощью такой алгебры, называется много-
уровневой средой.
Основные свойства функций погружения
Будем рассматривать только такие среды,
для которых имеет место тождество [ , ]e u
[ ]e u . Состояние среды e называется нераз-
ложимым, если из того, что ][uee , следует,
что uee , . Множество неразложимых со-
стояний среды назовем ее ядром. Неразложи-
мое состояние среды соответствует состоянию
до погружения в нее каких бы то ни было аген-
тов, а среда с пустым ядром предполагает, что
в нее изначально погружено бесконечное мно-
жество агентов. Среда называется конечно-раз-
ложимой, если всякое ее состояние можно пред-
ставить в виде ],...,[ 1 muue с неразложимым e. В
дальнейшем, если не оговорено противное, бу-
дут рассматриваться только конечно-разложи-
мые среды.
Одношаговое погружение определяется пра-
вилом ),,(
][][
,
cbaP
ueue
uuee
c
ba
.
Здесь ),,( cbaP – разрешающий предикат.
Правило применимо только в том случае, ко-
гда разрешающий предикат истинен. Для ко-
нечно-разложимой среды, в которую погруже-
но несколько агентов, следует воспользоваться
производным правилом:
),,(
],...,[],...,[
],,...,[],...,[
11
1111 dbcP
uueuue
uuuueuue
m
d
m
m
b
mm
c
m
,
где e – неразложимое состояние среды.
Другая форма правила одношагового по-
гружения:
][].)[.(),,( ueuubeeacbaP c .
6 УСиМ, 2012, № 6
Одношаговое правило можно понимать так.
Если агент хочет выполнить действие b (одно
из возможных), то среда разрешает это дейст-
вие, если у нее найдутся два действия a и с,
такие, что имеет место P (a, b, c). В этом случае
переход зависит только от того, что среда мо-
жет сделать за один шаг.
Более общее правило может быть сформули-
ровано, если в разрешающий предикат доба-
вить поведение среды: P (e, a, b, c). Но для то-
го, чтобы обеспечить непрерывность функции
погружения, нужно потребовать непрерывность
разрешающего предиката: он должен зависеть
только от конечного префикса поведения e. Та-
кое правило называется правилом одношагово-
го префиксного погружения (head insertion). На-
конец, еще более общий случай получается, ес-
ли разрешающий предикат зависит и от пове-
дения агента: P (e, u, a, b, c). Такое погружение
называется прогнозирующим.
Рассмотренное правило не является полным.
Требуются дополнительные правила для тер-
минальных состояний среды и агента, а также
для недетерминированного выбора. Примерами
таких правил могут быть тождества 0[u] = 0
[u] = , e[] = e, которые можно дополнить
тождеством e[0] = 0 для неразложимого со-
стояния среды e.
Функция погружения называется аддитив-
ной, если
][][])[(],[][][ veueufeveuevue .
Аддитивность функции погружения может
означать, что как среда, так и агент делают свой
выбор независимо, но так, чтобы была возмож-
ность продолжать движение. При этом следует
иметь в виду, что если нет правила, по которо-
му возможен переход из e[u] , то e[u] = 0.
Кроме аддитивных, на практике встречаются
коммутативные погружения с тождествами
e[u, v] = e[v, u] и, как частный случай коммута-
тивных, параллельные погружения: e[u, v] =
= e[u || v].
Атрибутные среды
Для многих практических приложений по-
нятие среды и агента слишком абстрактно, по-
скольку игнорирует структуру состояний сре-
ды и агентов. Кроме того, при переходе в тер-
минальное состояние теряется информация о
состоянии среды, если она имеет структуру. Всю
необходимую информацию можно, разумеет-
ся, передавать через действия, но это часто вы-
глядит неестественно и громоздко. Для того
чтобы решить эту проблему, в [22] было вве-
дено понятие атрибутной транзиционной сис-
темы. Атрибутные транзиционные системы от-
личаются от размеченных тем, что в них раз-
мечены не только переходы, но и состояния.
Алгебра поведений для атрибутных систем от-
личается: поведения могут быть размечены ат-
рибутными разметками. Для этой цели, кроме
префиксинга, вводится еще одна операция, опе-
рация разметки : u, где u – поведение, – раз-
метка. Теперь вся необходимая информация о
состоянии среды может передаваться через ее
разметку. В частности может быть много тер-
минальных констант, соответствующих успеш-
ному завершению или тупику, поскольку они
могут иметь различные разметки.
Атрибутные среды строятся на основе не-
которой логической базы. Эта база включает в
себя набор типов (целые, вещественные, пере-
числимые, символьные, поведения и т.д.), ин-
терпретированных на некоторых областях дан-
ных, символы для обозначения констант из этих
областей и набор типизированных функцио-
нальных и предикатных символов. Часть этих
символов интерпретирована (например, ариф-
метические операции и неравенства, равенство
для всех типов и т.д.). Неинтерпретированные
функциональные и предикатные символы на-
зываются атрибутами. Неинтерпретированные
функциональные символы арности 0 называ-
ются простыми атрибутами, остальные – функ-
циональными атрибутами (неинтерпретирован-
ный предикатный символ рассматривается как
функциональный с бинарной областью значе-
ний). Функциональные символы используются
для определения структур данных, таких как
массивы.
Над логической базой атрибутной среды
строится базовый логический язык. Обычно это
язык первого порядка, возможно с кванторами.
При необходимости могут включаться некото-
рые модальности темпоральной логики. Атри-
УСиМ, 2012, № 6 7
бутным выражением называется простой ат-
рибут или выражение вида f (t1, , tn), где f –
функциональный атрибут арности n, t1, , tn –
уже построенные атрибутные выражения или
константы подходящих типов. Если все выра-
жения t1, , tn константы, то атрибутное вы-
ражение называется константным.
Ядро атрибутной среды состоит из формул
базового языка. Атрибутные среды делятся на
два класса: конкретные и символьные.
Неразложимое состояние конкретной ат-
рибутной среды представляет собой формулу
вида t1 = a1 tn = an, где t1, , tn – различные
константные атрибутные выражения, a1, , an –
константы. Обычно такую формулу представ-
ляют в виде частичного отображения с обла-
стью определения (t1, , tn) и областью значе-
ний, равной множеству всех констант. Конкрет-
ные атрибутные среды удобно использовать для
формализации операционной семантики языков
программирования и языков спецификации про-
граммных систем. Состояние среды – это состо-
яние памяти (структур данных, объектов, сете-
вых конструкций, каналов и т.п.). Программы –
это агенты, погруженные в среду. Для парал-
лельных языков программирования взаимодей-
ствие осуществляется через общую память или
обмен сообщениями. При взаимодействии че-
рез общую память основную роль играет парал-
лельная композиция поведений (асинхронная
или синхронизируемая). Обмен сообщениями
предполагает использование специальных струк-
тур данных в среде для организации взаимо-
действия. Действия агентов в конечном итоге
сводятся к присваиваниям (x := t, где x – атри-
бутное выражение, t – алгебраическое выраже-
ние базового языка) и проверкам условий
(check , где – формула базового языка). Со-
ответствующие правила имеют вид:
),,(
][][
,
:
::
txeP
ueue
uuee
tx
txtx
;
check
check
|
[ ] [ ]
u u
e
e u e u
.
Разрешающее условие для присваивания мо-
жет накладывать ограничение на однознач-
ность значений для аргументов левой и правой
части присваивания.
Программные конструкции (различные ви-
ды циклов, ветвления и т.п.) в большинстве
случаев достаточно просто моделируются ре-
курсивными уравнениями в алгебре поведе-
ний. Например,
. .if then P else Q check P check Q ,
( ; ) while do P if then P while do P else .
Неразложимые состояния символьной сре-
ды – это формулы базового языка произволь-
ного вида. Конкретные и символьные состоя-
ния атрибутной среды вида F [u1, u2, ] также
рассматриваются как формулы. Предполагает-
ся, что все погруженные агенты имеют уникаль-
ные имена (это могут быть, например, их атри-
бутные отметки). Далее, среди атрибутов базо-
вого языка есть функциональный атрибут state,
определенный на именах агентов и принимаю-
щий значения в области их поведений.
Если m1, m2, имена агентов u1, u2, , то
1 2 1 1
2 2
[ , ,...] (state( ) )
(state( ) ) ... .
F u u F m u
m u
Локальные свойства
Наиболее известные способы спецификации
программ и систем (программных и техничес-
ких) находятся в области темпоральной, дина-
мической и некоторых других видов модальных
логик [23]. Однако в большинстве случаев они
применяются тогда, когда уже известна доста-
точно подробная модель системы и решается
проблема проверки свойств этой системы, за-
данных в логической форме (model checking).
Другой способ описания требований и спе-
цификации систем – описание локальных по-
веденческих свойств системы. В математичес-
кой форме речь идет о свойствах отношения пе-
реходов транзиционной системы, а в случае,
когда система представлена в виде композиции
среды и агентов, речь идет об описании функ-
ции погружения.
Рассмотрим локальные свойства системы,
представленной как конкретная или символь-
ная атрибутная среда. В общем случае локаль-
ное свойство атрибутной среды имеет вид фор-
мулы x ( < u > ), где x – список (типизи-
8 УСиМ, 2012, № 6
рованных) параметров, и – формулы базо-
вого языка, u – процесс (конечное поведение
специфицируемой системы). Формула назы-
вается предусловием, а формула – постусло-
вием локального свойства. От параметров мо-
гут зависеть как условия, так и поведение сис-
темы. Локальное свойство может рассматривать-
ся как формула темпоральной логики, выража-
ющая тот факт, что если (для подходящих зна-
чений параметров) состояние системы удовле-
творяет условию , то поведение u может быть
инициировано, и после его успешного заверше-
ния, разметка нового состояния будет удовлет-
ворять условию . Не трудно проследить ана-
логию между тройками Хоара (формулы ди-
намической логики) и локальными свойствами
систем. Другая аналогия – это продукции, ши-
роко применяемые при описании систем ис-
кусственного интеллекта.
Локальные свойства, используемые во вход-
ном языке системы VRS для представления ин-
серционных моделей распределенных взаимо-
действующих систем, носят название базовых
протоколов. Они привязаны к базовому языку
системы VRS, а для представления поведения
системы используются MSC диаграммы [24].
Обычно базовые протоколы определяются не-
зависимо друг от друга и на них априори не за-
дано никаких отношений следования, определя-
ющих порядок их применения. Поэтому семан-
тика спецификаций на основе базовых протоко-
лов не очевидна. В процессе исследования се-
мантики языка базовых протоколов было разра-
ботано несколько подходов к построению такой
семантики. В этих подходах существенную роль
играют понятия абстракции и конкретизации,
на которых остановимся более подробно.
Абстракции. При работе с большими сис-
темами, такими как телекоммуникационные сис-
темы, сети типа Интернет, многопроцессорные
системы с большим числом компонент, невоз-
можно манипулировать полными описаниями их
состояний. Поэтому, принято заменять состоя-
ния таких систем различного рода абстрактны-
ми объектами. В инсерционном моделировании
в качестве абстракций больших систем исполь-
зуются атрибутные системы, состояния кото-
рых размечаются формулами базового языка.
Если состояния сами представлены формула-
ми, получаем символьные атрибутные модели.
Для изучения соотношений между абстракт-
ными и конкретными моделями в [19] введены
понятия абстракции и конкретизации атрибут-
ных транзиционных систем.
Предполагается, что состояния исходной сис-
темы и формулы базового языка связаны от-
ношением (семантического) следования s |= ,
которое означает, что формула истинна на
разметке состояния s (разметка может не быть
формулой). Если же состояние s не размечено,
то s |= означает, что есть тождественно ис-
тинная формула базового языка, т.е. истинна
на любых разметках. Отношение следования
определено также на состояниях абстрактной
системы, которые размечены формулами базо-
вого языка, и в этом случае s |= означает, что
есть следствие формулы, которая размечает
данное состояние.
Пусть S и S – две атрибутные (не обяза-
тельно различные) системы с размеченными
состояниями, одной и той же логической ба-
зой и множеством действий. Пусть BL – ба-
зовый язык. Определим отношение абстрак-
ции SS Abs таким образом, что
( , ) ( )(( | ) ( | ))s s s s Abs BL .
Система S называется прямой абстракцией
системы S , а система S прямой конкретиза-
цией системы S, если существует непустое от-
ношение 1 Abs , которое является отноше-
нием моделирования, т.е. имеет место следую-
щее утверждение:
( , )(( , )
( )( ( , ) )).
a
a
s S s S s s s t
t S s t t t
Система S называется обратной абстрак-
цией системы S , а система S – обратной кон-
кретизацией системы S, если существует не-
пустое отношение 1 Abs , которое является
отношением обратного моделирования, т.е. име-
ет место следующее утверждение:
( , )(( , )
( )( ( , ) )).
a
a
s S s S s s s t
t S s t t t
УСиМ, 2012, № 6 9
Система и ее абстракция связаны следующим
образом. Если в прямой абстракции системы из
некоторого состояния достижимо заданное свой-
ство, то оно также достижимо из некоторого со-
стояния самой системы. Для обратной абстрак-
ции имеет место двойственное свойство: если
из некоторого состояния системы достижимо со-
стояние, в котором заданное свойство наруша-
ется, то из некоторого начального состояния ее
обратной абстракции также достижимо состо-
яние, в котором это свойство нарушается.
Прикладное значение этих утверждений со-
стоит в том, что, комбинируя прямую и обрат-
ную абстракции, можно получать различные ре-
зультаты по верификации систем и генерации
тестов. Например, если есть подозрение в том,
что система имеет ошибку, то найти ее можно
с помощью прямой абстракции, убедиться же в
том, что в системе нет ошибок, можно с помо-
щью обратной абстракции. Обратную абстрак-
цию удобно также использовать для генерации
тестов, обеспечивающих определенную степень
покрытия требований, выраженных в виде сис-
тем базовых протоколов.
Семантика. В [19] была построена общая
семантика систем базовых протоколов, сопос-
тавляющая каждой системе P базовых прото-
колов некоторую фиксированную транзицион-
ную систему S(P), определенную с помощью
системы уравнений в алгебре поведений. Эта
система уравнений строится следующим обра-
зом. Сначала по системе P строится множество
Pinst конкретизированных базовых протоколов.
Конкретизированный базовый протокол (z)
<u (z) > (z) получается из формулы x ((x)
< u (x)> (x)) путем подстановки конкретно-
го набора значений z параметров вместо x. Да-
лее на множестве действий среды определяет-
ся отношение перестановочности, и на базе
этого отношения определяется частично после-
довательная композиция (()*()) поведений. Для
атрибутных систем перестановочность может
означать их информационную независимость.
На множестве конкретизированных свойств оп-
ределяются функции app (F, ) = 0,1 и pt (F, ) = F
(предикатный трансформер). Первая использу-
ется для определения применимости свойства с
предусловием к состоянию среды F, вторая –
для вычисления нового состояния среды с по-
мощью постусловия . Основное требование к
функции pt состоит в том, чтобы условие было
истинным на состоянии F . Система уравнений
для поведений FS системы S(P) в состояниях
F, имеет вид:
instPu
Fapp
FptF u
,1),(
),( )*( SS .
Для определения применимости протоколов
используются два метода: экзистенциальный и
универсальный. Определение применимости по
экзистенциальному методу означает выполни-
мость конъюнкции F , применимость по уни-
версальному методу означает общезначимость
импликации F .
Другой подход к определению семантики
базовых протоколов, также рассмотренный в
статье [19], состоит в сопоставлении системе
базовых протоколов P некоторого множества
C(P) конкретных атрибутных систем, которые
по определению объявляются реализациями си-
стемы P. Было показано, что система S(P) есть
абстракцией любой системы из класса C(P).
Эта абстракция будет прямой, если выбран уни-
версальный метод, и обратной, если выбран
экзистенциальный метод.
В [25] был предложен новый подход, осно-
ванный на общем (абстрактном) понятии реа-
лизации системы базовых протоколов. В этой
работе базовые протоколы рассматривались с
привязкой к интерпретированным MSC диа-
граммам системы VRS, используемым в каче-
стве способа задания процессов системы. Но
понятие реализации легко обобщается и на
произвольные локальные свойства.
В соответствии с этой семантикой каждая
спецификация P на языке базовых протоколов
определяет некоторый класс атрибутных тран-
зиционных систем, которые объявляются реа-
лизациями системы P. Этот класс определяется
аксиоматически и включает в себя как конкрет-
ные, так и символьные реализации. На состоя-
ниях реализации по-прежнему должно быть оп-
ределено отношение истинности s | = и от-
ношение перестановочности действий, которое
10 УСиМ, 2012, № 6
определяет частично последовательную компо-
зицию. Основная аксиома, определяющая реа-
лизацию, имеет вид
[ ]*[ ]( , ), |B Cappl s s s s .
Здесь B и C – базовые протоколы, [B] и [C] –
их процессы. Предполагается, что [B] и [C]
перестановочны. Условие есть предусловие
базового протокола B, а условие его посту-
словие.
Предикатный трансформер. Каждая фор-
мула базового языка соответствует множеству
конкретных состояний, на котором она истин-
на (покрывает это множество). Поэтому функ-
ция погружения для символьной среды должна
быть согласованной с функцией погружения со-
ответствующей конкретной среды. Эта согла-
сованность определяется в терминах предикат-
ного трансформера, который сам по себе опре-
деляет переходы как в конкретной, так и в сим-
вольной атрибутной среде. Если в конкретной
системе s s и s |= F, то | ( , )s pr F . Та-
ких функций может быть много, и простейшая
из них определяется как ( , )pr F . Но при
этом полностью теряется информация о пре-
дыдущем состоянии F. Между тем, часть этой
информации может переходить в новое состо-
яние. Например, если постусловие меняет зна-
чения только нескольких атрибутов, то осталь-
ные не меняют своих значений. Среди всех
функций, определяющих предикатный транс-
формер, может существовать наисильнейшая.
Она должна удовлетворять обратному усло-
вию: если | ( , )s pr F и s s , то должно
быть s |= F. Вопрос о существовании сильней-
шего предикатного трансформера и возможно-
сти выразить его средствами базового языка
зависит от этого языка. В работе [26] постро-
ен сильнейший предикатный трансформер для
входного языка системы VRS.
Рассмотрим более детально структуру преди-
катного трансформера для случая атрибутов про-
стых типов. Пусть базовый протокол имеет вид
( ( , , ) ( , , ) ( , ))x z s x u z s x s x , (1)
где x – список параметров, z – список атрибу-
тов, которые входят в предусловия, но не вхо-
дят в постусловия, s – список атрибутов, вхо-
дящих в постусловия. Пусть F(z,s) – формула
текущего состояния. Основное предположе-
ние, используемое для построения предикат-
ного трансформера, состоит в том, что после
завершения базового протокола изменить свое
значение могут только те атрибуты, которые яв-
но входят в постусловие. Условием примени-
мости базового протокола служит одно из двух
утверждений ( , )( ( , )z s F z s ( ( , , ))x z s x или
( , )( ( , ) ( ( , , ))z s F z s x z s x . При использовании
первого условия получаем прямую абстракцию
всех конкретных моделей, а при использовании
второго – обратную. Предикатный трансформер
должен сформировать сильнейшее постусло-
вие, следующее из условия применимости. Вот
это условие (оно будет одним и тем же как для
прямой, так и для обратной абстракции):
)),(),,(),()(,( xsxyzyzFyx .
После формирования этого условия, преди-
катный трансформер должен удалить кванторы,
если это возможно. Таким образом, для реали-
зации абстрактной модели базовых протоколов
нужны дедуктивные средства (прувер и солвер
для базового языка).
Если в постусловиях используются присва-
ивания, то формула модифицируется с исполь-
зованием обычной (Хоаровской) семантики при-
сваиваний. Возможны также обобщения кон-
струкции предикатного трансформера в слу-
чае, когда допускаются структуры данных та-
кие, как массивы, списки и т.п.
Используя семантику базовых протоколов
можно генерировать трассы и сценарии функ-
ционирования системы как на уровне конкрет-
ных, так и на уровне абстрактных моделей. Эти
трассы и сценарии можно использовать для ди-
намической проверки различных свойств сис-
темы, например, доказывать инвариантность или
достижимость условий, выразимых в базовом
языке, а также условий, выразимых с помощью
различных видов темпоральной логики. Исполь-
зуя дедуктивные средства, можно также про-
водить статическую верификацию. Например,
для доказательства инвариантности свойства ,
достаточно доказать, что это свойство сохра-
УСиМ, 2012, № 6 11
няется всеми базовыми протоколами, а сохра-
нение свойства = (z, s) базовым протоколом
(1) означает истинность формулы
( , , )( ( ( , ) ( , , )) ( , ) ( , ))z s x y z y z y x s x z s ,
смысл которой состоит в том, что если в ка-
кой-то момент было истинным и был приме-
ним протокол (1), то после его применения
свойство остается истинным.
Верификация. Язык базовых протоколов, ре-
ализованный в системе VRS, допускает исполь-
зование атрибутов числовых и символьных ти-
пов (свободные термы), массивов, списков и
функциональных типов данных. Дедуктивная
система обеспечивает доказательство утвержде-
ний в теории первого порядка, представляющей
собой интеграцию теорий целочисленных и ве-
щественных линейных неравенств, перечисли-
мых типов данных, свободных (неинтерпрети-
рованных) функциональных символов и теорию
очередей. В дедуктивной системе успешно до-
казываются или опровергаются только некото-
рые классы формул, поэтому при верификации
иногда могут быть получены отказы для неко-
торых промежуточных запросов. На практике
такие отказы происходят достаточно редко и в
большинстве случаев не влияют на получение
окончательного результата.
В качестве языка процессов используется
язык MSC [24] с инсерционной семантикой
[27, 28]. Система также допускает использова-
ние языка SDL [29] и соответствующих диа-
граммных представлений языка UML [30].
Основные средства системы VRS – это кон-
кретный и символьный генераторы трасс и
средства статической верификации, включаю-
щие в себя проверку полноты и непротиворе-
чивости базовых протоколов и проверку инва-
риантности свойств.
Система успешно применялась в ряде прак-
тических проектов из области телекоммуника-
ции, встроенных систем, телематики и др. Ко-
личество требований, формализованных в виде
базовых протоколов, достигало 10 000, а коли-
чество атрибутов – в пределах 1000. Методика
использования системы включает в себя ряд
технологий для верификации систем и генера-
ции тестов.
Одна из типичных технологий применяется
для проверки полноты и непротиворечивости
базовых протоколов. Два базовых протокола на-
зываются непротиворечивыми, если при любой
конкретизации этих протоколов их предусловия
не могут быть одновременно истинными. Проти-
воречивость двух протоколов означает, что для
некоторых состояний выбор протокола, который
применяется в этих состояниях, происходит не-
детерминированным образом. Этот недетерми-
низм может быть нежелательным, и система со-
общает о противоречивости (предупреждение)
разработчику. Система базовых протоколов на-
зывается полной, если для любого конкретного
состояния существует хотя бы один базовый
протокол, применимый в этом состоянии. Не-
полнота системы базовых протоколов означает
возможность тупикового состояния (dead lock).
В вышеприведенной формулировке условия
непротиворечивости и полноты проверяются
статически путем анализа предусловий базо-
вых протоколов с использованием дедуктив-
ных средств. На самом деле непротиворечи-
вость и полноту следует проверять не на всех
состояниях, а лишь на достижимых из множе-
ства начальных состояний системы. Если эти
состояния можно описать формулой базового
языка, то снова можно применить статическую
проверку этих свойств, включив их в соответ-
ствующие формулы.
Если система непротиворечива и полна, про-
верка закончена. Если же найден случай проти-
воречия или неполноты и он не принят разра-
ботчиком в силу того, что не ясно, достижимо
ли соответствующее состояние, то возникает но-
вая задача – проверка недостижимости условия,
выражающего нарушение требования непроти-
воречивости или полноты. Поскольку недости-
жимость условия означает инвариантность его
отрицания, то можно снова применить статичес-
кий анализ, пытаясь доказать соответствующие
свойства. Если это удается, задача решена, в про-
тивном случае можно пытаться усилить соответ-
ствующие свойства либо применить динамичес-
кую верификацию, т.е. конкретную или сим-
вольную генерацию трасс, пытаясь доказать или
опровергнуть достижимость искомых свойств.
12 УСиМ, 2012, № 6
Инсерционные машины
Для реализации инсерционных моделей не-
которого класса используется интерпретатор
моделей, который называется инсерционной ма-
шиной. Инсерционная машина состоит из трех
основных компонент:
Модельный драйвер. Эта компонента уп-
равляет движением модели по дереву ее пове-
дения, вычисляя переходы из текущего в новое
состояние.
Анфолдер поведений агентов. Текущее со-
стояние модели представляется в виде алгебра-
ического выражения в расширенной алгебре по-
ведений. Входной язык допускает использова-
ние рекурсивных определений для описания по-
ведений агентов и структур данных или состо-
яний среды. Анфолдер поведений использует
эти описания для того, чтобы получить разло-
жение состояния в виде выражения E[u1, u2, ],
где E – неразложимое состояние среды.
Интерактор среды. Приводит состояние
среды к нормальной форме
.i i
i I
E a E
,
используя описание функции погружения.
После приведения к нормальной форме драй-
веру модели остается только выбрать направ-
ление движения i I и осуществить переход
i
a EE i или остановиться, если .
Различаются два типа инсерционных машин:
машины реального времени или интерактив-
ные машины и аналитические инсерционные
машины. Машины реального времени работа-
ют в реальной или виртуальной среде, взаимо-
действуя с внешней средой в реальном време-
ни. Аналитические машины используются для
анализа моделей, исследования их свойств, ре-
шения задач на инсерционных моделях и т.п.
Соответственно модельные драйверы также де-
лятся на интерактивные и аналитические. Ин-
терактивный драйвер после нормализации со-
стояния должен выбрать один переход и вы-
полнить его путем передачи своего действия
во внешнюю среду. Интерактивная машина с
учетом внешнего наблюдателя функционирует
как агент, погруженный во внешнюю среду с
функцией погружения, определяющей законы
функционирования этой среды. Внешняя сре-
да, например, может изменить поведенческий
префикс состояния внутренней среды в соот-
ветствии со своей функцией погружения.
Интерактивный драйвер организован доста-
точно сложно. Он может иметь критерии успеш-
ного функционирования и работать как интел-
лектуальная система, собирая информацию о
прошлом, создавая модель внешней среды и
улучшая алгоритмы принятия решений по вы-
бору действий с целью повышения уровня ус-
пешности своего функционирования. Кроме то-
го, интерактивный драйвер может иметь интер-
фейс для обмена физическими сигналами с внеш-
ней средой (например, прием визуальной или
акустической информации, информации о по-
ложении в пространстве и т.п.).
Аналитическая инсерционная машина, в про-
тивоположность интерактивной, может рассмат-
ривать различные варианты принятия решений
о действиях, возвращаясь в точки выбора и рас-
сматривая различные пути в дереве поведения
системы. Модель системы может включать в се-
бя также и модель внешней среды для этой сис-
темы. В общем случае аналитическая машина
осуществляет поиск состояний, обладающих за-
данными свойствами (достижимость целевых
состояний), или состояний, в которых заданные
свойства нарушаются. Внешняя среда аналити-
ческой машины может быть представлена поль-
зователем, взаимодействующим с машиной, фор-
мулируя задачи и управляя активностью маши-
ны. Аналитические машины, обогащенные ло-
гикой и дедуктивными средствами, использу-
ются для символьного моделирования систем.
Система VRS, помимо инсерционной маши-
ны, использующей специализированный вход-
ной язык описания требований и специфика-
ций, содержит средства для статического ана-
лиза инсерционных моделей, генерации тесто-
вых наборов, генерации кода и ряд других
средств, поддерживающих разработку распре-
деленных взаимодействующих систем.
Сегодня в Институте кибернетики им.
В.М. Глушкова ведется работа над созданием
новой системы инсерционного моделирования
УСиМ, 2012, № 6 13
IMS (Insertion Modeling System). Эта система
представляет собой среду для разработки ин-
серционных машин различного типа. Она со-
держит ряд прототипов инсерционных машин
с различными типами функций погружения и
средствами их развития. Базовой системой про-
граммирования для IMS является система ал-
гебраического программирования APS, обеспе-
чивающая гибкость и эффективность при раз-
работке новых инсерционных машин.
В статье, представленной в этом выпуске,
описана инсерционная машина для доказатель-
ного программирования. Она ориентирована на
верификацию императивных аннотированных
программ, использующих различные языки про-
граммирования.
Когнитивные архитектуры
Когнитивные архитектуры или интеллекту-
альные агенты – это активно развивающееся в
последнее время направление в искусственном
интеллекте. Его цель – построение модели че-
ловеческого разума, обладающей такими же
универсальными возможностями. В отличие от
специализированных систем искусственного ин-
теллекта, способных эффективно решать спе-
цифические классы задач, когнитивные архи-
тектуры должны адаптироваться к различным
новым, часто неожиданным ситуациям, возни-
кающим в результате взаимодействия с внеш-
ней средой, обучаться, ставить цели, улучшать
свое поведение и т.п. Недавно возникло новое
направление BICA (Biologically Inspired Cogni-
tive Architectures – биологически мотивиро-
ванные когнитивные архитектуры) [32]. В рам-
ках этого направления было выполнено сравне-
ние большого количества существующих архи-
тектур, выделены основные черты, которыми
должны обладать такие архитектуры, ежегодно
проводятся конференции, собирающие специа-
листов из различных областей, заинтересован-
ных в продвижении в этом направлении. Нача-
ли исследовать возможность создания когни-
тивной архитектуры на основе инсерционного
моделирования и авторы этой статьи.
Наши представления в краткой форме могут
быть выражены следующим образом. Инсер-
ционная когнитивная архитектура – это инсер-
ционная машина, которая осознает себя, имеет
центр оценки успешности своего поведения и
стремится к многократному достижению мак-
симального успеха. Как агент эта машина по-
гружена в свою внешнюю среду и имеет сред-
ства взаимодействия с ней. Внутренняя среда
создает и совершенствует свою модель и мо-
дель внешней среды и населяющих ее агентов.
Все эти модели строятся как многоуровневые
инсерционные среды. Для достижения своих це-
лей она использует основные механизмы, вы-
работанные в области биологически мотивиро-
ванных когнитивных архитектур, а также в об-
ласти инженерных проектов, поддерживающих
решение сложных интеллектуальных задач.
Уверенность в правильности нашего направ-
ления основана на следующих гипотезах:
Многоуровневая инсерционная среда может
быть с успехом использована для моделирова-
ния шести уровней неокортекса (коры голов-
ного мозга). Двигаясь от нижних уровней к выс-
шим, повышается уровень абстракции, переходя
к все более абстрактным символьным моделям.
Агенты, погруженные в среды верхнего уров-
ня, покрывают классы моделей нижнего уровня.
Человеческий разум должен содержать ме-
ханизмы, подобные драйверам инсерционных
машин, позволяющие активизировать модели
внешних и внутренних сред, произведенные в
результате накопления жизненного опыта, обу-
чения и унаследованные генетически.
Когнитивная архитектура функционирует
как инсерционная машина реального времени,
осознавая себя с помощью внутренней среды
самого верхнего уровня. Эта среда управляет
всеми средами (агентами) нижнего уровня, ак-
тивизируя или тормозя их деятельность. Аген-
ты всех уровней работают параллельно и неза-
висимо до тех пор, пока не попадают под кон-
троль сред верхних уровней, осуществляя мо-
бильные погружения в них.
Заключение. Основной областью примене-
ния инсерционного моделирования есть верифи-
кация технических систем, однако потенциаль-
ные возможности этого направления далеко не
исчерпываются этой областью. Инсерционное
моделирование можно рассматривать как одно
14 УСиМ, 2012, № 6
из направлений, призванное унифицировать об-
щую теорию взаимодействия в распределен-
ных системах, и допускающую применения в
других прикладных областях. В первую оче-
редь следует назвать возможные применения в
биологической и экономической информатике.
1. Gilbert D.R., Letichevsky A.A. A universal interpreter
for nondeterministic concurrent programming languages
/ M. Gabbrielli (Ed.) // Fifth Compulog network area
meeting on language design and semantic analysis me-
thods, Sept. 1996.
2. Letichevsky A., Gilbert D. A general theory of action lan-
guages // Кибернетика и системный анализ, 1998. –
№ 1. – С. 16–36.
3. Letichevsky A., Gilbert D. Interaction of agents and en-
vironments / D. Bert, C. Choppy (Eds.) // Resent
trends in Algebraic Development technique, LNCS
1827. – Berlin: Springer-Verlag, 1999. – P. 311–328.
4. Глушков В.М. Теория автоматов и вопросы проек-
тирования структур цифровых машин // Кибернети-
ка. – 1965. – № 1. – С. 3–11.
5. Glushkov V.M., Letichevsky A.A. Theory of algorithms
and descrete processors / J.T. Tou (Ed.). // Advances
in Information Systems. Science. – Plenum Press,
1969. – 1.–P. 1–58.
6. Капитонова Ю.В., Летичевский А.А. Математиче-
ская теория проектирования вычислительных сис-
тем. – М.: Наука, 1988. – 295 с.
7. Milner R. A Calculus of Communicating Systems // Lec-
ture Notes in Comp. Sci. – Springer-Verlag, 1980. – 92 р.
8. Milner R. Communication and Concurrency. – Pren-
tice Hall, 1989. – 250 р.
9. Milner R. The polyadic π-calculus: a tutorial, Tech.
Rep. ECS–LFCS–91–180, Laboratory for Foundations
of Comp. Sci., Department of Comp. Sci. – University
of Edinburgh, UK (1991).
10. Hoare C.A.R. Communicating Sequential Processes. –
New Jersey: Prentice Hall, 1985. – 238 р.
11. Bergstra J.A., Klop J.W. Process algebra for synchro-
nous communications // Information and Control. –
1984. – 60. – N 1/3. – P. 109–137.
12. Handbook of Process Algebra / J.A. Bergstra, A. Ponce,
S.A. Smolka (Eds.) – North-Holland, 2001. – 1342 p.
13. Rutten G. Coalgebras and systems, TCS 249. – Р. 31–52.
14. Hoare C.A.R., Jifeng He. Unifying Theories of Program-
ming. – Hemel Hempstead: Prentice Hall, 1999. – 295 р.
15. Meseguer J. Conditional rewriting logic as a unified
model of concurrency // Theoretical Comp. Sci., 1992. –
96. – P. 73–155.
16. Leveraging UML to deliver correct telecom applica-
tions in UML for Real: Design of Embedded Real-Time
Systems / S. Baranov, C. Jervis, V. Kotlyarov et. al. /
L. Lavagno, G. Martin, B. Selic (Eds.). – Kluwer
Acad. Publ., 2003. –P. 323–342.
17. Validation of Embedded Systems / J. Kapitonova, A. Le-
tichevsky, V. Volkov et al. R. Zurawski (Ed.) // The
Embedded Systems Handbook. – Miami: CRC Press,
2005. – P. 6–57.
18. Basic Protocols, Message Sequence Charts, and the
Verification of Requirements Specifications / A. Leti-
chevsky, J. Kapitonova, A. Letichevsky (Jr.) et al. // Comp.
Networks, Elsevier. – Amsterdam, 2005. – P. 662–675.
19. Спецификация систем с помощью базовых прото-
колов / А.Ад. Летичевский, Ю.В. Капитонова,
В.А. Волков и др. // Кибернетика и системный ана-
лиз. – 2005. – № 4. – С. 3–21.
20. Semantics of timed MSC language / A.A. Letichevsky,
J.V. Kapitonova, V.P. Kotlyarov et al. // Kibernetika and
System Analysis, 2002. – N 4. – P. 3–14.
21. Летичевский А.А., Капитонова Ю.В. Инсерционное
моделирование // Пр. міжнар. конф. «50 років Інститу-
ту кібернетики ім. В.М. Глушкова НАН України». –
К.: ИК имени В.М. Глушкова НАН Украины, 2008. –
С. 293–301.
22. Спецификация систем с помощью базовых прото-
колов / А.А. Летичевский, Ю.В. Капитонова, В.А. Вол-
ков и др. // Кибернетика и системный анализ. –
2004. – № 4. – С. 3–26.
23. Bradfield J., Stirling C. Modal Logic and mu-Calculi:
An introduction / J.A. Bergstra, A. Ponce, S.A. Smolka
(Eds.) // Handbook of Process Algebra. – North-Hol-
land, 2001. – 1342. – P. 293–330.
24. ITU-T. Z.120 Recommendation Z.120 (11/99): Lan-
guages for telecommunications applications – Message
Sequence Charts (MSC), 1999. – 129 р.
25. Insertion modeling in distributed system design / A.A. Le-
tichevsky, J.V. Kapitonova, V.P. Kotlyarov et al. // Про-
блеми програмування, 2008. – № 4. – C. 13–38.
26. Свойства предикатного трансформера системы VRS
/ А.А. Летичевский, А.Б. Годлевский, А.А. Летичев-
ский (мл.) и др. // Там же. – 2010. – № 4. – С. 3–16.
27. Letichevsky A. Algebra of behavior transformations and
its applications / V.B. Kudryavtsev, I.G. Rosenberg (Eds.)
// Structural theory of Automata, Semigroups, and Univer-
sal Algebra, NATO Science Series II. Mathematics, Phy-
sics and Chemistry – Springer, 2005. – 207. – P. 241–272.
28. Semantics of Message Sequence Charts / A.A. Letichev-
sky, J.V. Kapitonova, V.P. Kotlyarov et al. // SDL Fo-
rum, 2005. – P. 117–132.
29. ITU-T. Z.100 Recommendation Z.100 – Specification
and Description Language (SDL), 1999. – 200 р.
30. Object Management Group, Unified Modeling Lan-
guage Specification, 2.0. – 2003. – 240 p.
31. http://bicasociety.org/
32. Roggenbach M., Majster-Cederbaum M. Towards a uni-
fied view of bisimulation: a comparative study // TCS. –
2000. – 238. – P. 81–130.
Тел. для справок: +38 044 526-0058 (Киев)
© А.А. Летичевский, 2012
|
| id | nasplib_isofts_kiev_ua-123456789-83102 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0130-5395 |
| language | Russian |
| last_indexed | 2025-12-07T17:57:20Z |
| publishDate | 2012 |
| publisher | Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України |
| record_format | dspace |
| spelling | Летичевский, А.Ад. 2015-06-14T19:08:35Z 2015-06-14T19:08:35Z 2012 Инсерционное моделирование / А.Ад. Летичевский // Управляющие системы и машины. — 2012. — № 6. — С. 3-14. — Бібліогр.: 32 назв. — рос. 0130-5395 https://nasplib.isofts.kiev.ua/handle/123456789/83102 519.686.2 Представлен обзор современного состояния инсерционного моделирования – направления, которое развивается на протяжении последнего десятилетия как подход к построению общей теории взаимодействия агентов и сред в сложных распределенных многоагентных системах. The review of the current state of insertion modeling, – the direction which developed over the last decade as an approach to the construction of a general theory of the interaction of agents and environments in complex distributed multi-agent systems is presented. Подано огляд сучасного стану інсерційного моделювання – напрямку, який розвивається на протязі останнього десятиліття як підхід до побудови загальної теорії взаємодії агентів та середовищ у складних розподілених багатоагентних системах. ru Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України Управляющие системы и машины Теоретические основы инсерционного моделирования Инсерционное моделирование Insertional Modelling Інсерційне моделювання Article published earlier |
| spellingShingle | Инсерционное моделирование Летичевский, А.Ад. Теоретические основы инсерционного моделирования |
| title | Инсерционное моделирование |
| title_alt | Insertional Modelling Інсерційне моделювання |
| title_full | Инсерционное моделирование |
| title_fullStr | Инсерционное моделирование |
| title_full_unstemmed | Инсерционное моделирование |
| title_short | Инсерционное моделирование |
| title_sort | инсерционное моделирование |
| topic | Теоретические основы инсерционного моделирования |
| topic_facet | Теоретические основы инсерционного моделирования |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/83102 |
| work_keys_str_mv | AT letičevskiiaad insercionnoemodelirovanie AT letičevskiiaad insertionalmodelling AT letičevskiiaad ínsercíinemodelûvannâ |