Bisimilar and logically equivalent programs in PDL with parallel operator

We also add to PDL+ the parallel composition operator (PPDL+) and prove its soundness and completeness. We establish that the satisfiability problem for PPDL+ is in 2-EXPTIME. Finally, we define some fragments of PPDL+ and prove its EXPTIME-completeness.