Skip to main content

2016 | OriginalPaper | Buchkapitel

11. Temporal Logic Modeling of Biological Systems

verfasst von : Jean-Marc Alliot, Robert Demolombe, Martín Diéguez, Luis Fariñas del Cerro, Gilles Favre, Jean-Charles Faye, Naji Obeid, Olivier Sordet

Erschienen in: Towards Paraconsistent Engineering

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
1
The Nobel prize was awarded to Monod, Jacob and Lwoff in 1965 partly for the discovery of the lac operon by Monod and Jacob [16], which was the first genetic regulatory mechanism to be understood clearly, and is now a “standard” introductory example in molecular biology classes.
 
2
It is important here to notice that lactose can be either considered as a weak endogenous variable, or as an exogenous variable if we consider that the environment is always providing “enough” lactose. It is a simple example which shows that variables in a graph can be interpreted differently according to what is going to be observed.
 
3
For a more detailed survey of temporal extension of Answer Set Programming see [1].
 
4
The dual problem, which could be easily adapted to suit our needs.
 
Literatur
1.
Zurück zum Zitat 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)MathSciNetCrossRef 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)MathSciNetCrossRef
2.
Zurück zum Zitat 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) 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)
3.
Zurück zum Zitat 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) 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.
Zurück zum Zitat Brewka, G., Eiter, T., Truszczyński, M.: Answer set programming at a glance. Commun. ACM 54(12), 92–103 (2011)CrossRef Brewka, G., Eiter, T., Truszczyński, M.: Answer set programming at a glance. Commun. ACM 54(12), 92–103 (2011)CrossRef
5.
Zurück zum Zitat 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) 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)
6.
Zurück zum Zitat Clark, K.L.: Negation as failure. In: Logic and Databases, pp. 293–322. Plenum Press (1978) Clark, K.L.: Negation as failure. In: Logic and Databases, pp. 293–322. Plenum Press (1978)
7.
Zurück zum Zitat 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) 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.
Zurück zum Zitat 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) 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.
Zurück zum Zitat 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) 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.
Zurück zum Zitat 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) 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)
11.
Zurück zum Zitat 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) 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)
12.
Zurück zum Zitat Ferraris, P., Lee, J., Lifschitz, V.: A generalization of the lin-zhao theorem. Ann. Math. Artif. Intell. 47(1–2), 79–101 (2006)MathSciNetCrossRefMATH Ferraris, P., Lee, J., Lifschitz, V.: A generalization of the lin-zhao theorem. Ann. Math. Artif. Intell. 47(1–2), 79–101 (2006)MathSciNetCrossRefMATH
13.
Zurück zum Zitat 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) 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)
14.
Zurück zum Zitat 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) 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)
15.
Zurück zum Zitat 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) 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)
16.
Zurück zum Zitat Jacob, F., Monod, J.: Genetic regulatory mechanisms in the synthesis of proteins. J. Mol. Biol. 3, 318–356 (1961)CrossRef Jacob, F., Monod, J.: Genetic regulatory mechanisms in the synthesis of proteins. J. Mol. Biol. 3, 318–356 (1961)CrossRef
17.
Zurück zum Zitat Kean, A., Tsiknis, G.: An incremental method for generating prime implicants/implicates. J. Symbolic Comput. 9, 185–206 (1990)MathSciNetCrossRefMATH Kean, A., Tsiknis, G.: An incremental method for generating prime implicants/implicates. J. Symbolic Comput. 9, 185–206 (1990)MathSciNetCrossRefMATH
18.
Zurück zum Zitat Lin, F., Zhao, Y.: ASSAT: computing answer sets of a logic program by sat solvers. In: Artificial Intelligence, pp. 112–117 (2002) Lin, F., Zhao, Y.: ASSAT: computing answer sets of a logic program by sat solvers. In: Artificial Intelligence, pp. 112–117 (2002)
19.
Zurück zum Zitat 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) 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.
Zurück zum Zitat 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)CrossRef 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)CrossRef
Metadaten
Titel
Temporal Logic Modeling of Biological Systems
verfasst von
Jean-Marc Alliot
Robert Demolombe
Martín Diéguez
Luis Fariñas del Cerro
Gilles Favre
Jean-Charles Faye
Naji Obeid
Olivier Sordet
Copyright-Jahr
2016
DOI
https://doi.org/10.1007/978-3-319-40418-9_11