Information Technology Reference
In-Depth Information
AG (B
→
(AF(A1) V .. V
AF(An)))
EF (
S
*
)
Action
→
S
*
( C
*
)
AX (
S
*
)
AG ( Action
→
S
*
)
( C1
*
)
Λ
..
Λ
( Cn
*
)
( C1
*
)
V
..
V
( Cn
*
)
¬M
*
Fig. 9.
Translation of EPPSL patterns into CTL-formulas
S
*
:
S1
*
:
S2
*
:
S3
*
:
S4
*
:
Fig. 10.
Example of the translation strategy for a simple EPPSL model into a CTL-formula
