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

543 users

0 votes

Thank you so much for answering my question. Its intereseting to see that

August 31,2021 Problem 6a
1) (q0 <-> a | a & Xq0) & (q1 <-> a | ┬Ča & Xq1) & (q2 <-> q1 | q0 & Xq2) & !q2 - why is !q2 added in the end?
2) in equivalence 4 (q0 <-> a | a & Xq0) is written as in next line (q0 <-> 0). I m considering this state is a self loop and cannot understand why it is negated to 0.

related to an answer for: LTL model checking - state transition
in # Study-Organisation (Master) by (850 points)

1 Answer

0 votes
I have added a conjunction with !q2 since we want to derive the transition relation for the states where !q2 holds. Note that phi&!q2=phi[q2<-0]&!q2 holds, where phi[q2<-0] denotes the formula phi where all occurrences of q2 are replaced with 0.

For the same reason, (q0 <-> a | a & Xq0) & !a is equivalent to (q0 <-> 0 | 0 & Xq0) & !a which is again equivalent to (q0 <-> 0) & !a.
by (166k points)

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...