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://dx.doi.org/10.1007/978-3-030-91825-5_5.
Další formáty:   BibTeX LaTeX RIS
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 (703 Slovensko, domácí), Tatjana PETROV a David ŠAFRÁNEK (203 Česká republika, garant, domácí).
Vydání Cham, Performance Engineering and Stochastic Modeling, od s. 79-95, 17 s. 2021.
Nakladatel Springer
Další údaje
Originální 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
Kód RIV RIV/00216224:14330/21:00119728
Organizační jednotka Fakulta informatiky
ISBN 978-3-030-91824-8
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-030-91825-5_5
UT WoS 000766389200005
Klíčová slova anglicky probabilistic model checking; parameter synthesis; DTMC
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 28. 4. 2022 07:58.
Anotace
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 VaVNá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ů
VytisknoutZobrazeno: 4. 5. 2024 06:00