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:

enter image description here

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.

closed as off-topic by D.W., Luke Mathieson, A.Schulz, Realz Slaw, frafl Oct 17 '13 at 20:35

  • This question does not appear to be about computer science within the scope defined in the help center.
If this question can be reworded to fit the rules in the help center, please edit the question.

  • 4
    $\begingroup$ 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. $\endgroup$ – 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.

  • $\begingroup$ But isn't "blue" or "red" an observation? How could it be a test as well? $\endgroup$ – redundant6939 Oct 13 '13 at 18:45
  • 1
    $\begingroup$ 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". $\endgroup$ – Shaull Oct 13 '13 at 19:25

Not the answer you're looking for? Browse other questions tagged or ask your own question.