HAJNAL, Matej, Tatjana PETROV and 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, p. 79-95. ISBN 978-3-030-91824-8. Available from: https://dx.doi.org/10.1007/978-3-030-91825-5_5.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name DiPS: A Tool for Data-Informed Parameter Synthesis for Markov Chains from Multiple-Property Specifications
Authors HAJNAL, Matej (703 Slovakia, belonging to the institution), Tatjana PETROV and David ŠAFRÁNEK (203 Czech Republic, guarantor, belonging to the institution).
Edition Cham, Performance Engineering and Stochastic Modeling, p. 79-95, 17 pp. 2021.
Publisher Springer
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/21:00119728
Organization unit Faculty of Informatics
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
Keywords in English probabilistic model checking; parameter synthesis; DTMC
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 28/4/2022 07:58.
Abstract
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.
Links
GA18-00178S, research and development projectName: Diskrétní bifurkační analýza reaktivních systémů
Investor: Czech Science Foundation
PrintDisplayed: 18/5/2024 09:43