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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F21%3A00119728" target="_blank" >RIV/00216224:14330/21:00119728 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-030-91825-5_5" target="_blank" >http://dx.doi.org/10.1007/978-3-030-91825-5_5</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-91825-5_5" target="_blank" >10.1007/978-3-030-91825-5_5</a>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA18-00178S" target="_blank" >GA18-00178S: Diskrétní bifurkační analýza reaktivních systémů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Performance Engineering and Stochastic Modeling

ISBN

9783030918248

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

17

Strana od-do

79-95

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Tsukuba

Datum konání akce

1. 1. 2021

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000766389200005