Tweaking the Odds in Probabilistic Timed Automata

Arnd Hartmanns*, Joost-Pieter Katoen, Bram Kohlen, Jip Spel

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)
58 Downloads (Pure)


We consider probabilistic timed automata (PTA) in which probabilities can be parameters, i.e. symbolic constants. They are useful to model randomised real-time systems where exact probabilities are unknown, or where the probability values should be optimised. We prove that existing techniques to transform probabilistic timed automata into equivalent finite-state Markov decision processes (MDPs) remain correct in the parametric setting, using a systematic proof pattern. We implemented two of these parameter-preserving transformations—using digital clocks and backwards reachability—in the Modest Toolset. Using Storm ’s parameter space partitioning approach, parameter values can be efficiently synthesized in the resulting parametric MDPs. We use several case studies from the literature of varying state and parameter space sizes to experimentally evaluate the performance and scalability of this novel analysis trajectory for parametric PTA.
Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems - 18th International Conference, QEST 2021, Paris, France, August 23-27, 2021, Proceedings
EditorsAlessandro Abate, Andrea Marin
Place of PublicationCham
Number of pages20
ISBN (Electronic)978-3-030-85172-9
ISBN (Print)978-3-030-85171-2
Publication statusPublished - 19 Aug 2021
Event18th International Conference on Quantitative Evaluation of Systems, QEST 2021 - Virtual Conference
Duration: 23 Aug 202127 Aug 2021
Conference number: 18

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference18th International Conference on Quantitative Evaluation of Systems, QEST 2021
Abbreviated titleQEST 2021
CityVirtual Conference


  • 2024 OA procedure


Dive into the research topics of 'Tweaking the Odds in Probabilistic Timed Automata'. Together they form a unique fingerprint.

Cite this