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.


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.