Algorithmic algebraic model checking I: Challenges from systems biology