Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen › Begutachtung
Beitragende
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
Originalsprache | Englisch |
---|---|
Titel | 33rd International Conference on Concurrency Theory, CONCUR 2022 |
Redakteure/-innen | Bartek Klin, Slawomir Lasota, Anca Muscholl |
Herausgeber (Verlag) | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
ISBN (elektronisch) | 9783959772464 |
Publikationsstatus | Veröffentlicht - 1 Sept. 2022 |
Peer-Review-Status | Ja |
Publikationsreihe
Reihe | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
Band | 243 |
ISSN | 1868-8969 |
Konferenz
Titel | 33rd International Conference on Concurrency Theory, CONCUR 2022 |
---|---|
Dauer | 12 - 16 September 2022 |
Stadt | Warsaw |
Land | Polen |
Externe IDs
ORCID | /0000-0002-5321-9343/work/160951237 |
---|
Schlagworte
ASJC Scopus Sachgebiete
Schlagwörter
- distribution transformer semantics, Model checking, parametric Markov chains