Process logic with regular formulas (Q1062047)

The reviewer [Acta Inf. 14, 359-369 (1980; Zbl 0423.68005)] proposed that dynamic logic invented by V. R. Pratt and temporal logic exploited for computer science by A. Pnueli and his school should be combined to yield the right process logic. In response to this suggestion, \textit{D. Harel, D. Kozen} and \textit{R. Parikh} [J. Comput. Syst. Sci. 25, 144-170 (1982; Zbl 0494.03016)] succeeded in presenting a decidable propositional process logic of a natural axiomatization. Keeping this line, the authors have made a great step toward the right process logic by using the operators chop and slice instead of f and suf. Most of the technical discussion here is devoted to showing that this new logic is more expressive than the formerly proposed one.