Dynamic logic (modal logic)

Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs and later applied to more general complex behaviors arising in linguistics, philosophy, AI, and other fields.

Modal logic is characterized by the modal operators ${\displaystyle \Box p}$ (box p) asserting that ${\displaystyle p\,\!}$ is necessarily the case, and ${\displaystyle \Diamond p}$ (diamond p) asserting that ${\displaystyle p\,\!}$ is possibly the case. Dynamic logic extends this by associating to every action ${\displaystyle a\,\!}$ the modal operators ${\displaystyle [a]\,\!}$ and ${\displaystyle \langle a\rangle \,\!}$, thereby making it a multimodal logic. The meaning of ${\displaystyle [a]p\,\!}$ is that after performing action ${\displaystyle a\,\!}$ it is necessarily the case that ${\displaystyle p\,\!}$ holds, that is, ${\displaystyle a\,\!}$ must bring about ${\displaystyle p\,\!}$. The meaning of ${\displaystyle \langle a\rangle p\,\!}$ is that after performing ${\displaystyle a\,\!}$ it is possible that ${\displaystyle p\,\!}$ holds, that is, ${\displaystyle a\,\!}$ might bring about ${\displaystyle p\,\!}$. These operators are related by ${\displaystyle [a]p\equiv \neg \langle a\rangle \neg p\,\!}$ and ${\displaystyle \langle a\rangle p\equiv \neg [a]\neg p\,\!}$, analogously to the relationship between the universal (${\displaystyle \forall \,\!}$) and existential (${\displaystyle \exists \,\!}$) quantifiers.

...
Wikipedia