Model Checking EGF on Basic Parallel Processes

In this paper we study the problem of model checking the logic EGF over Basic Parallel Processes (BPP). The logic EGF is obtained by extending the logic EF with the CTL* notation EGF, which means that there exists an infinite path on which there are infinitely many entries satisfying certain property. We prove that this problem is PSPACE-complete, and Sigma(p)(d)-complete for certain classes of fixed formula with the nesting depth d of modal operators.