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?
