Skip to main content
SpringerLink
Log in

Discretization of Continuous Dynamical Systems Using UPPAAL

  • Chapter
  • First Online:
ModelEd, TestEd, TrustEd

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10500))

Abstract

We want to enable the analysis of continuous dynamical systems (where the evolution of a vector of continuous state variables is described by differential equations) by model checking. We do this by showing how such a dynamical system can be translated into a discrete model of communicating timed automata that can be analyzed by the UPPAAL tool. The basis of the translation is the well-known Euler approach for solving differential equations where we use fixed discrete value steps instead of fixed time steps. Each state variable is represented by a timed automaton in which the delay for taking the next value is calculated on the fly using the differential equations. The state variable automata proceed independently but may notify each other when a value step has been completed; this leads to a recalculation of delays. The approach has been implemented in the tool ANIMO for analyzing biological kinase networks in cells. This tool has been used in actual biological research on osteoarthritis dealing with systems where the dimension of the state vector (the number of nodes in the network) is in the order of one hundred.

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

Notes

  1. 1.

    Models generated by ANIMO are saved in the system’s temporary directory. Further details are available in the ANIMO manual at http://fmt.cs.utwente.nl/tools/animo/content/Manual.pdf.

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126, 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. In: Proceedings of the IEEE, pp. 971–984 (2000)

    Google Scholar 

  3. Bos, W.: Interactive signaling network analysis tool. Master’s thesis, University of Twente (2009)

    Google Scholar 

  4. Bouyer, P., Markey, N., Perrin, N., Schlehuber-Caissier, P.: Timed-automata abstraction of switched dynamical systems using control funnels. In: Sankaranarayanan, S., Vicario, E. (eds.) FORMATS 2015. LNCS, vol. 9268, pp. 60–75. Springer, Cham (2015). doi:10.1007/978-3-319-22975-1_5

    Chapter  Google Scholar 

  5. Brim, L., Češka, M., Šafránek, D.: Model checking of biological systems. In: Bernardo, M., de Vink, E., Di Pierro, A., Wiklicky, H. (eds.) SFM 2013. LNCS, vol. 7938, pp. 63–112. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38874-3_3

    Chapter  Google Scholar 

  6. Brim, L., Fabriková, J., Drazan, S., Safránek, D.: Reachability in biochemical dynamical systems by quantitative discrete approximation. CoRR, abs/1107.5924 (2011)

    Google Scholar 

  7. Butcher, J.: Numerical Methods for Ordinary Differential Equations, 2nd edn. Wiley, Chichester (2008)

    Book  MATH  Google Scholar 

  8. Cardelli, L., Tribastone, M., Tschaikowski, M., Vandin, A.: ERODE: a tool for the evaluation and reduction of ordinary differential equations. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 310–328. Springer, Heidelberg (2017). doi:10.1007/978-3-662-54580-5_19

    Chapter  Google Scholar 

  9. Carter, R., Navarro-López, E.M.: Dynamically-driven timed automaton abstractions for proving liveness of continuous systems. In: Jurdziński, M., Ničković, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 59–74. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33365-1_6

    Chapter  Google Scholar 

  10. Clarke, E.M.: Model checking. In: Ramesh, S., Sivakumar, G. (eds.) FSTTCS 1997. LNCS, vol. 1346, pp. 54–56. Springer, Heidelberg (1997). doi:10.1007/BFb0058022

    Chapter  Google Scholar 

  11. Cytoscape 3 ANIMO app. http://apps.cytoscape.org/apps/animo

  12. David, A., Grunnet, J.D., Jessen, J.J., Larsen, K.G., Rasmussen, J.I.: Application of model-checking technology to controller synthesis. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 336–351. Springer, Heidelberg (2011). doi:10.1007/978-3-642-25271-6_18

    Chapter  Google Scholar 

  13. David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for biological systems. Int. J. Softw. Tools Technol. Transfer 17(3), 351–367 (2015)

    Article  Google Scholar 

  14. Donzé, A., Krogh, B., Rajhans, A.: Parameter synthesis for hybrid systems with an application to simulink models. In: Majumdar, R., Tabuada, P. (eds.) HSCC 2009. LNCS, vol. 5469, pp. 165–179. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00602-9_12

    Chapter  Google Scholar 

  15. Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 169–181. Springer, Heidelberg (1980). doi:10.1007/3-540-10003-2_69

    Chapter  Google Scholar 

  16. Fehnker, A.: Scheduling a steel plant with timed automata. In: Proceedings of the Sixth International Conference on Real-Time Computing Systems and Applications, RTCSA 1999, p. 280. IEEE Computer Society, Washington, DC (1999)

    Google Scholar 

  17. Goethem, S.V., Jacquet, J.-M., Brim, L., Šafránek, D.: Timed modelling of gene networks with arbitrarily precise expression discretization. Electron. Notes Theoret. Comput. Sci. 293, 67–81 (2013). Proceedings of the Third International Workshop on Interactions Between Computer Science and Biology (CS2Bio 2012)

    Article  Google Scholar 

  18. Habets, L.C.G.J.M., van Schuppen, J.H.: Control of piecewise-linear hybrid systems on simplices and rectangles. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 261–274. Springer, Heidelberg (2001). doi:10.1007/3-540-45351-2_23

    Chapter  Google Scholar 

  19. Habets, L.C.G.J.M., van Schuppen, J.H.: Control to facet problems for affine systems on simplices and polytopes - with applications to control of hybrid systems. In: Proceedings of the 44th IEEE Conference on Decision and Control, pp. 4175–4180, December 2005

    Google Scholar 

  20. Jongerden, M., Haverkort, B., Bohnenkamp, H., Katoen, J.: Maximizing system lifetime by battery scheduling. In: 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2009, Los Alamitos. IEEE Computer Society Press, June 2009

    Google Scholar 

  21. Killcoyne, S., Carter, G.W., Smith, J., Boyle, J.: Cytoscape: a community-based framework for network modeling. Methods Mol. Biol. (Clifton, N.J.) 563, 219–239 (2009)

    Article  Google Scholar 

  22. Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. (STTT) 1, 134–152 (1997)

    Article  MATH  Google Scholar 

  23. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). doi:10.1007/10722167_15

    Chapter  Google Scholar 

  24. Maler, O., Batt, G.: Approximating continuous systems by timed automata. In: Fisher, J. (ed.) FMSB 2008. LNCS, vol. 5054, pp. 77–89. Springer, Heidelberg (2008). doi:10.1007/978-3-540-68413-8_6

    Chapter  Google Scholar 

  25. Monteiro, P.T., Ropers, D., Mateescu, R., Freitas, A.T., de Jong, H.: Temporal logic patterns for querying dynamic models of cellular interaction networks. Bioinformatics 24(16), i227–i233 (2008)

    Article  Google Scholar 

  26. PPlane. http://math.rice.edu/~dfield/dfpp.html

  27. Schivo, S., Scholma, J., Karperien, H.B.J., Post, J.N., van de Pol, J.C., Langerak, R.: Setting parameters for biological models with ANIMO. In: André, E., Frehse, G. (eds.) Proceedings 1st International Workshop on Synthesis of Continuous Parameters, Grenoble, France. Electronic Proceedings in Theoretical Computer Science, vol. 145, pp. 35–47. Open Publishing Association, April 2014

    Google Scholar 

  28. Schivo, S., Scholma, J., van der Vet, P.E., Karperien, M., Post, J.N., van de Pol, J., Langerak, R.: Modelling with ANIMO: between fuzzy logic and differential equations. BMC Syst. Biol. 10(1), 56 (2016)

    Article  Google Scholar 

  29. Schivo, S., Scholma, J., Wanders, B., Urquidi Camacho, R., van der Vet, P., Karperien, M., Langerak, R., van de Pol, J., Post, J.: Modelling biological pathway dynamics with Timed Automata. IEEE J. Biomed. Health Inform. 18(3), 832–839 (2013)

    Article  Google Scholar 

  30. Schivo, S., Scholma, J., Wanders, B., Urquidi Camacho, R.A., van der Vet, P.E., Karperien, H.B.J., Langerak, R., van de Pol, J.C., Post, J.N.: Modelling biological pathway dynamics with timed automata. In: 12th IC on Bioinformatics and Bioengineering (BIBE 2012), pp. 447–453. IEEE Computer Society (2012)

    Google Scholar 

  31. Scholma, J., Kerkhofs, J., Schivo, S., Langerak, R., van der Vet, P.E., Karperien, H.B.J., van de Pol, J.C., Geris, L., Post, J.N.: Mathematical modeling of signalingpathways in osteoarthritis. In: Lohmander, S. (ed.) 2013 Osteoarthritis Research Society International (OARSI) World Congress, Philadelphia, USA, vol. 21, Supplement, p. S123. Elsevier, Amsterdam, April 2013

    Google Scholar 

  32. Scholma, J., Schivo, S., Kerkhofs, J., Langerak, R., Karperien, H.B.J., van de Pol, J.C., Geris, L., Post, J.N.: ECHO: the executable chondrocyte. In: Tissue Engineering & Regenerative Medicine International Society, European Chapter Meeting, Genova, Italy, vol. 8, p. 54. Wiley, Malden, June 2014

    Google Scholar 

  33. Scholma, J., Schivo, S., Urquidi Camacho, R., van de Pol, J., Karperien, M., Post, J.: Biological networks 101: computational modeling for molecular biologists. Gene 533(1), 379–384 (2014)

    Article  Google Scholar 

  34. Siebert, H., Bockmayr, A.: Temporal constraints in the logical analysis of regulatory networks. Theoret. Comput. Sci. 391(3), 258–275 (2008). Converging Sciences: Informatics and Biology

    Article  MathSciNet  MATH  Google Scholar 

  35. Sloth, C., Wisniewski, R.: Verification of continuous dynamical systems by timed automata. Formal Methods Syst. Des. 39(1), 47–82 (2011)

    Article  MATH  Google Scholar 

  36. Sloth, C., Wisniewski, R.: Complete abstractions of dynamical systems by timed automata. Nonlinear Anal.: Hybrid Syst. 7(1), 80–100 (2013). (IFAC) World Congress 2011

    MathSciNet  MATH  Google Scholar 

  37. Stursberg, O., Kowalewski, S., Engell, S.: On the generation of timed discrete approximations for continuous systems. Math. Comput. Modell. Dyn. Syst. 6(1), 51–70 (2000)

    Article  MATH  Google Scholar 

  38. UPPAAL. www.uppaal.org

  39. Urquidi Camacho, R.: Modeling osteoarthritic cartilage with ANIMO: an executable biology approach to osteoarthritic signaling and gene expression. Master’s thesis, University of Twente, The Netherlands, July 2013

    Google Scholar 

  40. Wisniewski, R., Sloth, C.: Abstraction of dynamical systems by timed automata. Model. Ident. Control 32(2), 79 (2011)

    Article  MATH  Google Scholar 

  41. Xing, J., Theelen, B.D., Langerak, R., van de Pol, J., Tretmans, J., Voeten, J.P.M.: UPPAAL in practice: quantitative verification of a RapidIO network. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6416, pp. 160–174. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16561-0_20

    Chapter  Google Scholar 

