1
$\begingroup$

given a Kripke Structure I want to check if a CTL formula is satisfied or not. the CTL is: $$ AG(c \vee AX\neg E((a\vee b)Uc)) $$ I have read that it is better to write to CTL in terms of $\wedge $ and E so for instance for an inner part $AX \neg E((a\vee b)Uc) $ I have re-written as: $$ \neg EX\neg(\neg E(\neg(\neg a\wedge\neg b)Uc) $$ but it seems to be illegal CTL.

generally what is the best approach for these kinds of problems to solve. re-write the formula in terms of other operations or just draw the parse tree.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.