Stochastic Petri nets (SPN) are a form of Petri net where the transitions fire after a probabilistic and randomly determined delay. They are adopted in a wide range of appli- cations thanks to their capability of incorporating randomness in the models and taking into account possible fluctuations and environmental noise. In Systems Biology, they are becoming a reference formalism to model metabolic networks, in which the noise due to molecule interactions in the environment plays a crucial role. Some frameworks have been proposed to implement and dynamically simulate SPN. Nevertheless, they do not allow for automatic model parametrization, which is a crucial task to identify the network configurations that lead the model to satisfy temporal properties of the model. This paper presents a framework that synthesizes the SPN models into SystemC code. The framework allows the user to formally define the network properties to be observed and to automatically extrapolate, thorough Assertion-based Verification (ABV), the parameter configurations that lead the network to satisfy such properties. We applied the framework to implement and simulate a complex biological network, i.e., the purine metabolism, with the aim of reproducing the metabolomics data obtained in-vitro from naive lymphocytes and autoreactive T cells implicated in the induction of experimental autoimmune disorders.
Efficient Simulation and Parametrization of Stochastic Petri Nets in SystemC: A Case study from Systems Biology
Simone Caligola;Tommaso Carlucci;Franco Fummi;Carlo Laudanna;Gabriela Constantin;Nicola Bombieri;Rosalba Giugno
2019-01-01
Abstract
Stochastic Petri nets (SPN) are a form of Petri net where the transitions fire after a probabilistic and randomly determined delay. They are adopted in a wide range of appli- cations thanks to their capability of incorporating randomness in the models and taking into account possible fluctuations and environmental noise. In Systems Biology, they are becoming a reference formalism to model metabolic networks, in which the noise due to molecule interactions in the environment plays a crucial role. Some frameworks have been proposed to implement and dynamically simulate SPN. Nevertheless, they do not allow for automatic model parametrization, which is a crucial task to identify the network configurations that lead the model to satisfy temporal properties of the model. This paper presents a framework that synthesizes the SPN models into SystemC code. The framework allows the user to formally define the network properties to be observed and to automatically extrapolate, thorough Assertion-based Verification (ABV), the parameter configurations that lead the network to satisfy such properties. We applied the framework to implement and simulate a complex biological network, i.e., the purine metabolism, with the aim of reproducing the metabolomics data obtained in-vitro from naive lymphocytes and autoreactive T cells implicated in the induction of experimental autoimmune disorders.File | Dimensione | Formato | |
---|---|---|---|
main.pdf
accesso aperto
Tipologia:
Documento in Pre-print
Licenza:
Creative commons
Dimensione
761.02 kB
Formato
Adobe PDF
|
761.02 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.