 where \(^*\) stands for the iteration operator, \(S^*\) denoting an arbitrary (finite) number of iterations of program \(S\). The axiom expresses that if after any number of iterations of \(S\) the truth of \(P\) is preserved by the execution of \(S\), then, if \(P\) is true at the current state, it will also be true after any number of iterations of \(S\). A weaker form of PDL, called HML, with only an atomic action box and diamond and propositional connectives, was introduced by Hennessy &amp; Milner to reason about concurrent processes, and in particular analyze process equivalence (Hennessy and Milner 1980).