VMCAI 09: LTL Generalized Model Checking Revisited

Generalized Model Checking is the mixtrue of MC with game semantic, that is , something is unfixed, and GMC try to find out definition of these unfixed entities, or decide if such definition exist, such that the concrete MC or satisfiability problom can be solved.

This topic remind me of the synthesis and fix problem, which also has some thing left to be defined.