Towards personalized prostate cancer therapy using delta-reachability analysis

Recent clinical studies suggest that the efficacy of hormone therapy for prostate cancer depends on the characteristics of individual patients. In this paper, we develop a computational framework for identifying patient-specific androgen ablation therapy schedules for postponing the potential cancer relapse. We model the population dynamics of heterogeneous prostate cancer cells in response to androgen suppression as a nonlinear hybrid automaton. We estimate personalized kinetic parameters to characterize patients and employ δ-reachability analysis to predict patient-specific therapeutic strategies. The results show that our methods are promising and may lead to a prognostic tool for prostate cancer therapy.

• Publication year

  2014

• Venue

  International Conference on Hybrid Systems: Computation and Control

• Publication date

  2014-10-27

• Fields of study

  Biology, Medicine, Computer Science, Engineering

• Identifiers
  DOI 10.1145/2728606.2728634arXiv 1410.7346
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• dReach: δ-Reachability Analysis for Hybrid Systems

  2015cited by this paper
• Planning as Model Checking in Hybrid Domains

  2014cited by this paper
• Mathematical modeling of PDGF-driven glioblastoma reveals optimized radiation dosing schedules.

  2014cited by this paper
• Parameter Synthesis for Cardiac Cell Hybrid Models Using δ-Decisions

  2014influential reference
• Cancer hybrid automata: Model, beliefs and therapy

  2014cited by this paper
• Parameter synthesis for polynomial biological models

  2014cited by this paper
• Parameter synthesis with IC3

  2013cited by this paper
• Advances in Prostate Cancer

  2013cited by this paper
• Flow*: An Analyzer for Non-linear Hybrid Systems

  2013cited by this paper
• Cancer statistics, 2013

  2013cited by this paper
• Statistical Model Checking Based Calibration and Analysis of Bio-pathway Models

  2013cited by this paper
• dReal: An SMT Solver for Nonlinear Theories over the Reals

  2013cited by this paper
• Satisfiability modulo ODEs

  2013cited by this paper
• A clinical data validated mathematical model of prostate cancer growth under intermittent androgen suppression therapy

  2012cited by this paper
• Delta-Decidability over the Reals

  2012cited by this paper
• SMT-Based Verification of Hybrid Systems

  2012cited by this paper
• SMT-based scenario verification for hybrid systems

  2012cited by this paper
• δ-Complete Decision Procedures for Satisfiability over the Reals

  2012cited by this paper
• Approximate probabilistic analysis of biopathway dynamics

  2012cited by this paper
• Mathematical modeling of prostate cancer progression in response to androgen ablation therapy

  2011cited by this paper
• SpaceEx: Scalable Verification of Hybrid Systems

  2011cited by this paper
• Probabilistic approximations of ODEs based bio-pathway dynamics

  2011cited by this paper
• Piecewise affine systems modelling for optimizing hormone therapy of prostate cancer

  2010cited by this paper
• Development of a mathematical model that predicts the outcome of hormone therapy for prostate cancer.

  2010cited by this paper
• Hybrid optimal scheduling for intermittent androgen suppression of prostate cancer.

  2010cited by this paper
• Intermittent androgen suppression for prostate cancer

  2010cited by this paper
• A Counterexample-Guided Approach to Parameter Synthesis for Linear Hybrid Automata

  2008cited by this paper
• A Mathematical Model of Intermittent Androgen Suppression for Prostate Cancer

  2008influential reference
• Locally advanced prostate cancer--biochemical results from a prospective phase II study of intermittent androgen suppression for men with evidence of prostate-specific antigen recurrence after radiotherapy.

  2007cited by this paper
• Locally advanced prostate cancer—biochemical results from a prospective phase II study of intermittent androgen suppression for men with evidence of prostate‐specific antigen recurrence after radiotherapy

  2007influential reference
• Final results of the Canadian prospective phase II trial of intermittent androgen suppression for men in biochemical recurrence after radiotherapy for locally advanced prostate cancer

  2006influential reference
• A mathematical investigation of the multiple pathways to recurrent prostate cancer: comparison with experimental data.

  2004influential reference
• Parameter estimation in biochemical pathways: a comparison of global optimization methods.

  2003cited by this paper
• A mathematical model of prostate tumor growth and androgen-independent relapse

  2003influential reference
• Symbolic Model Checking without BDDs

  1999cited by this paper
• The theory of hybrid automata

  1996cited by this paper
• [Theoretical considerations and initial clinical results of intermittent hormone treatment of patients with advanced prostatic carcinoma].

  1995influential reference
• Cancer statistics

  1989cited by this paper
• and as an in

  year unknowncited by this paper

• Subject-Specific Dosage Estimation for Primary Hypothyroidism Using Sparse Data

  2025cites this paper
• SMT based parameter identifiable combination detection for non-linear continuous and hybrid dynamics

  2024influential citation
• A Model Checking-based Analysis Framework for Systems Biology Models

  2020cites this paper
• Review: Mathematical Modeling of Prostate Cancer and Clinical Application

  2020cites this paper
• Lince: Lightweight Prototyping of Hybrid Programs

  2019cites this paper
• Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans

  2018cites this paper
• Optimal design of personalized prostate cancer therapy using Infinitesimal Perturbation Analysis

  2017cites this paper
• Review of stochastic hybrid systems with applications in biological systems modeling and analysis

  2017cites this paper
• Topics in perturbation analysis for Stochastic Hybrid Systems

  2016cites this paper
• Hybrid Modeling of Cancer Drug Resistance Mechanisms

  2016cites this paper
• Parameter estimation of rule-based models using statistical model checking

  2016cites this paper
• Bifurcation Analysis of Cardiac Alternans Using \delta -Decidability

  2016cites this paper
• Computational model validation using a novel multiscale multidimensional spatio-temporal meta model checking approach

  2016cites this paper
• Bifurcation Analysis of Cardiac Alternans Using δ-Decidability

  2016cites this paper
• Formal Methods for Biological Systems: Languages, Algorithms, and Applications

  2016cites this paper
• Personalized cancer therapy design: Robustness vs. optimality

  2016cites this paper
• An evolutionary-type model for tumor immunotherapy

  2015cites this paper
• Infinitesimal Perturbation Analysis for Personalized Cancer Therapy Design

  2015influential citation
• BioPSy: An SMT-based Tool for Guaranteed Parameter Set Synthesis of Biological Models

  2015cites this paper