×

zbMATH — the first resource for mathematics

Verification of spatial and temporal modalities in biochemical systems. (English) Zbl 1351.68157
Pauleve, Loic (ed.) et al., Post-proceedings of the 5th international workshop on static analysis and systems biology (SASB 2014), Munich, Germany, September 10, 2014. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 316, 29-44 (2015).
Summary: Biochemical systems such as metabolic and signaling pathways tend to be arranged in a physical space: the product of one reaction must be in the right place to become the reactant for the subsequent reaction in the pathway. Moreover, in some cases, the behavior of the systems can depend on both, the location of the reactants as well as on the time needed for the reaction to occur. We address the problem of specifying and verifying properties of biochemical systems that exhibit both temporal and spatial modalities at the same time. For that, we use as specification language 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 for reactions to occur. We show that our framework is general enough to give a declarative semantics to P-Systems and we show that such logical characterization has a strong level of adequacy. Hence, derivations in SELL follow exactly the behavior of the modeled system.
For the entire collection see [Zbl 1329.92010].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
92C40 Biochemistry, molecular biology
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abate, Alessandro; Bai, Yu; Sznajder, Nathalie; Talcott, Carolyn L.; Tiwari, Ashish, Quantitative and probabilistic modeling in pathway logic, (Proceedings of BIBE 2007, (2007), IEEE), 922-929
[2] Andreoli, Jean-Marc, Logic programming with focusing proofs in linear logic, J. Log. Comput., 2, 3, 297-347, (1992) · Zbl 0764.03020
[3] Bernardini, Francesco; Manca, Vincenzo, Dynamical aspects of p systems, Biosystems, 70, 2, 85-93, (2003), Cell Computing · Zbl 1023.68032
[4] Bernardo, Marco, SFM 2008, (Degano, Pierpaolo; Zavattaro, Gianluigi, Parallel Computing Technologies, LNCS, vol. 5016, (2008), Springer)
[5] Mitali Bhattacharjee, Rajesh Raju, Aneesha Radhakrishnan, et al., A bioinformatics resource for tweak-fn14 signaling pathway, Journal of Signal Transduction 2012, 2012.
[6] Chiara, Bodei, A control flow analysis for beta-binders with and without static compartments, Theor. Comput. Sci., 410, 33-34, 3110-3127, (2009) · Zbl 1173.68039
[7] Bortolussi, Luca; Policriti, Alberto, Modeling biological systems in stochastic concurrent constraint programming, Constraints, 13, 1-2, 66-90, (2008) · Zbl 1144.92001
[8] Brodo, Linda; Degano, Pierpaolo; Priami, Corrado, A stochastic semantics for bioambients, (Malyshkin, Victor, Parallel Computing Technologies, LNCS, vol. 4671, (2007), Springer Berlin Heidelberg), 22-34
[9] Caires, Luís; Cardelli, Luca, A spatial logic for concurrency (part I), Inf. Comput., 186, 2, 194-235, (2003) · Zbl 1068.03022
[10] Cardelli, Luca, Brane calculi, (Danos, Vincent; Schachter, Vincent, CMSB, LNCS, vol. 3082, (2005), Springer Berlin Heidelberg), 257-278 · Zbl 1088.68657
[11] Chabrier-Rivier, Nathalie; Fages, François; Soliman, Sylvain, The biochemical abstract machine BIOCHAM, (Danos, Vincent; Schächter, Vincent, CMSB 2004, LNCS, vol. 3082, (2004), Springer), 172-191 · Zbl 1088.68817
[12] Chaouiya, Claudine, Petri net modelling of biological networks, Brief in Bioinformatics, 8, 4, 210-219, (2007)
[13] Kaustuv Chaudhuri, Joelle Despeyroux, A Hybrid Linear Logic for Constrained Transition Systems with Applications to Molecular Biology. Research Report, 2009. · Zbl 1359.03027
[14] Chiarugi, D.; Falaschi, M.; Hermith, D.; Olarte, C., A framework for modelling spatially dependent interactions of biological systems in ccp, (Proc. of IWBBIO’14, (2014)), in press
[15] Davide Chiarugi; Falaschi, Moreno; Hermith, Diana; Guzman, Michell; Olarte, Carlos, Simulating signalling pathways with bioways, Electr. Notes Theor. Comput. Sci., 293, 17-34, (2013)
[16] Davide Chiarugi; Falaschi, Moreno; Olarte, Carlos; Palamidessi, Catuscia, Compositional modelling of signalling pathways in timed concurrent constraint programming, (Zhang, Aidong; Borodovsky, Mark; Özsoyoglu, Gultekin; Mikler, Armin R., Proceedings of BCB 2010, (2010), ACM), 414-417
[17] Davide Chiarugi; Hermith, Diana; Falaschi, Moreno; Olarte, Carlos, Verification of spatial and temporal modalities in biochemical systems, (2014), ECT, Universidade Federal do Rio Grande do Norte, Available at · Zbl 1351.68157
[18] Ciliberto, Andrea; Novak, Béla; Tyson, John J., Steady states and oscillations in the p53/mdm2 network, Cell Cycle, 4, 3, 488-493, (2005)
[19] Ciocchetta, Federica; Degasperi, Andrea; Heath, JohnK; Hillston, Jane, Modelling and analysis of the nf-?b pathway in bio-pepa, (Priami, Corrado; Breitling, Rainer; Gilbert, David; Heiner, Monika; Uhrmacher, Adelinde M., Transactions on Computational Systems Biology XII, LNCS, vol. 5945, (2010), Springer Berlin Heidelberg), 229-262
[20] Ciocchetta, Federica; Guerriero, Maria Luisa, Modelling biological compartments in bio-pepa, Electronic Notes in Theoretical Computer Science, vol. 227, 77-95, (2009) · Zbl 1348.92069
[21] Ciocchetta, Federica; Bio-pepa, Jane Hillston, An extension of the process algebra PEPA for biochemical networks, Electronic Notes in Theoretical Computer Science, 194, 3, 103-117, (2008) · Zbl 1279.68254
[22] Clavel, Manuel; Durán, Francisco; Eker, Steven; Lincoln, Patrick; Martí-Oliet, Narciso; Meseguer, José; Quesada, Jose F., The maude system, (Narendran, Paliath; Rusinowitch, Michaël, Proc. of RTA-99, LNCS, vol. 1631, (1999), Springer), 240-243
[23] Danos, Vincent; Joinet, Jean-Baptiste; Schellinx, Harold, The structure of exponentials: uncovering the dynamics of linear logic proofs, (Gottlob, Georg; Leitsch, Alexander; Mundici, Daniele, Kurt Gödel Colloquium, LNCS, vol. 713, (1993), Springer), 159-171 · Zbl 0793.03061
[24] Degano, Pierpaolo; Prandi, Davide; Priami, Corrado; Quaglia, Paola, Beta-binders for biological quantitative experiments, Electr. Notes Theor. Comput. Sci., 164, 3, 101-117, (2006)
[25] Dematté, Lorenzo; Priami, Corrado; Romanel, Alessandro, The blenx language: A tutorial, (Bernardo, Marco; Degano, Pierpaolo; Zavattaro, Gianluigi, Formal Methods for Computational Systems Biology, LNCS, vol. 5016, (2008), Springer Berlin, Heidelberg), 313-365
[26] Faeder, James R.; Blinov, MichaelL; Hlavacek, William S., Rule-based modeling of biochemical systems with bionetgen, (Maly, Ivan V., Systems Biology, Methods in Molecular Biology, vol. 500, (2009), Humana Press), 113-167
[27] Fages, François; Ruet, Paul; Soliman, Sylvain, Linear concurrent constraint programming: operational and phase semantics, Inf. Comput., 165, 1, 14-41, (2001) · Zbl 1003.68065
[28] François Fages, Sylvain Soliman, Formal cell biology in biocham, in: Bernardo et al, vol. 4, pp. 54-80.
[29] Jasmin Fisher, Thomas A. Henzinger, Executable biology, in: Perrone et al, vol. 44, pp. 1675-1682.
[30] Girard, Jean-Yves, Linear logic. Theor. Comput. Sci., 50, 1-102, (1987) · Zbl 0625.03037
[31] Gong, Haijun; Zuliani, Paolo; Komuravelli, Anvesh; Faeder, James R.; Clarke, Edmund M., Computational modeling and verification of signaling pathways in cancer, (ANB, (2010)), 117-135 · Zbl 1349.92074
[32] Gori, Roberta; Levi, Francesca, An analysis for proving temporal properties of biological systems, (Kobayashi, Naoki, Proc. of APLAS 2006, LNCS, vol. 4279, (2006), Springer), 234-252 · Zbl 1168.68438
[33] Guerriero, Maria Luisa; Priami, Corrado, Causality and concurrency in beta-binders, (2006), University of Trento, Technical report
[34] Guerriero, Maria Luisa; Priami, Corrado; Romanel, Alessandro, Modeling static biological compartments with beta-binders, (Anai, Hirokazu; Horimoto, Katsuhisa; Kutsia, Temur, Proc. of AB 2007, LNCS, vol. 4545, (2007), Springer), 247-261 · Zbl 1126.92002
[35] Harris, Leonard A.; Hogg, Justin S.; Faeder, James R., Compartmental rule-based modeling of biochemical systems, (Dunkin, Ann; Ingalls, Ricki G.; Yücesan, Enver; Rossetti, Manuel D.; Hill, Ray; Johansson, Björn, Proc. of WSC 2009, (2009), WSC), 908-919
[36] Hermith, Diana; Olarte, Carlos; Rueda, Camilo; Valencia, Frank D., Modeling cellular signaling systems: an abstraction-refinement approach, (Rocha, Miguel P.; Corchado Rodríguez, Juan M.; Fdez-Riverola, Florentino; Valencia, Alfonso, Proc. of PACBB 2011, Advances in Intelligent and Soft Computing, vol. 93, (2011), Springer), 321-328
[37] Hinton, Andrew; Kwiatkowska, Marta; Norman, Gethin; Prism, David Parker, A tool for automatic verification of probabilistic systems, (Hermanns, Holger; Palsberg, Jens, TACAS 2006, LNCS, vol. 3920, (2006), Springer Berlin Heidelberg), 441-444
[38] Lincoln, Patrick; Tiwari, Ashish, Symbolic systems biology: hybrid modeling and analysis of biological networks, (Alur, Rajeev; Pappas, George J., Proc. of HSCC 2004, LNCS, vol. 2993, (2004), Springer), 660-672 · Zbl 1135.93308
[39] Nagasaki, M.; Doi, A.; Matsuno, H.; Miyano, S., A versatile Petri net based architecture for modeling and simulation of complex biological processes, Genome Inform., 15, 1, 180-197, (2004)
[40] Marino, Miculan; Bacci, Giorgio, Modal logics for brane calculus, (Priami, Corrado, CMSB 2006, LNCS, vol. 4210, (2006), Springer Berlin, Heidelberg), 1-16
[41] Nielsen, M.; Palamidessi, C.; Valencia, F., Temporal concurrent constraint programming: denotation, logic and applications, Nordic Journal of Computing, 9, 1, 145-188, (2002) · Zbl 1018.68019
[42] Nigam, Vivek; Olarte, Carlos; Pimentel, Elaine, A general proof system for modalities in concurrent constraint programming, (D’Argenio, Pedro R.; Melgratti, Hernán C., CONCUR, LNCS, vol. 8052, (2013), Springer), 410-424 · Zbl 1390.68485
[43] Olarte, Carlos; Nigam, Vivek; Pimentel, Elaine, Dynamic spaces in concurrent constraint programming, Electr. Notes Theor. Comput. Sci., 305, 103-121, (2014) · Zbl 1335.68180
[44] Felipe Perrone, L.; Lawson, Barry; Liu, Jason; Wieland, Frederick P., Proc. of WSC, (2006)
[45] Phillips, Andrew; Cardelli, Luca, Efficient, correct simulation of biological processes in the stochastic pi-calculus, (Calder, Muffy; Gilmore, Stephen, CMSB, LNCS, vol. 4695, (2007), Springer Berlin, Heidelberg), 184-199
[46] Păun, Gheorghe, From cells to computers: computing with membranes (p systems), Biosystems, 59, 3, 139-158, (2001)
[47] Regev, Aviv; Panina, Ekaterina M.; Silverman, William; Cardelli, Luca; Shapiro, Ehud, Bioambients: an abstraction for biological compartments, Theoretical Computer Science, 325, 1, 141-167, (2004) · Zbl 1069.68569
[48] De Ronde, Jorma J.; Ndjehan, Cecile Petmi, Modelling networks and pathways in systems biology, (2005/2006), Dublin City University, School of Computing, Technical report
[49] Saeedloei, Neda; Gupta, Gopal, Timed π-calculus, (Abadi, Martín; Lluch-Lafuente, Alberto, TGC 2013, LNCS, vol. 8358, (2013), Springer), 119-135 · Zbl 1348.68169
[50] Saraswat, Vijay A.; Rinard, Martin C.; Panangaden, Prakash, Semantic foundations of concurrent constraint programming, (Wise, David S., POPL, (1991), ACM Press), 333-352
[51] Talcott, Carolyn, Pathway logic, (Bernardo, Marco; Degano, Pierpaolo; Zavattaro, Gianluigi, Formal Methods for Computational Systems Biology, LNCS, vol. 5016, (2008), Springer Berlin, Heidelberg), 21-53
[52] Carolyn L. Talcott, Symbolic modeling of signal transduction in pathway logic, in: Perrone et al, vol. 44, pp. 1656-1665.
[53] Cristian Versari, Roberto Gorrieri pi@, A pi-based process calculus for the implementation of compartmentalised bio-inspired calculi, in: Bernardo et al, vol. 4, pp. 449-506.
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.