SMBioNet allows the selection of all models (values of parameters) associated to a given biological regulatory network which lead to a qualitative dynamics (a state transition graph) satisfying the biological knowledges (or hypothesis) on the behavior of studied system. These knowledges on the behavior, called temporal properties, can be mainly expressed as:
  a list of steady states (regular or singular),
  a list of functional feedback circuits,
  a CTL formula (checked with the NuSMV model checker).

see online : homepage