出版社：Centro Latinoamericano de Estudios en Informática
摘要：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 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 lamba virus. We argue that this model is both more elaborate and compact than the stochastic Pi calculus model proposed recently for the same system.
