More on looping vs. repeating in dynamic logic (Q2265813)

From MaRDI portal
Revision as of 09:24, 2 August 2023 by Importer (talk | contribs) (‎Created a new Item)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
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
    0 references
    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

    Identifiers