Medications at what cost?

Timed Automata (TA), first introduced by Alur and Dill [1], is now a standard modeling formalism for describing the behaviour of real-time systems. Several mature automated model checking tools exist (e.g. Kronos, Uppaal) and have been applied to the quantitative analysis of numerous industrial case-studies.

Priced Timed Automata (PricedTA) [2] extend timed automata with further time-dependent variables that can be used for the specification of the accumulation of cost during behaviour. This is achieved by associating cost to actions on transitions or the time spent at locations.

We have worked on solutions for optimal paths for medications for patients with multimorbidities [3,4]. This approach has explored the use of constraint solvers and further annotations to try to find such paths. Here we want to explore PricedTA to obtain optimal solutions with respect to different cost parameters: medication efficacy, cost, quality of life (e.g., less visits to the hospital for treatment, etc). The outcome should be a more efficient interplay between (timed) automata and constraint-solver based solutions to improve the understanding of different parameters across treatment plans.




[1] R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science,126(2):183–235, 1994.

[2] Gerd Behrmann, Kim G. Larsen, and Jacob I. Rasmussen: Priced Timed Automata: Algorithms and Applications. In: de Boer F.S., Bonsangue M.M., Graf S., de Roever WP. (eds) Formal Methods for Components and Objects. FMCO 2004. LNCS 3657. Springer (2004)

[3] J. Bowles and M. Caminati: A Flexible Approach for Finding Optimal Paths with Minimal Conflicts. In: Duan Z., Ong L. (eds) Formal Methods and Software Engineering. ICFEM 2017. LNCS 10610, pp. 209-225. Springer (2017).

[4] A. Kovalov and J. Bowles: Avoiding medication conflicts for patients with multimorbidities. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 376–390. Springer (2016). doi:10.1007/978-3-319-33693-0_24