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.

Olarte, C., Chiarugi, D., Falaschi, M., Hermith, D. (2016). A proof theoretic view of spatial and temporal dependencies in biochemical systems. THEORETICAL COMPUTER SCIENCE, 641, 25-42 [10.1016/j.tcs.2016.03.029].

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

Falaschi, Moreno;
2016-01-01

Abstract

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.
2016
Olarte, C., Chiarugi, D., Falaschi, M., Hermith, D. (2016). A proof theoretic view of spatial and temporal dependencies in biochemical systems. THEORETICAL COMPUTER SCIENCE, 641, 25-42 [10.1016/j.tcs.2016.03.029].
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S0304397516300184-main.pdf

accesso aperto

Tipologia: PDF editoriale
Licenza: Creative commons
Dimensione 779.01 kB
Formato Adobe PDF
779.01 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11365/1003928