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

915 questions

1k answers

1.4k comments

441 users

0 votes

Can someone please explain why the answer is it is true for every state, even though our product kripke structure doesn't have any initial state also if we remove deadends then we don't have any transitions in product kripke structure. Since formula asks for all the paths that satisfy the formula why we are showing in the states? why the answer is not for any formula it won't satisfy? 

Exam paper: question 7 (b)

Exam paper: https://es.cs.uni-kl.de/teaching/vrs/exams/2018.02.14.vrs/2018.02.14.vrs.solutions.pdf

in * TF "Vis. and Sci. Comp." by (870 points)

2 Answers

+1 vote
It is because we are asking for a A-quantified formula. Such formulas hold in all states that don't have infinite outgoing paths at all which is the case here.
by (142k points)
Ok, I understand now. Thank you so much.
+1 vote
As you said. If there are no infinite transitions, then the existential formula cannot be satisfied.

If the formula is not satisfied, then its negation is satisfied. The negation of the existential formula is a universal formula. That isn't surprising. If there are no infinite paths, then all (of the zero) infinite paths satisfy any arbitrary criterion.
by (25.6k points)
Ok, I understand now. Thank you so much.

Related questions

Imprint | Privacy Policy
...