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)\leftrightarrow \left(\mathbf{A}\left(\phi {\mathbf{W}}^{+}\psi \right)\wedge \mathbf{A}{\mathbf{F}}^{+}\psi \right)=\left(\neg \mathbf{E}\left(\neg \psi {\mathbf{U}}^{+}\neg \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 ...

Start Free Trial

No credit card required