A simplified proof of \(DDL<DL\) (Q1117214)

The main result of the paper (that the dynamic logic of deterministic flow-charts is strictly less expressive than its nondeterministic version, in symbols \(DDL<DL)\) was first announced in a paper of \textit{P. Berman}, \textit{J. Y. Halpern}, and \textit{J. Tiuryn} [Lect. Notes Comput. Sci. 140, 48-60 (1982; Zbl 0494.68032)]. But this paper contained a gap, namely, the proof of the most important ``polynomial lemma'' has been omitted. The lemma says that the number of nodes which are reachable during any computation of a deterministic flow-chart in the full binary tree of depth n, is bounded by an appropriate polynomial in n. The paper under review gives for the first time the full (and simplified) proof of the result. The result itself, that \(DDL<DL\), has been proved in a paper of the reviewer and \textit{M. A. Taitslin} [Inf. Control 57, 48-55 (1983; Zbl 0537.68037)] for the general case (for any type of tests), using quite a different idea. Yet another proof of \(DDL<DL\) in the case of atomic tests is contained in the paper of \textit{P. Urzyczyn} [Inf. Control 58, 59-87 (1983; Zbl 0552.68005)].