×

On the expressive power of some dynamic logics. (English. Russian original) Zbl 0598.68034

Math. USSR, Sb. 53, 411-419 (1986); translation from Mat. Sb., Nov. Ser. 125(167), No. 3, 410-419 (1984).
The comparison of various logics of programs and, in particular, the role of nondeterminism in dynamic logic is the main topic of the paper. The author’s main result states that it is not possible to translate the dynamic logic of regular programs, RG, into the deterministic dynamic logic of context-free programs, DC. The essential part of the proof is a theorem showing that, on some class of groups, every DC-formula is equivalent to an elementary formula. The main result then follows from the fact that all groups in this class are elementarily equivalent although there is an RG-formula which can distinguish two groups from the class considered.

MSC:

68Q65 Abstract data types; algebraic specification
68Q60 Specification and verification (program logics, model checking, etc.)
03B45 Modal logic (including the logic of norms)
03B60 Other nonclassical logic
PDFBibTeX XMLCite
Full Text: DOI