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

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-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 languageEnglish
Title of host publication33rd International Conference on Concurrency Theory, CONCUR 2022
EditorsBartek Klin, Slawomir Lasota, Anca Muscholl
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (electronic)9783959772464
Publication statusPublished - 1 Sept 2022
Peer-reviewedYes

Publication series

SeriesLeibniz International Proceedings in Informatics, LIPIcs
Volume243
ISSN1868-8969

Conference

Title33rd International Conference on Concurrency Theory, CONCUR 2022
Duration12 - 16 September 2022
CityWarsaw
CountryPoland

External IDs

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

Keywords

ASJC Scopus subject areas

Keywords

  • distribution transformer semantics, Model checking, parametric Markov chains