More on looping vs. repeating in dynamic logic. (English) Zbl 0559.68049
Two types of divergence in computation are referred to in a paper of D. Harel and 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.
Reviewer: H.Nishimura
MSC:
| 68Q65 | Abstract data types; algebraic specification |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B45 | Modal logic (including the logic of norms) |
Keywords:
high undecidability; infinite computations; program verification; dynamic logic; repeat; loop; validity problemsReferences:
| [1] | Harel, D., Dynamic logic, (Handbook of Philosophical Logic II (1984), Reidel: Reidel Dordrecht), 497-607 · Zbl 0875.03076 |
| [2] | Harel, D., Recurring dominoes: Making the highly undecidable highly understandable, Ann. Discrete Math. (1985), in press · Zbl 0531.68003 |
| [3] | Harel, D.; Pratt, V. R., Nondeterminism in logics of programs, (5th ACM Symp. on Principles of Programming Language (1978)), 203-213 |
| [4] | Harel, D.; Sherman, R., Looping vs. repeating in dynamic logic, Information and Control, 55, 175-192 (1982) · Zbl 0541.68010 |
| [5] | Keisler, J., Model Theory for Infinitary Logic (1971), North-Holland: North-Holland Amsterdam · Zbl 0222.02064 |
| [6] | Meyer, A. R.; Parikh, R., Definability in dynamic logic, J. Comput. Systems Sci., 23, 279-298 (1981) · Zbl 0472.03013 |
| [7] | Meyer, A. R.; Winklmann, K., Expressing program looping in regular dynamic logic, Theoret. Comput. Sci., 18, 301-323 (1982) · Zbl 0478.68031 |
| [8] | Wolper, P.; Vardi, M. Y.; Sistla, A. P., Reasoning about infinite computation paths, (24th IEEE Symp. on Foundations of Computer Science (1983)), 185-194 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
