×

zbMATH — the first resource for mathematics

A proof theoretic view of spatial and temporal dependencies in biochemical systems. (English) Zbl 1344.68140
Summary: 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.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03F52 Proof-theoretic aspects of linear logic and other substructural logics
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
92C40 Biochemistry, molecular biology
Software:
Bio-PEPA; BlenX; Pesca; PRISM; SLMC
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Fages, F.; Soliman, S., Formal cell biology in biocham, (Bernardo, M.; Degano, P.; Zavattaro, G., SFM 2008, LNCS, vol. 5016, (2008), Springer), 54-80
[2] Ciocchetta, F.; Guerriero, M. L., Modelling biological compartments in bio-PEPA, Electron. Notes Theor. Comput. Sci., 227, 77-95, (2009) · Zbl 1348.92069
[3] Dematté, L.; Priami, C.; Romanel, A., The blenx language: a tutorial, (Bernardo, M.; Degano, P.; Zavattaro, G., SFM 2008, LNCS, vol. 5016, (2008), Springer), 313-365 · Zbl 1160.68678
[4] Abate, A.; Bai, Y.; Sznajder, N.; Talcott, C. L.; Tiwari, A., Quantitative and probabilistic modeling in pathway logic, (BIBE 2007, (2007), IEEE CS), 922-929
[5] Fisher, J.; Henzinger, T. A., Executable biology, (Perrone, L. F.; Lawson, B.; Liu, J.; Wieland, F. P., WSC, (2006)), 1675-1682
[6] Girard, J., Linear logic, Theoret. Comput. Sci., 50, 1-102, (1987) · Zbl 0625.03037
[7] Danos, V.; Joinet, J.; Schellinx, H., The structure of exponentials: uncovering the dynamics of linear logic proofs, (Gottlob, G.; Leitsch, A.; Mundici, D., KGC’93, LNCS, vol. 713, (1993), Springer), 159-171 · Zbl 0793.03061
[8] Nigam, V.; Olarte, C.; Pimentel, E., A general proof system for modalities in concurrent constraint programming, (D’Argenio, P. R.; Melgratti, H. C., CONCUR 2013, LNCS, vol. 8052, (2013), Springer), 410-424 · Zbl 1390.68485
[9] Olarte, C.; Pimentel, E.; Nigam, V., Subexponential concurrent constraint programming, Theoret. Comput. Sci., 606, 98-120, (2015) · Zbl 1332.68027
[10] Păun, G.; Rozenberg, G., A guide to membrane computing, Theoret. Comput. Sci., 287, 1, 73-100, (2002) · Zbl 1061.68054
[11] Bernardini, F.; Manca, V., Dynamical aspects of P systems, Biosystems, 70, 2, 85-93, (2003)
[12] Ciobanu, G.; Pan, L.; Păun, G.; Pérez-Jiménez, M. J., P systems with minimal parallelism, Theoret. Comput. Sci., 378, 1, 117-130, (2007) · Zbl 1118.68066
[13] Andreoli, J.-M., Logic programming with focusing proofs in linear logic, J. Logic Comput., 2, 3, 297-347, (1992) · Zbl 0764.03020
[14] Fages, F.; Ruet, P.; Soliman, S., Linear concurrent constraint programming: operational and phase semantics, Inform. and Comput., 165, 1, 14-41, (2001) · Zbl 1003.68065
[15] Watkins, K.; Cervesato, I.; Pfenning, F.; Walker, D., A concurrent logical framework: the propositional fragment, (Berardi, S.; Coppo, M.; Damiani, F., TYPES 2003, LNCS, vol. 3085, (2003), Springer), 355-377 · Zbl 1100.68548
[16] Tiu, A. F.; Miller, D., A proof search specification of the pi-calculus, Electron. Notes Theor. Comput. Sci., 138, 1, 79-101, (2005) · Zbl 1272.03143
[17] Cervesato, I.; Scedrov, A., Relating state-based and process-based concurrency through linear logic (full-version), Inform. and Comput., 207, 10, 1044-1077, (2009) · Zbl 1181.68168
[18] Chiarugi, D.; Falaschi, M.; Hermith, D.; Olarte, C., Verification of spatial and temporal modalities in biochemical systems, Electron. Notes Theor. Comput. Sci., 316, 29-44, (2015) · Zbl 1351.68157
[19] Bhattacharjee, M.; Raju, R.; Radhakrishnan, A., A bioinformatics resource for TWEAK-fn14 signaling pathway, J. Signal Transduct., (2012)
[20] Negri, S.; von Plato, J., Structural proof theory, (2001), Cambridge University Press · Zbl 1113.03051
[21] Miller, D.; Saurin, A., From proofs to focused proofs: a modular proof of focalization in linear logic, (Duparc, J.; Henzinger, T. A., CSL 2007, LNCS, vol. 4646, (2007), Springer), 405-419 · Zbl 1179.03064
[22] Bernardini, F.; Gheorghe, M.; Manca, V., On P systems and almost periodicity, Fund. Inform., 64, 1-4, 29-42, (2005) · Zbl 1102.68026
[23] Freund, R., Asynchronous P systems and P systems working in the sequential mode, (Mauri, G.; Paun, G.; Pérez-Jiménez, M. J.; Rozenberg, G.; Salomaa, A., WMC 2004, LNCS, vol. 3365, (2004), Springer), 36-62 · Zbl 1117.68363
[24] Maria, E. D.; Despeyroux, J.; Felty, A. P., A logical framework for systems biology, (Formal Methods in Macro-Biology - First International Conference, FMMB 2014, (2014)), 136-155 · Zbl 1402.92210
[25] Fink, S. L.; Cookson, B. T., Apoptosis, pyroptosis, and necrosis: mechanistic description of dead and dying eukaryotic cells, Infect. Immun., 84, 4, 1907-1916, (2005)
[26] Miller, D.; Nadathur, G.; Pfenning, F.; Scedrov, A., Uniform proofs as a foundation for logic programming, Ann. Pure Appl. Logic, 51, 1-2, 125-157, (1991) · Zbl 0721.03037
[27] Manna, Z.; Pnueli, A., The temporal logic of reactive and concurrent systems - specification, (1992), Springer
[28] Caires, L.; Cardelli, L., A spatial logic for concurrency - II, Theoret. Comput. Sci., 322, 3, 517-565, (2004) · Zbl 1050.68104
[29] Mardare, R.; Priami, C.; Quaglia, P.; Vagin, O., Model checking biological systems described using ambient calculus, (Danos, V.; Schächter, V., CMSB 2004, LNCS, vol. 3082, (2005), Springer), 85-103 · Zbl 1088.68645
[30] Dang, Z.; Ibarra, O. H.; Li, C.; Xie, G., On the decidability of model-checking for P systems, J. Autom. Lang. Comb., 11, 3, 279-298, (2006) · Zbl 1149.68404
[31] Clarke, E. M.; Grumberg, O.; Peled, D. A., Model checking, (2001), MIT Press
[32] Chiarugi, D.; Falaschi, M.; Hermith, D.; Olarte, C., A framework for modelling spatially dependent interactions of biological systems in CCP, (Rojas, I.; Guzman, F. M.O., IWBBIO 2014, (2014), Copicentro Editorial), 912-923
[33] Chiarugi, D.; Falaschi, M.; Olarte, C.; Palamidessi, C., A declarative view of signaling pathways, (Bodei, C.; Ferrari, G. L.; Priami, C., Programming Languages with Applications to Biology and Security, Lecture Notes in Computer Science, vol. 9465, (2015), Springer), 183-201 · Zbl 1443.92092
[34] Olarte, C.; Pimentel, E., Proving concurrent constraint programming correct, revisited, Electron. Notes Theor. Comput. Sci., 312, 179-195, (2015) · Zbl 1342.68238
[35] Saraswat, V. A.; Rinard, M. C.; Panangaden, P., Semantic foundations of concurrent constraint programming, (Wise, D. S., POPL 1991, (1991), ACM Press), 333-352
[36] Pimentel, E.; Olarte, C.; Nigam, V., A proof theoretic study of soft concurrent constraint programming, Theory Pract. Log. Program., 14, 4-5, 649-663, (2014) · Zbl 1309.68034
[37] Saeedloei, N.; Gupta, G., Timed π-calculus, (Abadi, M.; Lluch-Lafuente, A., TGC 2013, LNCS, vol. 8358, (2013), Springer), 119-135 · Zbl 1348.68169
[38] Harris, L. A.; Hogg, J. S.; Faeder, J. R., Compartmental rule-based modeling of biochemical systems, (Dunkin, A.; Ingalls, R. G.; Yücesan, E.; Rossetti, M. D.; Hill, R.; Johansson, B., WSC, (2009)), 908-919
[39] Regev, A.; Panina, E. M.; Silverman, W.; Cardelli, L.; Shapiro, E. Y., Bioambients: an abstraction for biological compartments, Theoret. Comput. Sci., 325, 1, 141-167, (2004) · Zbl 1069.68569
[40] Cardelli, L., Brane calculi, (Danos, V.; Schächter, V., CMSB 2004, LNCS, vol. 3082, (2005), Springer), 257-278 · Zbl 1088.68657
[41] Chabrier-Rivier, N.; Fages, F.; Soliman, S., The biochemical abstract machine BIOCHAM, (Danos, V.; Schächter, V., CMSB 2004, LNCS, vol. 3082, (2005), Springer), 172-191 · Zbl 1088.68817
[42] Guerriero, M. L.; Priami, C.; Romanel, A., Modeling static biological compartments with beta-binders, (Anai, H.; Horimoto, K.; Kutsia, T., AB 2007, LNCS, vol. 4545, (2007), Springer), 247-261 · Zbl 1126.92002
[43] Versari, C.; Gorrieri, R., Pi @: a pi-based process calculus for the implementation of compartmentalised bio-inspired calculi, (Bernardo, M.; Degano, P.; Zavattaro, G., SFM 2008, LNCS, vol. 5016, (2008), Springer), 449-506
[44] Hinton, A.; Kwiatkowska, M. Z.; Norman, G.; Parker, D., PRISM: a tool for automatic verification of probabilistic systems, (Hermanns, H.; Palsberg, J., TACAS 2006, LNCS, vol. 3920, (2006), Springer), 441-444
[45] Gong, H.; Zuliani, P.; Komuravelli, A.; Faeder, J. R.; Clarke, E. M., Computational modeling and verification of signaling pathways in cancer, (Horimoto, K.; Nakatsui, M.; Popov, N., ANB 2010, LNCS, vol. 6479, (2010), Springer), 117-135 · Zbl 1349.92074
[46] Gori, R.; Levi, F., An analysis for proving temporal properties of biological systems, (Kobayashi, N., APLAS 2006, LNCS, vol. 4279, (2006), Springer), 234-252 · Zbl 1168.68438
[47] Caires, L.; Cardelli, L., A spatial logic for concurrency (part I), Inform. and Comput., 186, 2, 194-235, (2003) · Zbl 1068.03022
[48] Miculan, M.; Bacci, G., Modal logics for brane calculus, (Priami, C., CMSB 2006, LNCS, vol. 4210, (2006), Springer), 1-16
[49] Bodei, C., A control flow analysis for beta-binders with and without static compartments, Theoret. Comput. Sci., 410, 33-34, 3110-3127, (2009) · Zbl 1173.68039
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.