In 2005, I was diagnosed with prostate cancer. This paper fits what I learned: one faces difficult choices because each cancer is different and there are many treatment options. This paper focuses on the hormone treatment that shuts down testosterone production. This makes many prostate cancer cells stop dividing. Some do not. Those that respond ultimately die. Some mutate to resist the treatment. Continuous hormone treatment selects for treatment resistant cells, so patients have to switch to an on-off treatment schedule to control the cancer. This paper proposes a way to search for schedules that will control a particular patient’s cancer for longer. The authors apply a tool (dReach). They tested it on 22 patients. This was not a full-blown clinical trial.

The tool uses model checking. Model checking is a formal logical and mathematical procedure to see if a particular property holds for an abstraction of the system being modeled. The authors’ prostate model is a hybrid automata. It has three discrete states, and in each state follows four ordinary differential equations with many parameters. The paper discusses several models and picks one. They provide evidence that this model can be fitted closely to individual patients. Recent research on the genetics of hormone-resistant prostate cancer [1] may make it necessary to update this model. The tool dReach’s search uses approximations. Researchers in model checking and hybrid systems should turn to an online article [2] for the tool’s computer science theory.