 with p an atomic proposition coming from a given set, and a a basic program coming from a given set. For formulas, the intended reading of the Boolean operators is standard, and formulas of the form \([\alpha]\varphi\) express that “every execution of program \(\alpha\) from the current state leads to a state satisfying \(\varphi\)”. For programs, while the basic programs simply represent themselves, “\(\varphi \qbin\)” is a program that ‘does nothing’ when \(\varphi\) is the case but ‘fails’ otherwise (essentially, a test for \(\varphi)\), “\(\alpha \scbin \beta\)” represents the program that results from executing \(\alpha\) and then executing \(\beta\) (their sequential composition), “\(\alpha \bcup \beta\)” represents the program that results from executing either \(\alpha\) or else \(\beta\) (their non-deterministic choice), and “\({\alpha^{\ast}}\)” represents the program that results from repeating \(\alpha\) a finite number of times \((\alpha\)’s iteration).