Deterministic Context-Free Dynamic Logic Is More Expressive than Deterministic Dynamic Logic of Regular Programs1
Paweł Urzyczyn · Fundamenta Informaticae · 1987
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.