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

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 $CTL$-logic on reduced Kripke structure — Kripke structure of component Petri net.