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.
Original languageUndefined
Title of host publicationISPOR 18th Annual European Congress Research Abstracts
Place of PublicationAmsterdam
PublisherInternational Society for Pharmacoeconomics and Outcomes Research (ISPOR)
PagesA702-A703
DOIs
StatePublished - Nov 2015

Publication series

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

Fingerprint

Timed automata
Automata
Prostate cancer
Model checking
Statistical model
Update
Paradigm
Model
Functional analysis
Discrete event simulation
Message passing
Modeling
Performance evaluation
Distributed systems
Timing
Computer science
Schedule
Simulation model
Health
Economics

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. p. A702-A703 (Value in Health; Vol. 18, No. 7).

Research output: ScientificConference contribution

@inbook{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",
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. 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: ScientificConference contribution

TY - CHAP

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)

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