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...
Main Authors: | , |
---|---|
Published: |
2023
|
Online Access: | https://hdl.handle.net/1721.1/148984 |