Prostate Cancer Model

The Prostate Cancer Treatment model exhibits more nonlinear ODEs.

Dynamics

"Minimal Resistor Model"

The reachability questions are

\begin{align} \frac{dx}{dt} & = (\alpha_x(k_1+(1-k_1)\frac{z}{z+k_2}-\beta_x( (1-k_3)\frac{z}{z+k_4}+k_3)) - m_1(1-\frac{z}{z_0}))x + c_1 x \\ \frac{dy}{dt} & = m_1(1-\frac{z}{z_0})x+(\alpha_y (1- d\frac{z}{z_0}) - \beta_y)y+c_2y \\ \frac{dz}{dt} & = \frac{-z}{\tau} + c_3z \\ \frac{dv}{dt} & = (\alpha_x (k_1+(1-k_1)\frac{z}{z+k_2}-\beta_x(k_3+(1-k_3)\frac{z}{z+k_4})) \\ & \quad - m_1(1-\frac{z}{z_0}))x + c_1 x + m_1(1-\frac{z}{z_0})x+(\alpha_y (1- d\frac{z}{z_0}) - \beta_y)y+c_2y \end{align}

Hybrid System Model

Logic Encoding

Result

Reference

  1. Bing Liu, Soonho Kong, Sicun Gao, and Edmund Clarke. Parameter Identification Using Delta-Decisions for Biological Hybrid Systems, CMU SCS Technical Report, CMU-CS-13-136, 2014.