Most model checking techniques consider single systems. With the rise of using Software Product Line Engineering (SPLE) for critical systems there is a need for model checking techniques applicable to Software Product Lines (SPL). Inspired by Classen et al. we try to devise logics to formally describe properties suitable for the analysis of SPLs. We attempt to provide logics for both product-based and family-based model checking based on CTL. These logics allow both nested (nCTL) and single (sCTL) product-family restrictions on the specification of the SPL. Also, we provide an equivalence between nCTL and sCTL, and algorithms for both product-based and family-based model checking using sCTL and nCTL. A small toolset to use the algorithms in practice will be provided.