More on looping vs. repeating in dynamic logic (Q2265813)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | More on looping vs. repeating in dynamic logic |
scientific article |
Statements
More on looping vs. repeating in dynamic logic (English)
0 references
1985
0 references
Two types of divergence in computation are referred to in a paper of \textit{D. Harel} and \textit{V. R. Pratt} [5th ACM Symp. on Principles of Programming Languages, 203-213 (1978)] as global and local looping respectively. These notions give a repeat and loop constructs, whose expressive power has been investigated in different versions of dynamic logic. This paper shows that QDL, the first-order version of dynamic logic, is more expressive with repeat than with loop. The authors show also that the validity problems for formulas of the form \(\phi \supset \neg loop(\alpha)\) and \(\phi \supset \neg repeat(\alpha)\) are \(\Sigma^ 0_ 1\)-complete and \(\Pi^ 1_ 1\)-complete, respectively.
0 references
high undecidability
0 references
infinite computations
0 references
program verification
0 references
dynamic logic
0 references
repeat
0 references
loop
0 references
validity problems
0 references