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.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.
https://hdl.handle.net/11365/1003928