title: Modelling, property verification and behavioural equivalence of lactose operon regulation.
abstract: 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.
authors.affiliation: Instituto de Informática, Universidade Federal do Rio Grande do Sul, Porto Alegre, RS, Brazil. mcpinto@inf.ufrgs.br
authors.forename: Marcelo Cezar
authors.initials: MC
authors.lastname: Pinto
authors.forename: Luciana
authors.initials: L
authors.lastname: Foss
authors.forename: José Carlos Merino
authors.initials: JC
authors.lastname: Mombach
authors.forename: Leila
authors.initials: L
authors.lastname: Ribeiro
mesh_terms: D007785:Lactose / Q000378:metabolism*; D008962:Models, Theoretical; D009876:Operon; D049490:Systems Biology
chemical_list: D007785:Lactose