Query-based Verification of Biochemical Oscillations through Probabilistic Model Checking
Automated verification of stochastic models has been proved to be an effective technique for the analysis of a large class of stochastically behaving systems. In this paper we show how stochastic modelchecking can be effectively applied to the analysis of biological systems. We consider a few models...
Main Authors: | , , |
---|---|
Format: | Other/Unknown Material |
Language: | English |
Published: |
The Microsoft Research - University of Trento Centre for Computational and Systems Biology
2008
|
Subjects: | |
Online Access: | https://hdl.handle.net/11572/358684 |
id |
ftutrentoiris:oai:iris.unitn.it:11572/358684 |
---|---|
record_format |
openpolar |
spelling |
ftutrentoiris:oai:iris.unitn.it:11572/358684 2023-12-31T10:08:20+01:00 Query-based Verification of Biochemical Oscillations through Probabilistic Model Checking Ballarini, Paolo Mura, Ivan Mardare, Radu Ballarini, Paolo Mura, Ivan Mardare, Radu 2008 ELETTRONICO https://hdl.handle.net/11572/358684 eng eng The Microsoft Research - University of Trento Centre for Computational and Systems Biology country:ITA place:Trento ispartofseries:The Microsoft Research - Centre for Computational and Systems Biology Technical Report firstpage:1 lastpage:4 numberofpages:4 https://hdl.handle.net/11572/358684 info:eu-repo/semantics/openAccess info:eu-repo/semantics/other 2008 ftutrentoiris 2023-12-05T23:06:37Z Automated verification of stochastic models has been proved to be an effective technique for the analysis of a large class of stochastically behaving systems. In this paper we show how stochastic modelchecking can be effectively applied to the analysis of biological systems. We consider a few models of biological systems taken from the literature, and we consider both their encodings as ordinary differential equations and Markovian models. We show that stochastic model-checking verification of biological systems can complement both deterministic and stochastic simulation techniques when dealing with dynamical properties of oscillators. We demonstrate how stochastic model-checking can provide exact quantitative characterization of properties of systems exhibiting oscillatory behavior, providing insights that cannot be obtained with differential equations models and that would require a large number of runs with stochastic simulation approaches. This is the preliminary version of a paper that was published in the Proceedings of the International Workshop From Biology To Concurrency and back (FBTC 2008), satellite workshop of ICALP 2008, July 12, 2008, Reykjavik, Iceland, ENTCS 194(3). The original publication is available at DOI:10.1016/j.entcs.2009.02.002 Other/Unknown Material Iceland Università degli Studi di Trento: CINECA IRIS |
institution |
Open Polar |
collection |
Università degli Studi di Trento: CINECA IRIS |
op_collection_id |
ftutrentoiris |
language |
English |
description |
Automated verification of stochastic models has been proved to be an effective technique for the analysis of a large class of stochastically behaving systems. In this paper we show how stochastic modelchecking can be effectively applied to the analysis of biological systems. We consider a few models of biological systems taken from the literature, and we consider both their encodings as ordinary differential equations and Markovian models. We show that stochastic model-checking verification of biological systems can complement both deterministic and stochastic simulation techniques when dealing with dynamical properties of oscillators. We demonstrate how stochastic model-checking can provide exact quantitative characterization of properties of systems exhibiting oscillatory behavior, providing insights that cannot be obtained with differential equations models and that would require a large number of runs with stochastic simulation approaches. This is the preliminary version of a paper that was published in the Proceedings of the International Workshop From Biology To Concurrency and back (FBTC 2008), satellite workshop of ICALP 2008, July 12, 2008, Reykjavik, Iceland, ENTCS 194(3). The original publication is available at DOI:10.1016/j.entcs.2009.02.002 |
author2 |
Ballarini, Paolo Mura, Ivan Mardare, Radu |
format |
Other/Unknown Material |
author |
Ballarini, Paolo Mura, Ivan Mardare, Radu |
spellingShingle |
Ballarini, Paolo Mura, Ivan Mardare, Radu Query-based Verification of Biochemical Oscillations through Probabilistic Model Checking |
author_facet |
Ballarini, Paolo Mura, Ivan Mardare, Radu |
author_sort |
Ballarini, Paolo |
title |
Query-based Verification of Biochemical Oscillations through Probabilistic Model Checking |
title_short |
Query-based Verification of Biochemical Oscillations through Probabilistic Model Checking |
title_full |
Query-based Verification of Biochemical Oscillations through Probabilistic Model Checking |
title_fullStr |
Query-based Verification of Biochemical Oscillations through Probabilistic Model Checking |
title_full_unstemmed |
Query-based Verification of Biochemical Oscillations through Probabilistic Model Checking |
title_sort |
query-based verification of biochemical oscillations through probabilistic model checking |
publisher |
The Microsoft Research - University of Trento Centre for Computational and Systems Biology |
publishDate |
2008 |
url |
https://hdl.handle.net/11572/358684 |
genre |
Iceland |
genre_facet |
Iceland |
op_relation |
ispartofseries:The Microsoft Research - Centre for Computational and Systems Biology Technical Report firstpage:1 lastpage:4 numberofpages:4 https://hdl.handle.net/11572/358684 |
op_rights |
info:eu-repo/semantics/openAccess |
_version_ |
1786841012709097472 |