A proof theoretic view of spatial and temporal dependencies in biochemical systems.

The behavior of biochemical systems such as metabolic and signaling pathways may depend on either the location of the reactants or on the time needed for a reaction to occur. In this paper we propose a formalism for specifying and verifying properties of biochemical systems that combines, coherently, temporal and spatial modalities. To this aim, we consider a fragment of intuitionistic linear logic with subexponentials (SELL). The subexponential signature allows us to capture the spatial relations among the different components of the system and the timed constraints. We illustrate our approach by specifying some well-known biological systems and verifying properties of them. Moreover, we show that our framework is general enough to give a logic-based semantics to P systems. We show that the proposed logical characterizations have a strong level of adequacy. Hence, derivations in SELL follow exactly the behavior of the modeled system.