Skip to main content
SpringerLink
Log in

Compositional Analysis of Boolean Networks Using Local Fixed-Point Iterations

  • Conference paper
  • First Online:
Reachability Problems (RP 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9899))

Included in the following conference series:

  • 356 Accesses

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  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)

    Article  Google Scholar 

  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). http://doi.acm.org/10.1145/309847.309942

  3. Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 100(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  4. Cheng, D., Qi, H.: A linear representation of dynamics of Boolean networks. IEEE Trans. Autom. Control 55(10), 2251–2258 (2010)

    Article  MathSciNet  Google Scholar 

  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. 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. 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. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960). http://doi.acm.org/10.1145/321033.321034

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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. Greenberg, B.S.: NXSYS, Signaling and Interlocking Simulator. http://www.nycsubway.org/wiki/NXSYS,_Signalling_and_Interlocking_Simulator

  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)

    Article  Google Scholar 

  13. Hochma, G., Margaliot, M., Fornasini, E., Valcher, M.E.: Symbolic dynamics of Boolean control networks. Automatica 49(8), 2525–2530 (2013)

    Article  MathSciNet  Google Scholar 

  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. Kauffman, S.A.: The Origins of Order: Self Organization and Selection in Evolution. Oxford University Press, New York (1993). http://opac.inria.fr/record=b1077782

    Google Scholar 

  16. Kuncak, V., Rustan, K. Leino, M.: On computing the fixpoint of a set of Boolean equations (2004). http://arXiv.org/abs/cs.PL/0408045

  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)

    Chapter  Google Scholar 

  18. Wuensche, A., et al.: Discrete dynamical networks and their attractor basins. Complex. Int. 6, 3–21 (1998)

    Google Scholar 

  19. Zhao, Y., Kim, J., Filippone, M.: Aggregation algorithm towards large-scale Boolean network analysis. IEEE Trans. Autom. Control 58(8), 1976–1985 (2013)

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgement

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.

Author information

Authors and Affiliations

  1. CMLA, ENS Cachan, CNRS, Université Paris-Saclay, 61 Av. du Président Wilson, 94235, Cachan Cedex, France

    Adrien Le Coënt

  2. LSV, ENS Cachan, CNRS, Université Paris-Saclay, 61 Av. du Président Wilson, 94235, Cachan Cedex, France

    Laurent Fribourg

  3. Thales Research & Technology, 1 Av. Augustin Fresnel, 91767, Palaiseau, France

    Romain Soulat

Authors
  1. Adrien Le Coënt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Laurent Fribourg
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Romain Soulat
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Adrien Le Coënt .

Editor information

Editors and Affiliations

  1. Aalborg University, Aalborg, Denmark

    Kim Guldstrand Larsen

  2. University of Liverpool, Liverpool, United Kingdom

    Igor Potapov

  3. Aalborg University, Aalborg, Denmark

    Jiří Srba

Appendix: Railway Interlocking System

Appendix: Railway Interlocking System

Railway Interlocking is one part of a complete railway system that ensures the safety of all trains and passengers. Given the routes that trains wish to travel along and current train positions (among other information), the Interlocking computes a safe environment for trains (mainly signals indications, and switches positions).

A part of the railway interlocking functioning can be translated to boolean equations. In this example, we have taken the boolean variables and equations associated with protection, movement command and locking of two railway switches while abstracting away all the timed components of those systems. Computing the attractors allows to find what states those switches will reach upon reception of a new command.

The dynamics of the system tested in Sect. 4.1 is given by the rules:

  • 23NLP = !23RLP (OR (AND 23ANN 23ANS) (AND 23BNN 23BNS) 18PBS 23NL)

  • 23RLP = !23NLP (OR (AND 23RN 23RS) 23RL)

  • 23ANS = (OR 16PBS 16XR) !23RS !23RWK

  • 23BNS = (OR 25ANS 25RS) !23RN !23RWK

  • 23ANN = (OR 25BNN 25RN) !23RS !23RWK

  • 23BNN = (OR 32XS 32PBS) !23RN !23RWK

  • 23RS = 25ANS !23ANS !23BNN !23NWK

  • 23RN = 25BNN !23ANS !23BNN !23NWK

  • 23NWZ = (OR (AND 23NWZ !23RWZ) (AND 23NLP 23LS))

  • 23RWZ = (OR (AND 23RWZ !23NWZ) (AND 23RLP 23LS))

  • 23NWC = (AND 23NWZ 23NWP)

  • 23RWC = (AND 23RWZ 23RWP)

  • 23NWK = 23NWC (OR 23NLP !23LS)

  • 23RWK = 23RWC (OR 23RLP !23LS)

  • 25ANS = (OR 22PBS 28ZS 22XS 22XR) !25RS !25RWK

  • 25BNS = (OR 23ANS 23RS) !25RN !25RWK

  • 25ANN = (OR 23BNN 23RN) !25RS !25RWK

  • 25BNN = (OR 34XS 34PBS) !25RN !25RWK

  • 25RN = 23BNN !25ANS !25BNN !25NWK

  • 25RS = 23ANS !25ANS !25BNN !25NWK

  • 25NLP = !25RLP (OR (AND 25ANN 25ANS) (AND 25BNN 25BNS) 28XS 25NL)

  • 25RLP = !25NLP (OR (AND 25RN 25RS) 25RL)

  • 25NWZ = (OR (AND 25NWZ !25RWZ) (AND 25NLP 25LS))

  • 25RWZ = (OR (AND 25RWZ !25NWZ) (AND 25RLP 25LS))

  • 25NWC = (AND 25NWZ 25NWP)

  • 25RWC = (AND 25RWZ 25RWP)

  • 25NWK = 25NWC (OR 25NLP !25LS)

  • 25RWK = 25RWC (OR 25RLP !25LS)

The left-hand sides of these equations correspond to the 28 state variables. The other expressions appearing in the right-hand sides correspond to the 22 parameters.

The system is split into 4 sub-systems as follows:

  • For sub-system 1, the state variables are: 23NLP, 23RLP, 23ANS, 23BNS, 23ANN, 23BNN, 23RS and 23RN.

    The parameters are: 18PBS, 23RL, 16PBS, 16XR, 32XS, 32PBS and 23NL.

  • For sub-system 2, the state variables are: 23NWZ, 23RWZ, 23NWC, 23RWC, 23NWK and 23RWK.

    The parameters are: 23LS, 23NWP and 23RWP.

  • For sub-system 3, the state variables are: 25ANS, 25BNS, 25ANN, 25BNN, 25RN, 25RS and 25NLP.

    The parameters are: 22PBS, 28ZS, 22XS, 22XR, 34XS, 34PBS, 28XS and 25NL.

  • For sub-system 4, the state variables are: 25RLP, 25NWZ, 25RWZ, 25NWC, 25RWC, 25NWK and 25RWK.

    The parameters are: 25RL, 25LS, 25NWP and 25RWP.

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Le Coënt, A., Fribourg, L., Soulat, R. (2016). Compositional Analysis of Boolean Networks Using Local Fixed-Point Iterations. In: Larsen, K., Potapov, I., Srba, J. (eds) Reachability Problems. RP 2016. Lecture Notes in Computer Science(), vol 9899. Springer, Cham. https://doi.org/10.1007/978-3-319-45994-3_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-45994-3_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-45993-6

  • Online ISBN: 978-3-319-45994-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation