 Another construct has been studied: the intersection of programs. By adding intersection of programs to PDL, we obtain the logic IPDL. In IPDL, for all programs α, β, the expression α∩β stands for a new program with semantics