Baier, C, Funke, F, Jantsch, S, Karimov, T, Lefaucheux, E, Ouaknine, J, Purser, D, Whiteland, MA and Worrell, J
(2022)
Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications.
In: 33rd International Conference on Concurrency Theory (CONCUR 2022).
Abstract
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).
| Item Type: | Conference or Workshop Item (Unspecified) |
|---|---|
| Divisions: | Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 29 Mar 2023 11:07 |
| Last Modified: | 04 Jul 2024 21:41 |
| DOI: | 10.4230/LIPIcs.CONCUR.2022.10 |
| Open Access URL: | https://doi.org/10.4230/LIPIcs.CONCUR.2022.10 |
| Related URLs: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3169346 |
Altmetric
Altmetric
