Compositional Analysis of Boolean Networks Using Local Fixed-Point Iterations

  • Adrien Le CoëntEmail author
  • Laurent Fribourg
  • Romain Soulat
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9899)


We present a compositional method which allows to over-approximate the set of attractors and under-approximate the set of basins of attraction of a Boolean network (BN). This merely consists in replacing a global fixed-point computation by a composition of local fixed-point computations. Once these approximations have been computed, it becomes much more tractable to generate the exact sets of attractors and basins of attraction. We illustrate the interest of our approach on several examples, among which is a BN modeling a railway interlocking system with 50 nodes and millions of attractors.



We are most grateful to Philippe Schnoebelen for insightful explanations on Abstract Interpretation and numerous comments on an earlier draft of this paper.

This work is supported by Institut Farman (ENS Cachan) and by the French National Research Agency through the “iCODE Institute project” funded by the IDEX Paris-Saclay, ANR-11-IDEX-0003-02.


  1. 1.
    Akutsu, T., Kosub, S., Melkman, A.A., Tamura, T.: Finding a periodic attractor of a Boolean network. IEEE/ACM Trans. Comput. Biol. Bioinform. 9(5), 1410–1421 (2012)CrossRefGoogle Scholar
  2. 2.
    Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: DAC, pp. 317–320 (1999).
  3. 3.
    Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 100(8), 677–691 (1986)CrossRefzbMATHGoogle Scholar
  4. 4.
    Cheng, D., Qi, H.: A linear representation of dynamics of Boolean networks. IEEE Trans. Autom. Control 55(10), 2251–2258 (2010)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Cheng, D., Qi, H., Zhao, Y.: On Boolean control networks - an algebraic approach. In: Proceedings of the 18th IFAC World Congress, Milano, pp. 8366–8377 (2011)Google Scholar
  6. 6.
    Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbrüggen, R. (eds.) Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)Google Scholar
  7. 7.
    Cousot, P.: Compositional separate modular static analysis of programs by abstract interpretation. In: Proceedings of SSGRR - Advances in Infrastructure for Electronic Business, Science, and Education on the Internet, pp. 6–10 (2001)Google Scholar
  8. 8.
    Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960). MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Dubrova, E., Teslenko, M.: A SAT-based algorithm for finding attractors in synchronous Boolean networks. IEEE/ACM Trans. Comput. Biol. Bioinform. (TCBB) 8(5), 1393–1399 (2011)CrossRefGoogle Scholar
  10. 10.
    Fokkink, W., Hollingshead, P., Groote, J., Luttik, S., van Wamel, J.: Verification of interlockings: from control tables to ladder logic diagrams. In: Proceedings of FMICS, vol. 98, pp. 171–185 (1998)Google Scholar
  11. 11.
    Greenberg, B.S.: NXSYS, Signaling and Interlocking Simulator.,_Signalling_and_Interlocking_Simulator
  12. 12.
    Guo, W., Yang, G., Wu, W., He, L., Sun, M.: A parallel attractor finding algorithm based on Boolean satisfiability for genetic regulatory networks. PLoS ONE 9(4), e94258 (2014)CrossRefGoogle Scholar
  13. 13.
    Hochma, G., Margaliot, M., Fornasini, E., Valcher, M.E.: Symbolic dynamics of Boolean control networks. Automatica 49(8), 2525–2530 (2013)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Hong, C., Hwang, J., Cho, K.-H., Shin, I.: An efficient steady-state analysis method for large boolean networks with high maximum node connectivity. PLoS ONE 10(12) (2015).doi: 10.1371/journal.pone.0145734 Google Scholar
  15. 15.
    Kauffman, S.A.: The Origins of Order: Self Organization and Selection in Evolution. Oxford University Press, New York (1993). Google Scholar
  16. 16.
    Kuncak, V., Rustan, K. Leino, M.: On computing the fixpoint of a set of Boolean equations (2004).
  17. 17.
    Naldi, A., Thieffry, D., Chaouiya, C.: Decision diagrams for the representation and analysis of logical models of genetic networks. In: Calder, M., Gilmore, S. (eds.) CMSB 2007. LNCS (LNBI), vol. 4695, pp. 233–247. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  18. 18.
    Wuensche, A., et al.: Discrete dynamical networks and their attractor basins. Complex. Int. 6, 3–21 (1998)Google Scholar
  19. 19.
    Zhao, Y., Kim, J., Filippone, M.: Aggregation algorithm towards large-scale Boolean network analysis. IEEE Trans. Autom. Control 58(8), 1976–1985 (2013)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Adrien Le Coënt
    • 1
    Email author
  • Laurent Fribourg
    • 2
  • Romain Soulat
    • 3
  1. 1.CMLA, ENS Cachan, CNRSUniversité Paris-SaclayCachan CedexFrance
  2. 2.LSV, ENS Cachan, CNRSUniversité Paris-SaclayCachan CedexFrance
  3. 3.Thales Research & TechnologyPalaiseauFrance

Personalised recommendations