DiPS: A Tool for Data-Informed Parameter Synthesis for Markov
Chains from Multiple-Property Specifications

D 2021

DiPS: A Tool for Data-Informed Parameter Synthesis for Markov Chains from Multiple-Property Specifications

HAJNAL, Matej; Tatjana PETROV a David ŠAFRÁNEK

Základní údaje

Originální název

DiPS: A Tool for Data-Informed Parameter Synthesis for Markov Chains from Multiple-Property Specifications

Autoři

HAJNAL, Matej; Tatjana PETROV a David ŠAFRÁNEK

Vydání

Cham, Performance Engineering and Stochastic Modeling, od s. 79-95, 17 s. 2021

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/21:00119728

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-91824-8

ISSN

Klíčová slova anglicky

probabilistic model checking; parameter synthesis; DTMC

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 28. 4. 2022 07:58, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

We present a tool for inferring the parameters of a Discrete-time Markov chain (DTMC) with respect to properties written in probabilistic temporal logic (PCTL) informed by data observations. The tool combines, in a modular and user-friendly way, the existing methods and tools for parameter synthesis of DTMCs. On top of this, the tool implements several hybrid methods for the exploration of the parameter space based on utilising the intermediate results of parametric model checking – the symbolic representation of properties’ satisfaction in the form of rational functions. These methods are combined to support three different parameter exploration methods: (i) optimisation, (ii) parameter synthesis, (iii) Bayesian parameter inference. Each of the available methods makes a different trade-off between scalability and inference quality, which can be chosen by the user depending on the application context. In this paper, we present the implementation, the main features of the tool, and we evaluate its performance on several benchmarks.

Návaznosti

GA18-00178S, projekt VaV

Název: Diskrétní bifurkační analýza reaktivních systémů

Investor: Grantová agentura ČR, Diskrétní bifurkační analýza reaktivních systémů

Citovat

HAJNAL, Matej; Tatjana PETROV a David ŠAFRÁNEK. DiPS: A Tool for Data-Informed Parameter Synthesis for Markov Chains from Multiple-Property Specifications. In Ballarini et al. Performance Engineering and Stochastic Modeling. Cham: Springer, 2021, s. 79-95. ISBN 978-3-030-91824-8. Dostupné z: https://doi.org/10.1007/978-3-030-91825-5_5.

@inproceedings{1845004,
   author = {Hajnal, Matej and Petrov, Tatjana and Šafránek, David},
   address = {Cham},
   booktitle = {Performance Engineering and Stochastic Modeling},
   doi = {https://doi.org/10.1007/978-3-030-91825-5_5},
   editor = {Ballarini et al.},
   keywords = {probabilistic model checking; parameter synthesis; DTMC},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-030-91824-8},
   pages = {79-95},
   publisher = {Springer},
   title = {DiPS: A Tool for Data-Informed Parameter Synthesis for Markov Chains from Multiple-Property Specifications},
   year = {2021}
}

TY  - CONF
ID  - 1845004
AU  - Hajnal, Matej - Petrov, Tatjana - Šafránek, David
PY  - 2021
TI  - DiPS: A Tool for Data-Informed Parameter Synthesis for Markov Chains from Multiple-Property Specifications
PB  - Springer
CY  - Cham
SN  - 9783030918248
KW  - probabilistic model checking
KW  - parameter synthesis
KW  - DTMC
N2  - We present a tool for inferring the parameters of a Discrete-time Markov chain (DTMC) with respect to properties written in probabilistic temporal logic (PCTL) informed by data observations. The tool combines, in a modular and user-friendly way, the existing methods and tools for parameter synthesis of DTMCs. On top of this, the tool implements several hybrid methods for the exploration of the parameter space based on utilising the intermediate results of parametric model checking – the symbolic representation of properties’ satisfaction in the form of rational functions. These methods are combined to support three different parameter exploration methods: (i) optimisation, (ii) parameter synthesis, (iii) Bayesian parameter inference. Each of the available methods makes a different trade-off between scalability and inference quality, which can be chosen by the user depending on the application context. In this paper, we present the implementation, the main features of the tool, and we evaluate its performance on several benchmarks.
ER  -

HAJNAL, Matej; Tatjana PETROV a David ŠAFRÁNEK. DiPS: A Tool for Data-Informed Parameter Synthesis for Markov Chains from Multiple-Property Specifications. In Ballarini et al. \textit{Performance Engineering and Stochastic Modeling}. Cham: Springer, 2021, s.~79-95. ISBN~978-3-030-91824-8. Dostupné z: https://doi.org/10.1007/978-3-030-91825-5\_{}5.

Přehled o publikaci