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

How are the transitions here solved? And how is the structure drawn? Can someone explain?

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

1 Answer

0 votes
At first, we compute the omega-automaton which has the following transition relation:

(q0 <-> b | a & next(q0)) & (q1 <-> !b & (!a | next(q1)))

As the automaton has the initial states !(q0|q1), i.e., !q0&!q1, we compute the transitions of the initial state as follows:

!q0&!q1 & (q0 <-> b | a & next(q0)) & (q1 <-> !b & (!a | next(q1)))

which is simplified as shown in the solutions using propositional logic laws to the following formula

 !q0&!q1&a&!b&!next(q0)&!next(q1)

This means that from state !q0&!q1, there is only a transition to the same state with input a&!b. In the associated Kripke structure, the states are labeled with q0,q1,a,b and it therefore has the transitions listed in the solution which means that the above formula states that there are only transitions from state {a} to anyone of the states {a},{b},{},{a,b} so that there is only one infinite path starting in the initial state which is looping on state {a}.
by (166k points)
Imprint | Privacy Policy
...