Download references

Acknowledgements

We thank Arend Rensink for an important comment on an earlier version of this work. We thank Wim Bos, Liesbeth Geris, Marcel Karperien, Johan Kerkhofs, Jaco van de Pol, Janine Post, Jetse Scholma, Ricardo Urquidi Camacho, Paul van der Vet, and Brend Wanders for the fruitful and pleasant collaboration leading to ANIMO.

Author information

Authors and Affiliations

  1. Formal Methods and Tools Group, Faculty of EEMCS, University of Twente, Enschede, The Netherlands

    Stefano Schivo & Rom Langerak

Authors
  1. Stefano Schivo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rom Langerak
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Rom Langerak .

Editor information

Editors and Affiliations

  1. RWTH Aachen University, Aachen, Germany

    Joost-Pieter Katoen

  2. University of Twente, Enschede, The Netherlands

    Rom Langerak

  3. University of Twente, Enschede, The Netherlands

    Arend Rensink

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Schivo, S., Langerak, R. (2017). Discretization of Continuous Dynamical Systems Using UPPAAL. In: Katoen, JP., Langerak, R., Rensink, A. (eds) ModelEd, TestEd, TrustEd. Lecture Notes in Computer Science(), vol 10500. Springer, Cham. https://doi.org/10.1007/978-3-319-68270-9_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68270-9_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-68269-3

  • Online ISBN: 978-3-319-68270-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation