A Stochastic Concurrent Constraint Based Framework to Model and Verify Biological Systems

Concurrent process calculi are powerful formalisms for modelling concurrent systems. The mathematical style underlying process calculi allow to both model and verify properties of a system, thus providing a concrete design methodology for complex systems. ntcc , a constraints-based calculus for modeling temporal non-deterministic and asynchronous behaviour of processes has been proposed recently. Process interactions in ntcc can be determined by partial information (i.e. constraints) accumulated in a global store. ntcc has also an associated temporal logic with a proof system that can be conveniently used to formally verify temporal properties of processes. We are interested in using ntcc to model the activity of genes in biological systems. In order to account for issues such as the basal rate of reactions or binding anities of molecular components, we believe that stochastic features must be added to the calculus. In this paper we propose an extension of ntcc with various stochastic constructs. We describe the syntax and semantics of this extension together with the new temporal logic and proof system associated with it. We show the relevance of the added features by modelling a non trivial biological system: the gene expression mechanisms of the virus. We argue that this model is both more elaborate and compact than the stochastic calculus model proposed recently for the same system.