Hybrid CTL (HCTL) extends the branching-time temporal logic CTL with hybrid operators that can refer to states mixing thus features from first-order logic and modal logic. The extended expressiveness of HCTL allows specifying properties to play a crucial role in analysing biological systems. An appropriate semantic structure for such systems is a collection of Kripke structures with the same state space that differ in their transition relation, and we call them coloured Kripke structures. The goal of the thesis is to propose an entirely symbolic BDD-based algorithm for model checking HCTL on coloured Kripke structures. Correctness and complexity of the algorithm should be discussed and the algorithm should be evaluated on several cases taken from systems biology.