A Generic Framework to Model, Simulate and Verify Genetic Regulatory Networks

Abstract
Process calculi are formalisms to model concurrent systems. Their mathematical basis and compositional style make possible to decompose a system into simple and well defined processes. Interaction among them is formally defined by the semantic of the calculi. These characteristics allow one to study systems coming from different areas such as arts, engineering and sciences. In this paper we propose a generic framework to model, simulate and verify genetic regulatory networks based on a non-deterministic timed concurrent constraint calculus. This framework provides a set of process definitions to model generic/parametric components in a biological context, a simulator to observe the system evolution in time and some insights to perform formal proofs to verify and make inferences over the systems. An instantiation of the framework is presented by modeling the lactose operon.