Parameter Synthesis for Biological Models

The parameter synthesis problem consists of identifying parameter values for which a given system model satisfies a desired behaviour. We present BioPSy, a tool that performs parameter set synthesis for biological models expressed in the Systems Biology Markup Language (SBML) given a desired behaviour expressed by time-series data. Three key features of BioPSy are:

1. BioPSy computes parameter intervals, not just single values,
2. the model is formally guaranteed to satisfy the desired behaviour for the identified intervals,
3. BioPSy can handle virtually any Lipschitz-continuous ODEs, including nonlinear ones.

BioPSy is able to achieve guaranteed synthesis by utilising Satisfiability Modulo Theory (SMT) solvers to determine acceptable parameter intervals. We have successfully applied our tool to several biological models including a prostate cancer therapy model, a human starvation model, and a cell.