Graded-CTL: Satisfiability and Symbolic Model Checking