Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed › peer-review
Contributors
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).
Details
Original language | English |
---|---|
Title of host publication | 33rd International Conference on Concurrency Theory, CONCUR 2022 |
Editors | Bartek Klin, Slawomir Lasota, Anca Muscholl |
Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
ISBN (electronic) | 9783959772464 |
Publication status | Published - 1 Sept 2022 |
Peer-reviewed | Yes |
Publication series
Series | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
Volume | 243 |
ISSN | 1868-8969 |
Conference
Title | 33rd International Conference on Concurrency Theory, CONCUR 2022 |
---|---|
Duration | 12 - 16 September 2022 |
City | Warsaw |
Country | Poland |
External IDs
ORCID | /0000-0002-5321-9343/work/160951237 |
---|
Keywords
ASJC Scopus subject areas
Keywords
- distribution transformer semantics, Model checking, parametric Markov chains