Combining formal methods and Bayesian approach for inferring discrete-state stochastic models from steady-state data

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F23%3A00134426" target="_blank" >RIV/00216224:14330/23:00134426 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1371/journal.pone.0291151" target="_blank" >https://doi.org/10.1371/journal.pone.0291151</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1371/journal.pone.0291151" target="_blank" >10.1371/journal.pone.0291151</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Combining formal methods and Bayesian approach for inferring discrete-state stochastic models from steady-state data

Popis výsledku v původním jazyce

Stochastic population models are widely used to model phenomena in different areas such as cyber-physical systems, chemical kinetics, collective animal behaviour, and beyond. Quantitative analysis of stochastic population models easily becomes challenging due to the combinatorial number of possible states of the population. Moreover, while the modeller easily hypothesises the mechanistic aspects of the model, the quantitative parameters associated to these mechanistic transitions are difficult or impossible to measure directly. In this paper, we investigate how formal verification methods can aid parameter inference for population discrete-time Markov chains in a scenario where only a limited sample of population-level data measurements-sample distributions among terminal states-are available. We first discuss the parameter identifiability and uncertainty quantification in this setup, as well as how the existing techniques of formal parameter synthesis and Bayesian inference apply. Then, we propose and implement four different methods, three of which incorporate formal parameter synthesis as a pre-computation step. We empirically evaluate the performance of the proposed methods over four representative case studies. We find that our proposed methods incorporating formal parameter synthesis as a pre-computation step allow us to significantly enhance the accuracy, precision, and scalability of inference. Specifically, in the case of unidentifiable parameters, we accurately capture the subspace of parameters which is data-compliant at a desired confidence level.

Název v anglickém jazyce

Combining formal methods and Bayesian approach for inferring discrete-state stochastic models from steady-state data

Popis výsledku anglicky

Stochastic population models are widely used to model phenomena in different areas such as cyber-physical systems, chemical kinetics, collective animal behaviour, and beyond. Quantitative analysis of stochastic population models easily becomes challenging due to the combinatorial number of possible states of the population. Moreover, while the modeller easily hypothesises the mechanistic aspects of the model, the quantitative parameters associated to these mechanistic transitions are difficult or impossible to measure directly. In this paper, we investigate how formal verification methods can aid parameter inference for population discrete-time Markov chains in a scenario where only a limited sample of population-level data measurements-sample distributions among terminal states-are available. We first discuss the parameter identifiability and uncertainty quantification in this setup, as well as how the existing techniques of formal parameter synthesis and Bayesian inference apply. Then, we propose and implement four different methods, three of which incorporate formal parameter synthesis as a pre-computation step. We empirically evaluate the performance of the proposed methods over four representative case studies. We find that our proposed methods incorporating formal parameter synthesis as a pre-computation step allow us to significantly enhance the accuracy, precision, and scalability of inference. Specifically, in the case of unidentifiable parameters, we accurately capture the subspace of parameters which is data-compliant at a desired confidence level.

Druh

J_imp - Článek v periodiku v databázi Web of Science

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/GA22-10845S" target="_blank" >GA22-10845S: Studium role polyhydroxyalkanoátů u bakterie Schlegelella thermodepolymerans – slibného bakteriálního kandidáta pro biotechnologie nové generace</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2023

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 periodika

Plos one

ISSN

1932-6203

e-ISSN

—

Svazek periodika

18

Číslo periodika v rámci svazku

11

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

26

Strana od-do

1-26

Kód UT WoS článku

001125277400020

EID výsledku v databázi Scopus

2-s2.0-85176771172