It is not wise to ask for a standard procedure that may exist, but may not be efficient if applied to any problem. In general, LTL model checking is done as follows to compute the states that satisfy A phi:
- translate the negation of the LTL formula phi to an equivalent existential nondeterministic omega-automaton
- compute the product of the Kripke structure and the omega-automaton
- determine the states that have a path in the product structure that starts in an initial state of the automaton and that satisfies the acceptance condition
How these steps are done in detail, may be different for the particular example that is considered. Sometimes, a big simplification can be done by observing something, mostly by omitting unreachable states, and deadend states. That can be done in many ways, and neither is there a unique solution nor is there a general recipe; just keep your eyes open when looking at such examples.
