Computation Tree Logic (CTL) with Simulink Design Verifier?

I try to use the Simulink Design Verifier 2.7 to verify my Stateflow models. For many simple objectives it works fine. But, now I have to model the combined AG EF (p) operator which is defined in the Computation Tree Logic (CTL). This operator shall verify that for all states there exists at least path in which p is true in the future. Is there a way to model this operator in Simulink and verify it using the Design Verifier?