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

Abstract

Abstract Concurrent process calculi are powerful formalisms for modelling concurrent systems. The mathematical style underlying process cal- culi allow to both model and verify properties of a system, thus pro- viding 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 informa- tion (i.e. constraints) accumulated in a global store. ntcc has also an associated temporal logic with a proof system that can be conve- niently 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 re- actions or binding affinities 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.