О проверке формул CTL-логики на моделях Крипке сети Петри параллельной распределённой системы

Abstract

Рассматриваются модели Крипке детальной сети Петри и её компонентной сети Петри. Устанавливается, что эти модели являются однотипными алгебраическими системами и доказывается их гомоморфизм, на основании которого строится алгоритм проверки формул темпоральной CTL-логики на модели Крипке детальной сети Петри через проверку CTL-формул на модели Крипке её компонентной сети Петри