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: | Report |
Language: | unknown |
Published: |
2008
|
Subjects: | |
Online Access: | http://eprints.biblio.unitn.it/1736/ http://eprints.biblio.unitn.it/1736/1/TR%2D05%2D2008.pdf |
id |
ftutrento:oai:eprints.biblio.unitn.it:1736 |
---|---|
record_format |
openpolar |
spelling |
ftutrento:oai:eprints.biblio.unitn.it:1736 2023-05-15T16:50:14+02:00 Query-based Verification of Biochemical Oscillations through Probabilistic Model Checking Ballarini, Paolo Mura, Ivan Mardare, Radu 2008 application/pdf http://eprints.biblio.unitn.it/1736/ http://eprints.biblio.unitn.it/1736/1/TR%2D05%2D2008.pdf unknown http://eprints.biblio.unitn.it/1736/1/TR%2D05%2D2008.pdf Ballarini, Paolo and Mura, Ivan and Mardare, Radu (2008) Query-based Verification of Biochemical Oscillations through Probabilistic Model Checking. UNSPECIFIED. QA076.7 Programming Languages - Semantics Departmental Technical Report NonPeerReviewed 2008 ftutrento 2019-12-14T18:52:25Z 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 Report Iceland University of Trento: unitn.it eprints |
institution |
Open Polar |
collection |
University of Trento: unitn.it eprints |
op_collection_id |
ftutrento |
language |
unknown |
topic |
QA076.7 Programming Languages - Semantics |
spellingShingle |
QA076.7 Programming Languages - Semantics Ballarini, Paolo Mura, Ivan Mardare, Radu Query-based Verification of Biochemical Oscillations through Probabilistic Model Checking |
topic_facet |
QA076.7 Programming Languages - Semantics |
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 |
format |
Report |
author |
Ballarini, Paolo Mura, Ivan Mardare, Radu |
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 |
publishDate |
2008 |
url |
http://eprints.biblio.unitn.it/1736/ http://eprints.biblio.unitn.it/1736/1/TR%2D05%2D2008.pdf |
genre |
Iceland |
genre_facet |
Iceland |
op_relation |
http://eprints.biblio.unitn.it/1736/1/TR%2D05%2D2008.pdf Ballarini, Paolo and Mura, Ivan and Mardare, Radu (2008) Query-based Verification of Biochemical Oscillations through Probabilistic Model Checking. UNSPECIFIED. |
_version_ |
1766040413409378304 |