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 -complete for certain classes of fixed formula with the nesting depth d of modal operators. © 2011 Springer-Verlag.
CITATION STYLE
Fu, H. (2011). Model checking EGF on basic parallel processes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6996 LNCS, pp. 120–134). https://doi.org/10.1007/978-3-642-24372-1_10
Mendeley helps you to discover research relevant for your work.