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...
| Hauptverfasser: | , |
|---|---|
| Veröffentlicht: |
2023
|
| Online Zugang: | https://hdl.handle.net/1721.1/148984 |