Global Model Checking

Question

In global model checking, if we come across AG(all states), the condition is considered satisfied.
Is this always true or only true when there are no dead-end states in the given structure?

Answer 1

You are wondering about the formula AG true, which holds in all states, including the deadend states (since those satisfy every A-formula). AG true can also be expressed in µ-calculus as nu x.[]x which can also be easily seen to be true, since []true is true and therefore the fixpoint is found after one iteration step.