Problems solving exercise 4.2

Question

In question 4.2 we're asked to transform a given FSM to a state transition diagram. Based on the specifications for the following FSM:

• I = !(p&q)
• R = !((q&o->next(q))->next(p)|p|a) = !q | !o | next(q) & !next(p) & !p & !a

following the answer on this question I came up with this:

There are neither outgoing transitions from {p} nor incoming transitions to {p} and all transitions may not contain input {a}, hence being an empty set, so only {},{} or {},{o}. Also we might have a next state that is not {q} in the cases that we're not currently in {q} or leave the state with an empty output (!o). The transitions hence should look like this:

• {q} --- !a ---> {q}
• {q} --- !a & !o ---> {q}
• {q} --- !a & !o ---> {}
• {} --- !a ---> {q}
• {} --- !a & !o ---> {q}
• {} --- !a ---> {}
• {} --- !a & !o ---> {}

If I understood the explanation of the answer to the above linked question correctly with these transitions we should be able to construct a Kripke structure. Based on the assumption that the transitions are correct I came up with the following Kripke structure:

According to this I now tried to formulate the solution for 4.2 a) which should then look like this:

init 0,1;
transitions (0,{},{},0);(0,{},{},2);(0,{},{},3);(1,{},{o},1);(1,{},{o},2);(1,{},{o},3);(2,{},{},2);(2,{},{},0);(2,{},{},1);(2,{},{},3);(3,{},{o},3);(3,{},{o},2);

However upon submitting I get a message that the solution is not correct, but I don't really know where I'm wrong as I followed the explanation of above mentioned post. So where did I go wrong? Is there actually an error in the approach or in any conversion of some equations/deriving the transitions or did I just miss to enter something that needs to be submitted alongside the "init" and "transitions" values like "labels" or anything like that?

Answer 1

Edit: Ah, sorry, my assumption was wrong. Your input was for the exercise tool. I didn't do the exercise so far. Maybe the syntax there is different. But nontheless, the Kripke structure doesn't seem to be correct.

I used the Propositional Logic Teaching Tool to get the truth table for the transition relation and used that then to come up with the FSM. I wanted to be sure about getting the correct FSM without doing any mistakes when doing it by hand. Then, I used the Automata Constructions Tool (which you probably used there) to construct a Kripke structure from the FSM (not giving the Kripke structure as input!), which I described as follows:

inputs a0,a1;
outputs o0,o1;
init 0,1;
transitions (0,a0,o0,0);(0,a0,o1,0); (0,a0,o0,1);(0,a0,o1,1); (1,a0,o0,0); (1,a0,o0,1); (1,a0,o1,1);

Note that you can't have empty sets for inputs and outputs (at least I assume that). Instead, you have to introduce new inputs for the variables a and o, e.g. for a, the input a0 is used to describe that a is false and so on.
 

Thereby, I came up with another Kripke structure than yours. But nontheless, I might have made a mistake, so please be careful!

By the way, I first was very confused that the automaton given is non-deterministic! How does that make sense when talking about Reactive Systems (which should be deterministic, or are there others?). Of course, the definitions are general and you can also get a Kripke structure from non-deterministic automatons, but it was very confusing for me in the beginning. Because this would mean, that there are several infinite computations going on in the Kripke structure simultaneously, with the system being in several different states at the same time.

Comments

It seems that we agree with the represented FSM.

About nondeterministic automata and reactive systems: That is not a contradiction. Reactive systems should be deterministic at the end. However, for verification, we often apply reductions by predicate abstraction and others, and that will lead to nondeterministic system models (since some states where merged into a single one). Thus, while the final reactive systems should be deterministic, verification still has to deal with nondeterministic models also.

---

Thank you very much!

Answer 2

First of all, I think your equivalent formulation of the transition relation is not correct, but that does not matter. You may first compute a DNF of the transition relation if you like:

    ¬p ∧ ¬a ∧ ¬next(p) ∧ next(q) ∨ 
    ¬p ∧ ¬q ∧ ¬a ∧ ¬next(p) ∨ 
    ¬p ∧ ¬a ∧ ¬o ∧ ¬next(p)

and this way, the transitions of the represented FSM are as follows:

    {q} --- !a ---> {q}
    {q} --- !a & !o ---> {}
    {} --- !a ---> {q}
    {} --- !a ---> {}

Some transitions you have listed are already subsumed by others you have listed where the output is not mentioned and therefore is a don't care value. So, the above transitions are all that you need, and your transitions are correct, but redundant.

The represented FSM looks as follows:

Taking deadend states into account, this corresponds with the following Krikpe structure:

and removing the deadend states, you will find the following part of it:

Am I right?

Comments

Then the solution should be this:

init 0,1;
transitions (0,{},{},0);(0,{},{},4);(0,{},{},1);(1,{},{o},0);(0,{},{},5);(1,{},{o},1);(1,{},{o},4);(1,{},{o},5);(4,{},{},4);(4,{},{},0);(4,{},{},1);(4,{},{},5);(5,{},{o},5);(5,{},{o},4);

However this is not correct. What is the mistake here?

---

Maybe I am wrong, but I think you want to describe the Kripke structure. As the exercises says, the syntax is different, and you must also use numbers for the states that are contiguous 0,..,n so not using 2 and 3 is not allowed. The structure above should therefore be:

    vars a,o,p,q;
    init 0;
    labels 0:; 1:o; 2:q; 3:q,o;
    transitions
        0->0; 0->1; 0->2; 0->3;
        1->0; 1->1; 1->2; 1->3;
        2->0; 2->1; 2->2; 2->3;
        3->0; 3->1; 3->2; 3->3;