## With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

No credit card required

In the above picture, nodes satisfying φ are shown solid (or as a shaded area), whereas ψ nodes are indicated by a circle.

The operator A U+ can be expressed by E U+ and A F+ . This characterization is similar to the definition of the unless-operator in linear temporal logic, cf. page 1648:

$\mathbf{A}\left(\phi {\mathbf{U}}^{+}\psi \right)↔\left(\mathbf{A}\left(\phi {\mathbf{W}}^{+}\psi \right)\wedge \mathbf{A}{\mathbf{F}}^{+}\psi \right)=\left(¬\mathbf{E}\left(¬\psi {\mathbf{U}}^{+}¬\left(\phi \vee \psi \right)\right)\wedge \mathbf{A}{\mathbf{F}}^{+}\psi \right).$

Therefore, it is sufficient to consider only the two basic operators E U + and A F+ in formal proofs and algorithms. Similarly, the formula E(φ W+ ψ) can be replaced by (E(φ U+ ψ) ∨ EG+ φ). However, there is no negation-free ...

## With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

No credit card required