modelchecker.dk / hybrid
Enter expression:
Example: B i (<NEXT>(<SBJ>(i & Word "which")))