Deterministic Context-Free Dynamic Logic Is More Expressive than Deterministic Dynamic Logic of Regular Programs 1

Abstract

We show an example of an algebra T^∙, such that every flow-chart program is equivalent in T^∙ to a loop-free approximation of itself, while a program augmented by one binary push-down store is not equivalent in T^∙ to any loop-free program. From this we deduce that the Deterministic Dynamic Logic of regular programs is strictly weaker than the Deterministic Context-Free Dynamic Logic.