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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Publication series

NameValue in Health
PublisherInternational Society for Pharmacoeconomics and Outcomes Research (ISPOR)
No.7
Volume18
ISSN (Print)1098-3015
ISSN (Electronic)1524-4733

Conference

ConferenceISPOR 18th Annual European Congress 2015
CountryItaly
CityMilan
Period7/11/1511/11/15
Internet address

Keywords

  • EWI-26885
  • METIS-316857
  • IR-100077

Cite this

Schivo, S., Degeling, K., Degeling, K., Koffijberg, H., IJzerman, M. J., & Langerak, R. (2015). PRM113 - Timed Automata Modeling of The Personalized Treatment Decisions In Metastatic Castration Resistant Prostate Cancer. In ISPOR 18th Annual European Congress Research Abstracts (pp. A702-A703). (Value in Health; Vol. 18, No. 7). Amsterdam: International Society for Pharmacoeconomics and Outcomes Research (ISPOR). DOI: 10.1016/j.jval.2015.09.2630
Schivo, Stefano ; Degeling, K. ; Degeling, Koen ; Koffijberg, Hendrik ; IJzerman, Maarten Joost ; Langerak, Romanus. / PRM113 - Timed Automata Modeling of The Personalized Treatment Decisions In Metastatic Castration Resistant Prostate Cancer. ISPOR 18th Annual European Congress Research Abstracts. Amsterdam : International Society for Pharmacoeconomics and Outcomes Research (ISPOR), 2015. pp. A702-A703 (Value in Health; 7).
@inproceedings{2e686ac7d4074f0f8e0afec126f5f0b6,
title = "PRM113 - Timed Automata Modeling of The Personalized Treatment Decisions In Metastatic Castration Resistant Prostate Cancer",
abstract = "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.",
keywords = "EWI-26885, METIS-316857, IR-100077",
author = "Stefano Schivo and K. Degeling and Koen Degeling and Hendrik Koffijberg and IJzerman, {Maarten Joost} and Romanus Langerak",
note = "eemcs-eprint-26885",
year = "2015",
month = "11",
doi = "10.1016/j.jval.2015.09.2630",
language = "Undefined",
series = "Value in Health",
publisher = "International Society for Pharmacoeconomics and Outcomes Research (ISPOR)",
number = "7",
pages = "A702--A703",
booktitle = "ISPOR 18th Annual European Congress Research Abstracts",

}

Schivo, S, Degeling, K, Degeling, K, Koffijberg, H, IJzerman, MJ & Langerak, R 2015, PRM113 - Timed Automata Modeling of The Personalized Treatment Decisions In Metastatic Castration Resistant Prostate Cancer. in ISPOR 18th Annual European Congress Research Abstracts. Value in Health, no. 7, vol. 18, International Society for Pharmacoeconomics and Outcomes Research (ISPOR), Amsterdam, pp. A702-A703, ISPOR 18th Annual European Congress 2015, Milan, Italy, 7/11/15. DOI: 10.1016/j.jval.2015.09.2630

PRM113 - Timed Automata Modeling of The Personalized Treatment Decisions In Metastatic Castration Resistant Prostate Cancer. / Schivo, Stefano; Degeling, K.; Degeling, Koen; Koffijberg, Hendrik; IJzerman, Maarten Joost; Langerak, Romanus.

ISPOR 18th Annual European Congress Research Abstracts. Amsterdam : International Society for Pharmacoeconomics and Outcomes Research (ISPOR), 2015. p. A702-A703 (Value in Health; Vol. 18, No. 7).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

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

AU - Schivo,Stefano

AU - Degeling,K.

AU - Degeling,Koen

AU - Koffijberg,Hendrik

AU - IJzerman,Maarten Joost

AU - Langerak,Romanus

N1 - eemcs-eprint-26885

PY - 2015/11

Y1 - 2015/11

N2 - 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.

AB - 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.

KW - EWI-26885

KW - METIS-316857

KW - IR-100077

U2 - 10.1016/j.jval.2015.09.2630

DO - 10.1016/j.jval.2015.09.2630

M3 - Conference contribution

T3 - Value in Health

SP - A702-A703

BT - ISPOR 18th Annual European Congress Research Abstracts

PB - International Society for Pharmacoeconomics and Outcomes Research (ISPOR)

CY - Amsterdam

ER -

Schivo S, Degeling K, Degeling K, Koffijberg H, IJzerman MJ, Langerak R. PRM113 - Timed Automata Modeling of The Personalized Treatment Decisions In Metastatic Castration Resistant Prostate Cancer. In ISPOR 18th Annual European Congress Research Abstracts. Amsterdam: International Society for Pharmacoeconomics and Outcomes Research (ISPOR). 2015. p. A702-A703. (Value in Health; 7). Available from, DOI: 10.1016/j.jval.2015.09.2630