×

zbMATH — the first resource for mathematics

Temporal logic modeling of biological systems. (English) Zbl 1429.92071
Akama, Seiki (ed.), Towards paraconsistent engineering. Cham: Springer. Intell. Syst. Ref. Libr. 110, 205-226 (2016).
Summary: Metabolic networks, formed by a series of metabolic pathways, are made of intracellular and extracellular reactions that determine the biochemical properties of a cell, and by a set of interactions that guide and regulate the activity of these reactions. Cancer, for example, can sometimes appear in a cell as a result of some pathology in a metabolic pathway. Most of these pathways are formed by an intricate and complex network of chain reactions, and can be represented in a human readable form using graphs which describe the cell signaling pathways. In this paper, we define a logic, called Molecular Interaction Logic (MIL), able to represent these graphs, and we present a method to automatically translate graphs into MIL formulas. Then, we show how MIL formulas can be translated into linear time temporal logic, and then grounded into propositional classical logic. This enables us to solve complex queries on graphs using only propositional classical reasoning tools such as SAT solvers.
For the entire collection see [Zbl 1366.03010].
MSC:
92C42 Systems biology, networks
03B44 Temporal logic
03B80 Other applications of logic
Software:
MiniSat; ASSAT
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aguado, F., Cabalar, P., Diéguez, M., Pérez, G., Vidal, C.: Temporal equilibrium logic: a survey. J. Appl. Non-Class. Logics 23(1-2), 2-24 (2013) · Zbl 1400.68199
[2] Aguado, F., Cabalar, P., Pérez, G., Vidal, C.: Loop formulas for splitable temporal logic programs. In: Proceedings of the 11th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’11), pp. 80-92. Vancouver, Canada (2011) · Zbl 1327.68058
[3] Audemard, G., Simon, L.: Predicting learnt clauses quality in modern sat solver. In: Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence (IJCAI’09), pp. 399-404 (2009)
[4] Brewka, G., Eiter, T., Truszczyński, M.: Answer set programming at a glance. Commun. ACM 54(12), 92-103 (2011)
[5] Cabalar, P., Pérez, G.: Temporal equilibrium logic: a first approach. In: Proceedings of the 11th International Conference on Computer Aided Systems Theory (EUROCAST’07), pp. 241-248 (2007) · Zbl 1394.03032
[6] Clark, K.L.: Negation as failure. In: Logic and Databases, pp. 293-322. Plenum Press (1978)
[7] Déharbe, D., Fontaine, P., LeBerre, D., Mazure, B.: Computing prime implicants. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 46-52. Portland, USA (2013)
[8] Demolombe, R., Fariñas del Cerro, L., Obeid, N.: Automated reasoning in metabolic networks with inhibition. In: 13th International Conference of the Italian Association for Artificial Intelligence, AI*IA’13, pp. 37-47. Turin, Italy (2013)
[9] Demolombe, R., Fariñas del Cerro, L., Obeid, N.: Logical model for molecular interactions maps. In: Fariñas del Cerro, L., Inoue, K. (eds.) Logical Modeling of Biological Systems, pp. 93-123. Wiley (2014)
[10] Demolombe, R., Fariñas del Cerro, L., Obeid, N.: Translation of first order formulas into ground formulas via a completion theory. J. Appl. Logic 15, 130-149 (2016) · Zbl 1436.03100
[11] Een, N., Sorensson, N.: An extensible sat-solver. In: Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT2003), pp. 502-518. Santa Margherita Ligure, Italy (2003) · Zbl 1204.68191
[12] Ferraris, P., Lee, J., Lifschitz, V.: A generalization of the lin-zhao theorem. Ann. Math. Artif. Intell. 47(1-2), 79-101 (2006) · Zbl 1105.68015
[13] Jabbour, S., Marques-Silva, J., Sais, L., Salhi, Y.: Enumerating prime implicants of propositional formulae in conjunctive normal form. In: Proceedings of the 14th European Conference, JELIA 2014, pp. 152-165. Funchal, Madeira, Portugal (2014) · Zbl 1432.68327
[14] Jackson, P.: Computing prime implicates. In: Proceedings of the 20th ACM Conference on Annual Computer Science (CSC’92), pp. 65-72. Kansas City, USA (1992) · Zbl 0925.03054
[15] Jackson, P.: Computing prime implicates incrementally. In: Proceedings of the 11th International Conference on Automated Deduction (CADE’11), pp. 253-267. Saratoga Springs, NY, USA (1992) · Zbl 0925.03054
[16] Jacob, F., Monod, J.: Genetic regulatory mechanisms in the synthesis of proteins. J. Mol. Biol. 3, 318-356 (1961)
[17] Kean, A., Tsiknis, G.: An incremental method for generating prime implicants/implicates. J. Symbolic Comput. 9, 185-206 (1990) · Zbl 0704.68100
[18] Lin, F., Zhao, Y.: ASSAT: computing answer sets of a logic program by sat solvers. In: Artificial Intelligence, pp. 112-117 (2002)
[19] Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pp. 46-57. Providence, Rhode Island, USA (1977)
[20] van Iersel, M.P., Kelder, T., Pico, A.R., Hanspers, K., Coort, S., Conklin, B.R., Evelo, C.: Presenting and exploring biological pathways with PathVisio. BMC Bioinform. 9, 399 (2008)
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.