Свойство доступности программы будет следующим:
[
s
(
b
1
2
)
⊃
♦
s
(
b
1
4
)]
∧
[
s
(
b
p
1
)
⊃
♦
s
(
b
p
3
)]
.
Доказательство свойств.
Известно, что для того чтобы иметь воз-
можность проверять наличие тех или иных свойств агентов и потоков
из числа рассмотренных или каких-либо иных дедуктивным способом,
необходимо иметь некоторый адекватный решаемым задачам провер-
ки свойств агентов и потоков язык исчисления и формулировки на
этом языке:
— базовых общезначимых аксиом (если они необходимы);
— аксиом, описывающих общие свойства моделей мультиагентной
системы (программы, состоящей из параллельных процессов), не за-
висящие от конкретного типа системы. Эти аксиомы назовем общими
агентскими аксиомами;
— аксиом, описывающих свойства конкретной модели мультиагент-
ной системы, зависящей от решаемой ею задачи. Эти аксиомы назовем
частными агентскими аксиомами. Частные агентские аксиомы описы-
вают графы переходов агентов;
— аксиом, описывающих общие свойства моделей потоков, не за-
висящие от конкретного типа потоков. Эти аксиомы назовем общими
потоковыми аксиомами;
— аксиом, описывающих свойства конкретной модели потоков. Эти
аксиомы назовем частными потоковыми аксиомами. Частные потоко-
вые аксиомы описывают графы переходов потоков;
— правил вывода, состоятельных для данного исчисления.
Аксиомы образуют базу знаний или онтологию, а свойства (тео-
ремы), которые требуется доказать, являются запросами к этой базе
знаний.
Онтология хранится в определенных форматах и может быть рас-
пределена между агентами. Каждый из агентов решает некоторую
частную задачу в соответствии со своей ролью. Часть из них решает
общую задачу ответа на запрос. Каждый агент имеет входной и вы-
ходной порты, собственную базу знаний (онтологию) и решатель, или
машину вывода, которая использует правила вывода. Через входной
порт агент получает сообщения и запросы от других агентов, а также
информацию из других источников, не являющихся агентами в указан-
ном смысле. Через выходной порт агент выдает сообщения и запросы
другим агентам, а также информацию получателям, не являющимися
агентами.
При описании свойств потоков и агентов использовалась некото-
рая версия временной модальной логики. Эти описания носят теоре-
тический характер, и использование напрямую рассмотренного языка
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2005. № 4 77
