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

Abstract

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
PublisherSpringer International Publishing AG
Pages39-58
Number of pages20
DOIs
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
PublisherSpringer
Volume12846

Conference

Conference18th International Conference on Quantitative Evaluation of Systems, QEST 2021
Abbreviated titleQEST 2021
CityVirtual Conference
Period23/08/2127/08/21

Fingerprint

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

Cite this