Timed Automata Modeling of The Personalized Treatment Decisions In Metastatic Castration Resistant Prostate Cancer

S. Schivo, K. Degeling, Hendrik Koffijberg, M.J. IJzerman, R. Langerak

Research output: Contribution to journalMeeting AbstractAcademic

23 Downloads (Pure)


Objectives: 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. This study is a first exploration of the suitability of Timed Automata for health economic modeling, using a case study on personalized treatment for metastatic Castration Resistant Prostate Cancer (mCRPC).

Methods: 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. These automata interact via message passing and are fully parameterized with quantitative information. 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. 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. Software for building timed automata is freely available for academic use and includes procedures for statistical model checking (SMC) to validate the (internal) behavior and results of the model.

Results: In several days a Timed Automata model has been produced that is compositional, easy to understand and easy to update. The behavior and results of the model have been assessed using the SMC tool. Actual results for the mCRPC case study obtained from the Timed Automata model are compared with results of a Discrete Event Simulation model in a separate study.

Conclusions: 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.
Original languageEnglish
Article numberPRM113
Pages (from-to)A702-A703
JournalValue in health
Issue number7
Publication statusPublished - Nov 2015
EventISPOR 18th Annual European Congress 2015 - MiCo - Milano Congressi, Milan, Italy
Duration: 7 Nov 201511 Nov 2015
Conference number: 18


Dive into the research topics of 'Timed Automata Modeling of The Personalized Treatment Decisions In Metastatic Castration Resistant Prostate Cancer'. Together they form a unique fingerprint.

Cite this