Parameter Synthesis for Parametric Probabilistic Dynamical Systems and Prefix-Independent Specifications

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

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

OriginalspracheEnglisch
Titel33rd International Conference on Concurrency Theory, CONCUR 2022
Redakteure/-innenBartek Klin, Slawomir Lasota, Anca Muscholl
Herausgeber (Verlag)Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (elektronisch)9783959772464
PublikationsstatusVeröffentlicht - 1 Sept. 2022
Peer-Review-StatusJa

Publikationsreihe

ReiheLeibniz International Proceedings in Informatics, LIPIcs
Band243
ISSN1868-8969

Konferenz

Titel33rd International Conference on Concurrency Theory, CONCUR 2022
Dauer12 - 16 September 2022
StadtWarsaw
LandPolen

Externe IDs

ORCID /0000-0002-5321-9343/work/160951237

Schlagworte

ASJC Scopus Sachgebiete

Schlagwörter

  • distribution transformer semantics, Model checking, parametric Markov chains