2026-07-25T15:15:40Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17073 2024-03-06T10:58:40Z ddc:004 open_access

Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications Baier, Christel Funke, Florian Jantsch, Simon Karimov, Toghrul Lefaucheux, Engel Ouaknine, Joël Purser, David Whiteland, Markus A. Worrell, James Model checking parametric Markov chains distribution transformer semantics 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). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christel Baier and Florian Funke and Simon Jantsch and Toghrul Karimov and Engel Lefaucheux and Joël Ouaknine and David Purser and Markus A. Whiteland and James Worrell 2022 Is Part Of LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2022.10 urn:nbn:de:0030-drops-170732 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.10 eng https://creativecommons.org/licenses/by/4.0/legalcode