This is a question concerning Kripke automaton. My answers seem a little short and I was wondering if I was missing something? Transition table of a Kripke automaton:
A -> red light is on
B and D -> blue light is on
C -> both light are on
1) Is the test 001blue satisfied by any state?
2) Is the test 001red satisfied by every state?
Attempt: Yes but I dont know how to show it.
3) Which test could tell difference btw A and C?
Attempt: test = 100both; C satisfies test, A doesnt
4) Can any test distinguish B and C?
Attempt: Yes, test = 10001blue; B satisfies test, C doesnt
5)Show that no test can tell the difference btw B and D.
Attempt: Their observations are different.