We illustrate the Thesis that, to a large extend:
- biochemical systems can be identified to transition systems (of different kinds, with discrete or continuous dynamics), 
- the biological properties known from experiments can be formalized in Temporal Logic (propositional or with numerical constraints)
- and biological validation amounts to model checking in this setting.
Through models on the cell cycle control we examplify this approach together with its reverse-engineering counter-part implemented in the Biochemical Abstract Machine environment BIOCHAM, for searching parameter values and learning reaction rules from temporal logic properties.