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


543 users

0 votes

In the VRS exam from 16th Feb 2022 the LTL model checking problem, we get the following w-automaton. We know how to translate and draw the transition diagram except for the accepting states. How do we know what the accepting states are?

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

1 Answer

0 votes
When we have a NDet-G, NDet-F, NDet-FG or NDet-GF automaton then the accepting states are defined by the acceptance conditions G phi, F phi, FG phi, and GF phi as the set of states that satisfy phi. In the above case, there is a set of sets of accepting states, and we may list the union in the graph, but we should better use different colors for each particular state set. So, we get the accepting states always from the acceptance conditions.
by (166k points)
Thank you, but I'm still confused. As far as I understand the acceptance condition is GF(a->q1)&GF(q0->q2) but how do I get from there to the accepting states in the diagram (which I assume are the green ones)?
I don't think that the green states in the figure are the accepting states. That must be some other meaning. It rather seems to me that these are the reachable states without finally deadend states. Therefore, only the green states matter and you may ignore the others.
Imprint | Privacy Policy