Published in Volume XXI, Issue 2, 2011, pages 249-282
Authors: J. Steggles
Abstract
Multi-valued networks (MVNs) provide a simple yet expressive qualitative state based modelling approach for biological systems. In this paper we develop an abstraction theory for asynchronous MVNs that allows the state space of a model to be reduced while preserving key properties. The abstraction theory therefore provides a mechanism for coping with the state space explosion problem and supports the analysis and comparison of MVNs. We take as our starting point the abstraction theory for synchronous MVNs which uses the under- approximation approach of trace set inclusion. We show this definition of asynchronous abstraction allows the sound inference of analysis properties and preserves other interesting model properties. One problem that arises in the asynchronous case is that the trace set of an MVN can be infinite making a simple trace set inclusion check infeasible. To address this we develop a decision procedure for checking asynchronous abstractions based on using the finite state graph of an asynchronous MVN to reason about its trace semantics and formally show that this decision procedure is correct. We illustrate the abstraction techniques developed by considering two detailed case studies in which asynchronous abstractions are identified and validated for existing asynchronous MVN models taken from the literature.
Full Text (PDF)References
[1] T. Akutsu, S. Miyano and S. Kuhara, Identification of genetic networks from small number of gene expression patterns under the Boolean network model, Proc. of Pac. Symp. on Biocomp., 4:17-28, 1999.
[2] R. Banks. Qualitatively Modelling Genetic Regulatory Networks: Petri Net Techniques and Tools. Ph. D. Dissertation, School of Computing Science, University of Newcastle upon Tyne, 2009.
[3] R. Banks and L. J. Steggles. A High-Level Petri Net Framework for Multi-Valued Genetic Regulatory Networks. Journal of Integrative Bioinformatics, 4(3):60, 2007.
[4] R. Banks, V. Khomenko, and L. J. Steggles. Modelling Genetic Regulatory Networks. In: I. Koch, W. Reisig and R. Schreiber (Eds), Modelling in Systems Biology: the Petri Net Approach, pages 73-100, Computational Biology Series, Springer Verlag, 2010.
[5] R. Banks and L. J. Steggles. An Abstraction Theory for Qualitative Models of Biological Systems. Electronic Proceedings in Theoretical Computer Science, 40:23-38, 2010.
[6] S. Bensalem, Y. Lakhnech, and S. Owre. Computing Abstractions of Infinite State Systems Compositionally and Automatically. In: Proc. of the 10th Int. Conference on Computer Aided Verification, Lecture Notes In Computer Science 1427, pages 319-331, Springer-Verlag, 1998.
[7] C. Chaouiya, E. Remy, and D. Thieffry. Petri Net Modelling of Biological Regulatory Networks. Journal of Discrete Algorithms, 6(2):165-177, 2008.
[8] C. Chaouiya, A. Naldi, E. Remy, and Thieffry. Petri net representation of multi-valued logical regulatory graphs. Natural Computing, 10(2):727-750, 2011.
[9] E. M. Clarke, O. Grumberg, and D. E. Long. Model Checking and Abstractions. ACM Transactions on Programming Languages and Systems, 16(5):1512 – 1542, 1994.
[10] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM, 50(5):752-794, 2003.
[11] J. Comet, H. Klaudel, and S. Liazu. Modeling Multi-valued Genetic Regulatory Networks Using High-Level Petri Nets. Lecture Notes in Computer Science, vol. 3536, pagse 208-227, Springer-Verlag, 2005.
[12] B. Drossel, T. Mihaljev, and F. Greil. Number and length of attractors in a critical Kauffman model with connectivity one. Physical Review Letters, 94(8), 2005.
[13] V. DSilva, D. Kroening, and G. Weissenbacher. A Survey of Automated Techniques for Formal Software Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27(7):1165- 1178 , 2008
[14] A. Esmaeili and C. Jacob. Evolutionary exploration of Boolean networks Proceedings of the IEEE Congress on Evolutionary Computation, pages 3396 – 3403, 2008.
[15] I. Harvey and T. Bossomaier. Time Out of Joint: Attractors in Asynchronous Random Boolean Networks. In: P. Husbands and I. Harvey (eds.), Proc. of ECAL97, pages 67-75, MIT Press 1997.
[16] S. Huang and D. Ingber. Shape-dependent control of cell growth, differentiation, and apoptosis: Switching between attractors in cell regulatory networks. Experimental Cell Research, 261(1):91-103, 2000.
[17] S. A. Kauffman. Metabolic stability and epigenesis in randomly constructed genetic nets. Journal of Theoretical Biology, 22(3):437-467, 1969.
[18] S. A. Kauffman. The origins of order: Self-organization and selection in evolution. Oxford University Press, New York, January 1993.
[19] P. Kungas. Petri Net Reachability Checking Is Polynomial with Optimal Abstraction Hierarchies. Lecture Notes in Computer Science, vol. 3607, pages 149-164, Springer-Verlag, 2005. Copyright: 2005
[20] A. Mishchenko and R. Brayton. Simplification of non-deterministic multi-valued networks. In: ICCAD ’02: Proc. of the 2002 IEEE/ACM Int. Conference on Computer-aided design, pages 557-562, 2002.
[21] A. Naldi, E. Remy, D. Thieffry, and C. Chaouiya. A Reduction of Logical Regulatory Graphs Preserving Essential Dynamical Properties. In: Proc. of CMSB ’09, Lecture Notes in Bioinformatics 5688, pages 266 – 280, Springer-Verlag, 2009.
[22] A. Naldi, E. Remy, D. Thieffry, and C. Chaouiya. Dynamically consistent reduction of logical regulatory graphs. Theoretical Computer Science, 412(21):2207-2218, 2011.
[23] A.B. Oppenheim, O. Kobiler, J. Stavans, D. L. Court, and S. L. Adhya. Switches in bacteriophage λ development. Annual Review of Genetics, 39:4470-4475, 2005.
[24] R. Pel´anek. Reduction and Abstraction Techniques for Model Checking. PhD thesis, Masaryk University Brno, 2006.
[25] R. Rudell and A. Sangiovanni-Vincentelli. Multiple-Valued Minimization for PLA Optimization. IEEE Transactions on Computer-Aided Design, CAD-6, 1987.
[26] A. Saadatpour, I. Albert, and R. Albert. Attractor analysis of asynchronous Boolean models of signal transduction networks. Journal of Theoretical Biology, 266:641-656, 2010.
[27] M. Santill´an and M. C. Mackey. Dynamic regulation of the tryptophan operon: A modeling study and comparison with experimental data PNAS, 98(4): 1364-1369, 2001.
[28] M. Schaub, T. Henzinger, and J. Fisher. Qualitative networks: A symbolic approach to analyze bio-logical signaling networks. BMC Systems Biology, 1:4, 2007.
[29] A. K. Sen and W. Liu. Dynamic analysis of genetic control and regulation of amino acid synthesis: The tryptophan operon in Escherichia coli. Biotechnology and Bioengineering, 35(2):185-194, 1990.
[30] E. Simao, E. Remy, D. Thieffry and C. Chaouiya. Qualitative modelling of regulated metabolic pathways: application to the tryptophan biosynthesis in E. Coli. Bioinformatics, 21: ii190-196, 2005.
[31] I. Suzuki and T. Murata. A method for stepwise refinement and abstraction of petri nets. Journal of Computer and System Sciences, 27:51-76, 1983.
[32] D. Thieffry and R. Thomas. Dynamical behaviour of biological regulatory networks – II. Immunity control in bacteriophage lambda. Bulletin of Mathematical Biology, 57:277-295, 1995.
[33] R. Thomas. Boolean formalization of genetic control circuits. Journal of Theoretical Biology, 42:563-585, 1990.
[34] R. Thomas and R. D’Ari. Biological Feedback, CRC Press, 1990.
[35] R. Thomas, D. Thieffry and M. Kaufman. Dynamical Behaviour of Biological Regulatory Networks – I. Biological Role of Feedback Loops and Practical use of the Concept of Loop-Characteristic State. Bulletin of Mathematical Biology, 57:247-276, 1995.
[36] L. Tournier and M. Chaves. Uncovering operational interactions in genetic networks using asynchronous Boolean dynamics. Journal of Theoretical Biology, 260:196-209, 2009.
[37] A. Veliz-Cuba. Reduction of Boolean Networks. http://arxiv.org/abs/0907.0285, submitted 2009. (Visited Dec 2010)
[38] H. Wimmel and K. Wolf, Karsten. Applying CEGAR to the petri net state equation. In: Proc. of TACAS’11/ETAPS’11, Lecture Notes in Computer Science, vol. 6605, pages 224-238, Springer-Verlag, 2011.
[39] A. Wuensch. Basins of Attraction in Network Dynamics: A Conceptual Framework for Biomolecular Networks, In: G.Schlosser and G.P.Wagner (Eds), Modularity in Development and Evolution, pages 288-311, Chicago University Press, 2002.
Bibtex
@article{sacscuza:steggles2011aamn,
title={Abstracting Asynchronous Multi-Valued Networks},
author={J. Steggles},
journal={Scientific Annals of Computer Science},
volume={21},
number={2},
organization={``A.I. Cuza'' University, Iasi, Romania},
year={2011},
pages={249--282},
publisher={``A.I. Cuza'' University Press}
}