and proved that there is no PDL0 formula equivalent to it. Hence, PDL has more expressive power than PDL0. Their argument actually can be generalized as follows. For all n ≥ 0, let PDLn+1 be the subset of PDL in which programs can contain tests A? only if A is a PDLn formula. For all n ≥ 0, Berman and Paterson considered the PDLn+1 formula An+1 defined by