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 and David ŠAFRÁNEK

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

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

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

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

Abstract

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.

Links

GA18-00178S, research and development project

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

Investor: Czech Science Foundation

Citovat

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.

@inproceedings{1845004,
   author = {Hajnal, Matej and Petrov, Tatjana and Šafránek, David},
   address = {Cham},
   booktitle = {Performance Engineering and Stochastic Modeling},
   doi = {http://dx.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  - JOUR
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 and 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, p.~79-95. ISBN~978-3-030-91824-8. Available from: https://dx.doi.org/10.1007/978-3-030-91825-5\_{}5.

Detailed Information on Publication Record