Реляционная версия многоагентной логики деревьев вычислений $\mathcal{CTLK}$

Рассматривается многоагентная логика деревьев вычислений — $\mathcal{CTLK}$ (Computation Tree Logic with Knowledge). Каждый агент представляет свой собственный вычислительный маршрут исходной задачи, а каждое новое ветвление возможных вычислительных маршрутов порождает новых агентов. Логика $\mathcal{CTLK}$ представляет собой естественное обогащение языка $\mathcal{CTL}$ дополнительными операторами знания. Предложена реляционная — альтернативная автоматной — семантика логики, описаны свойства $\mathcal{CTLK}^{Rel}$-фреймов, доказана финитная аппроксимируемость.