1Carnegie Mellon University CTL, CTL*, LTLFlavio LerdaBug Catching 15-398CTL, CTL*, LTL2Carnegie Mellon University CTL, CTL*, LTLFlavio LerdaBug Catching 15-398An example• We saw that AF AG p and AFG p are not equivalent3Carnegie Mellon University CTL, CTL*, LTLFlavio LerdaBug Catching 15-398An example• We saw that AF AG p and AFG p are not equivalent4Carnegie Mellon University CTL, CTL*, LTLFlavio LerdaBug Catching 15-398An example• We saw that AF AG p and AFG p are not equivalent• We claimed that AFG p has not equivalent CTL formula5Carnegie Mellon University CTL, CTL*, LTLFlavio LerdaBug Catching 15-398An example• We saw that AF AG p and AFG p are not equivalent• We claimed that AFG p has not equivalent CTL formula• What about AF EG p and AFG p?6Carnegie Mellon University CTL, CTL*, LTLFlavio LerdaBug Catching 15-398An example• What about AF EG p and AFG p?7Carnegie Mellon University CTL, CTL*, LTLFlavio LerdaBug Catching 15-398An example• What about AF EG p and AFG
View Full Document