Model Checking Of State-Rich Formalisms (By Linking To Combination Of State-Based Formalism And Process Algebra)