The usefulness of mathematical models for the biological regulatory networks relies on the predictive capability of the models in order to suggest interesting hypotheses and suitable biological experiments. All mathematical frameworks dedicated to biological regulatory networks must manage a large number of abstract parameters, which are not directly measurable in the cell. The cornerstone to establish predictive models is the identification of the possible parameter values. Formal frameworks involve qualitative models with discrete values and computer-aided logic reasoning. They can provide the biologists with an automatic identification of the parameters via a formalization of some biological knowledge into temporal logic formulas. For pedagogical reasons, we focus on gene regulatory networks and develop a qualitative model of the detoxification of benzo[a]pyrene in human cells to illustrate the approach.