On conditions imposed on sections of a Kripke structure that simulate the functioning of the compound components allocated in detailed Petri net of parallel distributed system for verification of accuracy of temporal logic formulae

Изучаются модели Крипке детальной сети Петри и её компонентной сети Петри параллельной распределённой системы. Устанавливаются необходимые и достаточные условия для проверки истинности формул темпоральной CT L-логики по редуцированной модели Крипке — модели Крипке компонентной сети Петри.