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 |
|---|---|
| Abbreviated title | CONCUR 2022 |
| Conference number | 33 |
| 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