Автоматная модель проверки корректности атрибутной политики информационной безопасности в системах с конечным числом объектов

Работа посвящена задаче проверки корректности политики информационной безопасности типа ABAC в случае систем с ограниченным числом объектов. При данных условиях задача сводится к проверке достижимости класса состояний в бесконечной переходной системе. Доказывается, что при условии автоматного задания политики доступа задача проверки ее корректности алгоритмически разрешима.