The paper “Verification of parametric Markov Automata under time-bounded reachability” by Kevin van de Glind, Matthias Volk and Tim Willemse has been accepted for publication at QEST+FORMATS 2026.

The paper introduces parametric Markov automata (pMA) in which transition rates and transition probabilities can be represented by parameters. The paper presents an analysis technique for pMA based on discretization and model checking of the resulting MDP. The approach is implemented using Storm and allows to synthesize regions which accept/violate a given reachability query.

QEST+FORMATS is part of CONFEST 2026 and takes place on September 2nd-4th, 2026 in Liverpool, UK.