Modelling, property verification and behavioural equivalence of lactose operon regulation

Understanding biochemical pathways is one of the biggest challenges in the field of molecular biology nowadays. Computer science can contribute in this area by providing formalisms and tools to simulate and analyse pathways. One formalism that is suited for modelling concurrent systems is Milner's Calculus of Communicating Systems (CCS). This paper shows the viability of using CCS to model and reason about biochemical networks. As a case study, we describe the regulation of lactose operon. After describing this operon formally using CCS, we validate our model by automatically checking some known properties for lactose regulation. Moreover, since biological systems tend to be very complex, we propose to use multiple descriptions of the same system at different levels of abstraction. The compatibility of these multiple views can be assured via mathematical proofs of observational equivalence.