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

+2 votes
The que is from 2017 Aug Prob 7.b

After constructing the product we see that the  KA X K has no infinite paths. So E(phi) does not hold on any state but is  it not that A(phi) holds trivially on all the states? Why do we have to check for K ?

can someone pls explain this.
in * TF "Emb. Sys. and Rob." by (870 points)

1 Answer

+2 votes
For LTL model checking, we have to check that all initial states of a structure satisfy the LTL formula Aφ. Now, we translate ¬φ to an existential ω-automaton A∃(Q,I,R,ψ), hence, checking K ⊨ Aφ is the same as K ⊨ A¬¬φ, which is the same as K ⊨ A¬A∃(Q,I,R,ψ), and also the same as K ⊨ AA∀(Q,I,R,¬ψ). We should therefore check in the product structure KxA ⊨ A¬ψ or KxA ⊨ ¬Eψ.

In the example, the product KxA has no infinite paths, thus KxA ⊨ ¬Eψ holds, so KxA ⊨ A¬ψ holds, and therefore also K ⊨ Aφ holds, right?
by (166k points)
edited by

Related questions

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