Hence one can simply compare the behaviors of two LTSs by inspecting solely the atomic programs and safely extrapolate on the comparative behavior of these LTSs even for complex programs. We say that the program constructs of PDL are safe for bisimulation. See Van Benthem [1998] for precise characterizations of program constructs that are safe for bisimulation.