We consider the model-checking problem for parametric probabilistic
dynamical systems, formalised as Markov chains with parametric
transition functions, analysed under the distribution-transformer
semantics (in which a Markov chain induces a sequence of distributions
over states).
We examine the problem of synthesising the set of
parameter valuations of a parametric Markov chain such that the orbits
of induced state distributions satisfy a prefix-independent ω-regular
property.
Our main result establishes that in all non-degenerate
instances, the feasible set of parameters is (up to a null set)
semialgebraic, and can moreover be computed (in polynomial time
assuming that the ambient dimension, corresponding to the number of
states of the Markov chain, is fixed).
Proceedings of CONCUR 22, LIPIcs 243, 2022. 17 pages.
PDF
© 2022 Christel Baier, Florian Funke, Simon Jantsch, Toghrul
Karimov, Engel Lefaucheux, Joël Ouaknine, David Purser,
Markus A. Whiteland, and James Worrell.