A version of temporal logic introduced in 1977 and intended for program verification has two modalities, corresponding to dynamic logic's and modalities for a single program A, understood as the whole universe taking one step forwards in time.
O versiune de logică temporală introdusă în 1977 și destinată verificării de program are două modalități, corespunzând modalităților și ale logicii dinamice pentru un singur program A, înțelese ca întreg universul făcând un pas înainte în timp.