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

004.021: 004.312.4: 004.421.6: 004.414.2
Изучаются модели Крипке детальной сети Петри и её компонентной сети Петри параллельной распределённой системы. Устанавливаются необходимые и достаточные условия для проверки истинности формул темпоральной CT L-логики по редуцированной модели Крипке — модели Крипке компонентной сети Петри.
Kripke structures of detailed Petri net and its component Petri net of parallel distributed system are investigated. Necessary and sufficient conditions are established for checking the validity of formulas of temporal CT L-logic on reduced Kripke structure — Kripke structure of component Petri net.