TIMED AUTOMATA MODELING OF THE PERSONALIZED TREATMENT DECISIONS IN METASTATIC CASTRATION RESISTANT PROSTATE CANCER

Purpose: The Timed Automata modeling paradigm has emerged from Computer Science as a mature tool for the functional analysis and performance evaluation of timed distributed systems. It has been applied successfully to a large variety of systems, like communication networks, manufacturing plants, and signaling pathways in human stem cells. This study is a first exploration of the suitability of Timed Automata in evaluating the potential benefits of a personalized treatment process of metastatic Castration Resistant Prostate Cancer (mCRPC).

Method: The treatment process has been modeled by creating several independent timed automata, where an automaton represents a patient, a physician, a test, or a treatment/testing guideline schedule. The automata interact with each other via message passing. Messages can be passed, asynchronously, from one automaton to one or more other automata, at any point in time, thereby triggering events and decisions in the treatment process. The automata are fully parameterized in order to deal with quantitative information.

In the automata time is continuous, and both QALYs and costs can be incorporated using (assignable) local clocks. Uncertainty can be modeled using probabilities and timing intervals that can be uniformly or exponentially distributed.

The modeling and analysis has been performed using the state-of-the-art tool UPPAAL. Behaviour like reachability of states can be checked in order to validate the functional correctness of the model. Once sufficient confidence in the correctness of model has been obtained, performance can be evaluated by using the statistical model checking facility of UPPAAL where properties are checked on repeated simulations.

Result: In a relatively short time (several days) a model has been produced that is compositional (consisting of smaller building blocks), easy to understand (also because of the visual UPPAAL interface) and easy to update. The performance of the model has been assessed using the UPAAL SMC tool. The comparison of the results of this analysis with the results of a discrete event simulation is the topic of a separate study.

Conclusion: The Timed Automata paradigm can be successfully applied to evaluate the potential benefits of a personalized treatment process  of mCRPC. The compositional nature of the resulting model provides a good separation of all relevant components. This leads to models that are easy to formulate, validate, understand, maintain and update.