Es gelten folgende Entsprechungen:
A
U
(
ϕ
1
,
ϕ
2
)
=
μ
X
.
ϕ
2
∨
(
ϕ
1
∧
[
]
X
∧
<>
t
r
u
e
)
{\displaystyle {\mathsf {AU}}\left(\phi _{1},\phi _{2}\right)=\mu X.\phi _{2}\vee \left(\phi _{1}\wedge []X\wedge <>{\mathsf {true}}\right)}
E
U
(
ϕ
1
,
ϕ
2
)
=
μ
X
.
ϕ
2
∨
(
ϕ
1
∧
[
]
X
)
{\displaystyle {\mathsf {EU}}\left(\phi _{1},\phi _{2}\right)=\mu X.\phi _{2}\vee \left(\phi _{1}\wedge []X\right)}
Mit diesen beiden Operatoren lassen sich alle anderen CTL-Operatoren erzeugen. Es gibt nämlich folgende Entsprechungen (vorrausgesetzt das untill ist ein strong-until ):
A
F
(
ϕ
)
=
A
U
(
t
r
u
e
,
ϕ
)
{\displaystyle {\mathsf {AF}}(\phi )={\mathsf {AU}}({\mathsf {true}},\phi )}
E
F
(
ϕ
)
=
E
U
(
t
r
u
e
,
ϕ
)
{\displaystyle {\mathsf {EF}}(\phi )={\mathsf {EU}}({\mathsf {true}},\phi )}
A
G
(
ϕ
)
=
¬
E
F
(
¬
ϕ
)
{\displaystyle {\mathsf {AG}}(\phi )=\neg {\mathsf {EF}}(\neg \phi )}
E
G
(
ϕ
)
=
¬
A
F
(
¬
ϕ
)
{\displaystyle {\mathsf {EG}}(\phi )=\neg {\mathsf {AF}}(\neg \phi )}
![{\displaystyle {\mathsf {AU}}\left(\phi _{1},\phi _{2}\right)=\mu X.\phi _{2}\vee \left(\phi _{1}\wedge []X\wedge <>{\mathsf {true}}\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/75c6b18a36beb445fa757fd709dfb2bea81ea00d)
![{\displaystyle {\mathsf {EU}}\left(\phi _{1},\phi _{2}\right)=\mu X.\phi _{2}\vee \left(\phi _{1}\wedge []X\right)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e49bc67707f51723cd4159166835753b2dd7d095)
