# Kripke automaton and observations [closed]

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?

Attempt: No


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.

• This question appears to be off-topic because it is about grading answers to your exercises. Please see this related meta discussion. If you want to ask a specific question about a specific part of your attempt, please edit the question accordingly and it may be reopened. – D.W. Oct 14 '13 at 5:13

Your answers seem correct. As for 2: one way is to simply check, a quicker way is to observe that all states go to A upon reading 1, so the sequence 001 ends in A, and A satisfies "red".

3 can be solved by the test "blue" (without any moves) and 4 can be solved with the test "red".

As for 5: in order to show that no test can differentiate B and D, observe that for the letter 1, both go to A, for the letter 0 both go to C, and both have the same light (blue). Thus, you can say that the "language" of both state is equal.

• But isn't "blue" or "red" an observation? How could it be a test as well? – redundant6939 Oct 13 '13 at 18:45
• When you write 0001blue, you mean "follow the path 0001, and check if "blue" holds in the state that you reach". Similarly, the test "blue" is just "don't move, and check whether blue holds". – Shaull Oct 13 '13 at 19:25