The number of parameters and their mutual interdependence make the identification of parameter values a hard task. A common approach is to use parameter estimation based on fitting experimental data that might be of low resolution or even unavailable. Instead of estimating parameters from data (typically time-series), an alternative approach is to specify global hypotheses about systems behaviour in terms of temporal properties and to use parameter synthesis methods based on model checking.

PITHYA is a new high-performance tool that implements the state-of-the-art parameter synthesis methods. For a given mathematical ODE model it allows to visually explore the behaviour with respect to different parameter values. Moreover, a property can be specified describing behaviour constraints, e.g., maximal reachable concentration, time ordering of events, etc. The tool is then used to automatically synthesise parameter values satisfying the property. Systems biology is often defined as the emerging discipline that asks how do the collective interactions of molecular components give rise to the phenotype of the organism. Models are being used as explanatory tools for studying organisms as biological systems. Most models can be thought of as some form of a dynamical system. This provides a unified framework in which to compare different kinds of models. Models are often complex, in the sense of having many undetermined parameters, and the parameter problem emerges thus as one of the central difficulties in the field.

Unique features of the tool are the following:

• semi-automatised generation of discrete models from differential equations
• specification of system properties in hybrid temporal logic (HUCTL)
• interactive exploration of system behaviour with respect to changes in parameters
• visualisation of model phase-space and its discrete abstraction
• visualisation of parameter synthesis results