``During'' cannot be expressed by ``after'' (Q1085154)

Classes of flowcharts and tree schemes (generally nondeterministic) and programming logics over them using three temporal operators in addition to the standard \(<P>\alpha\) (''after'') are compared. The three new ones are ''throughout'' (''during'') - \(\alpha\) holds in any (some) state in every computation of P, and ''preserves'' - if \(\alpha\) holds in some state in a computation of P, it holds in all subsequent states. While in the deterministic case, none of these increases the power of the corresponding logic, in the nondeterministic case this is no more true for ''during''. This operator can be however expressed by means of array assignments or rich tests. At least one of the proofs of the paper is not customary for the dynamic logic area applying the theory of computational complexity: The assumption that a tree scheme without ''during'' can recognize the set of bit strings with even number of 1's contradicts a result concerning Boolean circuit complexity.