Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers

1.6k comments

529 users

0 votes

For the transition relation (q0 <-> !a | Xq0) & (q1 <-> a & Xq1) & (q2<-> q1 | q0 & Xq2), how do we get the truth table values? I see that SNF is used here but I tried doing on my own without using SNF like just plugging in values like how we do for symbolic computation, but that does not seem to be the case.

 Could you please explain one example atleast: when q0=q1=q2=0

in * TF "Emb. Sys. and Rob." by (1k points)

1 Answer

+1 vote
 
Best answer

For q0=q1=q2=0, we replace these variables by 0 in the transition relation, but not those behind an X-operator. Hence, from 

    (q0 <-> !a | Xq0) & (q1 <-> a & Xq1) & (q2<-> q1 | q0 & Xq2)

we get

    (0 <-> !a | Xq0) & (0 <-> a & Xq1) & (0<-> 0 | 0 & Xq2)

which is equivalent to

    !(!a | Xq0) & !(a & Xq1) 

by (166k points)
selected by
I got the same answer that you got. It seems that I made a small mistake by not further simplifying the equation which results in a & !Xq0& !Xq1. I was however aware that the "next state X" should not be substituted.

Thank you very much for the clarification.
SNF - LTL model checking

Related questions

Imprint | Privacy Policy
...