On the Expressive Power of Dynamic Logic

We show that "looping" of while-programs can be expressed in Regular First Order Dynamic Logic, disproving a conjecture made by Harel and Pratt. In addition we show that the expressive power of quantifier-free Dynamic Logic increases when nondeterminism is introduced in the programs that a...

Full description

Bibliographic Details
Main Authors: Meyer, Albert R., Winklmann, Karl
Published: 2023
Online Access:https://hdl.handle.net/1721.1/148984