Model Checking Approach to the Analysis of Biological Systems

  • Nikola Beneš
  • Luboš Brim
  • Samuel Pastva
  • David ŠafránekEmail author
Part of the Computational Biology book series (COBO, volume 30)


Formal verification techniques together with other computer science formal methods have been recently tailored for applications to biological and biomedical systems. In contrast to traditional simulation-based approaches, model checking opens an entirely novel way of viewing and analysing the dynamics of such systems. In particular, it can help in system identification and parameter synthesis, in comparison of models with respect to a priori given desired properties, in robustness analysis of systems, in relating models to experimental data, or in globally analysing the bifurcations of systems behaviour with respect to changes in parameters. In this review, we briefly describe the state-of-the-art methods and techniques employing model checking, as one of the most prominent verification techniques, to the analysis of biomedical systems. We demonstrate some of the advantages of using the model checking method by presenting a brief account of the technique itself followed by examples of the application of formal methods based on model checking to three areas related to the analysis of biomedical systems: verification of biological hypotheses, parameters synthesis, and bifurcation analysis. Finally, we discuss several case studies that show how fruitfully the methods can be utilised within the computational systems biology and biomedicine domain.



This work has been partially supported by the Czech Science Foundation grant No. 18-00178S.


  1. 1.
    Andreychenko A, Mikeev L, Wolf V (2015) Model reconstruction for moment-based stochastic chemical kinetics. ACM Trans Model Comput Simul 25(2):12:1–12:19MathSciNetCrossRefGoogle Scholar
  2. 2.
    Areces C, ten Cate B (2007) Hybrid logics. In: Blackburn P, van Benthem J, Wolter F (eds) Handbook of modal logic, vol 3, 1st edn. ElsevierGoogle Scholar
  3. 3.
    Arellano G, Argil J, Azpeitia E, Benítez M, Carrillo M, Góngora P, Rosenblueth D, Alvarez-Buylla E (2011) “Antelope” a hybrid-logic model checker for branching-time boolean grn analysis. BMC Bioinform 12(1):490CrossRefGoogle Scholar
  4. 4.
    Backenköhler M, Bortolussi L, Wolf V (2018) Moment-based parameter estimation for stochastic reaction networks in equilibrium. IEEE/ACM Trans Comput Biol Bioinform 15(4):1180–1192CrossRefGoogle Scholar
  5. 5.
    Baier C, Katoen JP (2008) Principles of model checking. The MIT PressGoogle Scholar
  6. 6.
    Barnat J, Brim L, Krejčí A, Štreck A, Šafránek D, Vejnár M, Vejpustek T (2012) On parameter synthesis by parallel model checking. IEEE/ACM Trans Comput Biol Bioinform 9(3):693–705CrossRefGoogle Scholar
  7. 7.
    Barnat J, Brim L, Černá I, Dražan S, Fabriková J, Láník J, Šafránek D, Ma H (2009) BioDiVinE: A framework for parallel analysis of biological models. In: Computational models for cell processes (COMPMOD). EPTCS, vol 6, pp 31–45Google Scholar
  8. 8.
    Barnat J, Brim L, Šafránek D (2010) High-performance analysis of biological systems dynamics with the DiVinE model checker. Brief Bioinform 11(3):301–312CrossRefGoogle Scholar
  9. 9.
    Bartocci E, Corradini F, Merelli E, Tesei L (2010) Detecting synchronisation of biological oscillators by model checking. Theor Comput Sci 411(20):1999–2018MathSciNetCrossRefGoogle Scholar
  10. 10.
    Bartocci E, Liò P (2016) Computational modeling, formal analysis, and tools for systems biology. PLOS Comput Biol 12(1):1–22CrossRefGoogle Scholar
  11. 11.
    Batt G, Belta C, Weiss R (2007) Model checking liveness properties of genetic regulatory networks. In: TACAS. LNCS, vol 4424. Springer, pp 323–338Google Scholar
  12. 12.
    Batt G, Page M, Cantone I, Gössler G, Monteiro P, de Jong H (2010) Efficient parameter search for qualitative models of regulatory networks using symbolic model checking. Bioinformatics 26(18):603–610CrossRefGoogle Scholar
  13. 13.
    Batt G, Ropers D, Jong HD, Geiselmann J, Mateescu R, Schneider D (2005) Validation of qualitative models of genetic regulatory networks by model checking: analysis of the nutritional stress response in escherichia coli. Bioinformatics 21:19–28CrossRefGoogle Scholar
  14. 14.
    Batt G, Salah RB, Maler O (2007) On timed models of gene networks. In: Formal modeling and analysis of timed systems (FORMATS). LNCS, Springer, Berlin, pp 38–52Google Scholar
  15. 15.
    Batt G, Yordanov B, Weiss R, Belta C (2007) Robustness analysis and tuning of synthetic gene networks. Bioinformatics 23(18):2415–2422CrossRefGoogle Scholar
  16. 16.
    ter Beek MH, Fantechi A, Gnesi S, Mazzanti F (2011) A state/event-based model-checking approach for the analysis of abstract system properties. Sci Comput Prog 76:119–135CrossRefGoogle Scholar
  17. 17.
    Behrmann G, David A, Larsen KG (2004) A tutorial on uppaal. In: 4th international school on formal methods for the design of computer, communication, and software systems in formal methods for the design of real-time systems (SFM-RT), No. 3185. LNCS, Springer, Berlin, pp 200–236Google Scholar
  18. 18.
    Belta C, Habets LCGJM (2006) Controlling a class of nonlinear systems on rectangles. IEEE Trans Automat Contr 51(11):1749–1759MathSciNetCrossRefGoogle Scholar
  19. 19.
    Beneš N, Brim L, Demko M, Pastva S, Šafránek D (2016) Parallel SMT-based parameter synthesis with application to piecewise multi-affine systems. ATVA. LNCS 9938:192–208Google Scholar
  20. 20.
    Beneš N, Brim L, Demko M, Pastva S, Šafránek D (2016) A model checking approach to discrete bifurcation analysis. In: Fitzgerald J, Heitmeyer C, Gnesi S, Philippou A (eds.) FM 2016, vol 9995. LNCS, Springer, pp 85–101Google Scholar
  21. 21.
    Bernot G, Comet JP, Richard A, Guespin J (2004) Application of formal methods to biological regulatory networks: extending thomas’ asynchronous logical approach with temporal logic. J Theor Biol 229(3):339–347MathSciNetCrossRefGoogle Scholar
  22. 22.
    Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: Cleaveland WR (ed) Tools and algorithms for the construction and analysis of systems, vol 6806. LNCS, Springer, Berlin, pp 193–207CrossRefGoogle Scholar
  23. 23.
    Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R (2015) Abstraction-based parameter synthesis for multiaffine systems. In: Hardware and software: verification and testing, lecture notes in computer science, vol 9434, Springer International Publishing, pp 19–35Google Scholar
  24. 24.
    Bonzanni N, Feenstra KA, Fokkink W, Krepska E (2009) What can formal methods bring to systems biology? In: FM 2009: formal methods, second world congress, eindhoven, The Netherlands, November 2-6, 2009. Proceedings, Lecture notes in computer science, vol 5850, Springer, Berlin, pp 16–22CrossRefGoogle Scholar
  25. 25.
    Bortolussi L, Cardelli L, Kwiatkowska M, Laurenti L (2016) Approximation of probabilistic reachability for chemical reaction networks using the linear noise approximation. In: Quantitative evaluation of system (QEST 2016), vol 9826, Springer, Berlin, pp 72–88CrossRefGoogle Scholar
  26. 26.
    Bortolussi L, Milios D, Sanguinetti G (2015) U-check: model checking and parameter synthesis under uncertainty. In: Campos J, Haverkort BR (eds) Quantitative evaluation of systems. Springer International Publishing, Cham, pp 89–104CrossRefGoogle Scholar
  27. 27.
    Bortolussi L, Milios D, Sanguinetti G (2016) Smoothed model checking for uncertain continuous-time markov chains. Inf Comput 247:235–253MathSciNetCrossRefGoogle Scholar
  28. 28.
    Brim L, Češka M, Šafránek D (2013) Model checking of biological system. In: 13th International school on formal methods for the design of computer, communication and software systems: dynamical systemsGoogle Scholar
  29. 29.
    Brim L, Barnat J (2007) Tutorial: Parallel model checking. In: Bosnacki D, Edelkamp S (eds) Model checking software, 14th International SPIN workshop, Berlin, Germany, July 1-3, 2007, Proceedings, Lecture notes in computer science, vol 4595, Springer, Berlin, pp 187–203Google Scholar
  30. 30.
    Brim L, Demko M, Pastva S, Šafránek D (2015) High-performance discrete bifurcation analysis for piecewise-affine dynamical systems. In: Hybrid systems biology, Springer, Berlin, pp 58–74CrossRefGoogle Scholar
  31. 31.
    Brim L, Dluhoš P, Šafránek D, Vejpu stek T (2014) STL*: extending signal temporal logic with signal-value freezing operator. Information and computation 236, 52–67, special Issue on Hybrid Systems and BiologyMathSciNetCrossRefGoogle Scholar
  32. 32.
    Brim L, Češka M, Demko M, Pastva S, Šafránek D (2015) Parameter synthesis by parallel coloured CTL model checking. In: Roux O, Bourdon J (eds) Computational methods in systems biology, Lecture notes in computer science, vol 9308, pp 251–263. Springer International Publishing (2015)Google Scholar
  33. 33.
    Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: \(10^{20}\) states and beyond. Inf Comput 98(2):142–170Google Scholar
  34. 34.
    Calzone L, Chabrier-Rivier N, Fages F, Soliman S (2006) Machine learning biochemical networks from temporal logic properties. In: Transactions on computational systems biology VI, LNCS, Springer, Berlin, Heidelberg, pp 68–94CrossRefGoogle Scholar
  35. 35.
    Champneys A, Tsaneva-Atanasova K (2013) Dynamical systems theory, bifurcation analysis. In: Encyclopedia of systems biology, Springer, Berlin, pp 632–637CrossRefGoogle Scholar
  36. 36.
    Chaouiya C, Remy E, Mossé B, Thieffry D (2003) Qualitative analysis of regulatory graphs: a computational tool based on a discrete formal framework. In: Positive systems, vol 294, LNCIS, Springer, pp 830–832Google Scholar
  37. 37.
    Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV 2: an OpenSource tool for symbolic model checking. Computer aided verification (CAV), vol 2404, LNCS, Springer, Berlin, Heidelberg, pp 359–364CrossRefGoogle Scholar
  38. 38.
    Clarke EM, Enders R, Filkorn T, Jha S (1996) Exploiting symmetry in temporal logic model checking. Form Methods Syst Des 9(1–2):77–104CrossRefGoogle Scholar
  39. 39.
    Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, CambridgeGoogle Scholar
  40. 40.
    Clarke E, Zuliani P (2011) Statistical model checking for cyber-physical systems. Automated technology for verification and analysis (ATVA), vol 6996. LNCS, Springer, Berlin Heidelberg, pp 1–12zbMATHGoogle Scholar
  41. 41.
    Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2001) Progress on the state explosion problem in model checking. In: Informatics - 10 Years back. 10 Years ahead, vol 2000, LNCS, Springer, Berlin, pp 176–194Google Scholar
  42. 42.
    Collins P, Habets LC, van Schuppen JH, Černá I, Fabriková J, Šafránek D (2011) Abstraction of biochemical reaction systems on polytopes. In: Proceedings of the 18th IFAC world congress, vol 18, pp 14869–14875CrossRefGoogle Scholar
  43. 43.
    Dang T, Donze A, Maler O, Shalev N (2008) Sensitive state-space exploration. In: IEEE conference on decision and control, pp 4049–4054Google Scholar
  44. 44.
    Didier F, Henzinger TA, Mateescu M, Wolf V (2010) Sabre: a tool for stochastic analysis of biochemical reaction networks. CoRR arXiv:abs/1005.2819
  45. 45.
    Dluhoš P, Brim L, Šafránek D (2012) On expressing and monitoring oscillatory dynamics. In: Hybrid systems and biology (HSB), vol 92, EPTCS, pp 73–87Google Scholar
  46. 46.
    Donaldson R, Gilbert D (2008) A model checking approach to the parameter estimation of biochemical pathways. In: CMSB, vol 5307, LNCS, Springer, Berlin, pp 269–287CrossRefGoogle Scholar
  47. 47.
    Donzé A (2010) Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Computer aided verification (CAV). LNCS, Springer, Berlin, Heidelberg, pp 167–170CrossRefGoogle Scholar
  48. 48.
    Donzé A (2010) Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: CAV. vol 10, Springer, pp 167–170Google Scholar
  49. 49.
    Donzé A, Clermont G, Langmead CJ (2010) Parameter synthesis in nonlinear dynamical systems: application to systems biology. J Comput Biol 17(3):325–336MathSciNetCrossRefGoogle Scholar
  50. 50.
    Eker S, Knapp M, Laderoute K, Lincoln P, Meseguer J, Sonmez K (2002) Pathway logic: symbolic analysis of biological signaling. In: Pacific symposium on biocomputing, pp 400–412Google Scholar
  51. 51.
    Emerson EA, Sistla AP (1996) Symmetry and model checking. Form Methods Syst Des 9(1–2):105–131CrossRefGoogle Scholar
  52. 52.
    Fages F, Soliman S (2008) Formal cell biology in Biocham. In: 8th International school on formal methods for the design of computer, communication and software systems: computational systems biology SFM08, vol 5016, pp 54–80Google Scholar
  53. 53.
    Fages F, Rizk A (2008) On temporal logic constraint solving for analyzing numerical data time series. Theor Comput Sci 408(1):55–65MathSciNetCrossRefGoogle Scholar
  54. 54.
    Fisher J, Henzinger TA (2007) Executable cell biology. Nat Biotechnol 25(11):1239–1249CrossRefGoogle Scholar
  55. 55.
    Fröhlich F, Theis F, Hasenauer J (2014) Uncertainty analysis for non-identifiable dynamical systems: profile likelihoods, bootstrapping and more. In: CMBS, vol 8859, LNCS, Springer, Berlin, pp 61–72CrossRefGoogle Scholar
  56. 56.
    Gábor, A., Banga, J.R.: Improved parameter estimation in kinetic models: selection and tuning of regularization methods. In: CMSB, vol 8859, LNCS, Springer, Berlin, pp 45–60CrossRefGoogle Scholar
  57. 57.
    Gao S, Kong S, Clarke EM (2013) dReal: An SMT solver for nonlinear theories over the reals. In: CADE-24. , vol. 7898, LNCS, Springer, Berlin, pp 208–214CrossRefGoogle Scholar
  58. 58.
    Geldenhuys J, de Villiers PJA (1999) Runtime efficient state compaction in SPIN. In: Model checking software (SPIN), vol 1680. LNCS, Springer, Berlin, pp 12–21CrossRefGoogle Scholar
  59. 59.
    Gilbert D, Breitling R, Heiner M, Donaldson R (2009) An introduction to biomodel engineering, illustrated for signal transduction pathways. Membrane computing, vol 5391, LNCS, Springer, Berlin, pp 13–28CrossRefGoogle Scholar
  60. 60.
    Goethem SV, Jacquet JM, Brim L, Šafránek D (2013) Timed modelling of gene networks with arbitrary expression level discretization. In: Interactions between computer science and biology. ENTCS, ElsevierGoogle Scholar
  61. 61.
    Grosu R, Batt G, Fenton FH, Glimm J, Guernic CL, Smolka SA, Bartocci E (2011) From cardiac cells to genetic regulatory networks. CAV LNCS 6806:396–411MathSciNetGoogle Scholar
  62. 62.
    Hajnal M, Šafránek D, Demko M, Pastva S, Krejčí P, Brim L (2016) Toward modelling and analysis of transient and sustained behaviour of signalling pathways. In: Hybrid systems biology - 5th international workshop, HSB 2016, Grenoble, France, October 20-21, 2016, Proceedings. Springer, Berlin, pp 57–66CrossRefGoogle Scholar
  63. 63.
    Heath J, Kwiatkowska M, Norman G, Parker D, Tymchyshyn O (2008) Probabilistic model checking of complex biological pathways. Theor Comput Sci 319(3):239–257MathSciNetCrossRefGoogle Scholar
  64. 64.
    Heiner M, Gilbert D, Donaldson R (2008) Petri nets for systems and synthetic biology. In: Formal methods for the design of computer, communication, and software systems 8th international conference on formal methods for computational systems biology (SFM), vol 5016, LNCS, Springer, Berlin, pp 215–264Google Scholar
  65. 65.
    Holzmann GJ (2003) The Spin model checker: primer and reference manual. Addison-WesleyGoogle Scholar
  66. 66.
    Jha SK, Clarke EM, Langmead CJ, Legay A, Platzer A, Zuliani P (2009) A bayesian approach to model checking biological systems. In: Computational methods in systems biology. Springer, Berlin, pp 218–234CrossRefGoogle Scholar
  67. 67.
    Klarner H, Streck A, Šafránek D, Kolčák J, Siebert H (2012) Parameter identification and model ranking of thomas networks. In: Computational methods in systems biology (CMSB), LNCS, Springer, Berlin, pp 207–226CrossRefGoogle Scholar
  68. 68.
    Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Computer aided verification (CAV), vol 6806, LNCS, Springer, Berlin, pp 585–591CrossRefGoogle Scholar
  69. 69.
    Legay, A., Delahaye, B., Bensalem, S (2010) Statistical model checking: an overview. In: Runtime verification, Springer, Berlin, Heidelberg, pp 122–135CrossRefGoogle Scholar
  70. 70.
    Li Y, Albarghouthi A, Kincaid Z, Gurfinkel A, Chechik M (2014) Symbolic optimization with SMT solvers. In: POPL ’14. ACM, pp 607–618Google Scholar
  71. 71.
    Liu B, Kong S, Gao S, Zuliani P, Clarke EM (2014) Parameter synthesis for cardiac cell hybrid models using \(\delta \)-decisions. In: CMSB, vol 8859, LNCS, Springer, Berlin, pp 99–113Google Scholar
  72. 72.
    Madsen C, Shmarov F, Zuliani P (2015) BioPSy: An SMT-based tool for guaranteed parameter set synthesis of biological models. In: CMSB’15, vol 9308, LNCS, Springer, Berlin, pp 182–194CrossRefGoogle Scholar
  73. 73.
    Maler O, Batt G (2008) Approximating continuous systems by timed automata. In: Formal methods in systems biology (FMSB), LNCS, Springer, Berlin, pp 77–89Google Scholar
  74. 74.
    Maler O, Nickovic D, Pnueli A (2008) Checking temporal properties of discrete, timed and continuous behaviors. In: Pillars of computer science, Springer, Berlin, Heidelberg, pp 475–505Google Scholar
  75. 75.
    Mateescu R, Monteiro PT, Dumas E, de Jong H (2011) CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks. Theor Comput Sci 412(26):2854–2883MathSciNetCrossRefGoogle Scholar
  76. 76.
    Meijer H, Dercole F, Oldeman B (2011) Numerical bifurcation analysis. In: Mathematics of complexity and dynamical systems, Springer, Berlin, pp 1172–1194CrossRefGoogle Scholar
  77. 77.
    Mittnacht S (1998) Control of pRB phosphorylation. Curr Opin Genet Dev 8(1):21–27CrossRefGoogle Scholar
  78. 78.
    Monteiro PT, Ropers D, Mateescu R, Freitas AT, de Jong H (2008) Temporal logic patterns for querying qualitative models of genetic regulatory networks. In: ECAI, vol 178, FAIA, IOS Press, pp 229–233Google Scholar
  79. 79.
    Nenzi L, Silvetti S, Bartocci E, Bortolussi L (2018) A robust genetic algorithm for learning temporal specifications from data. In: Quantitative evaluation of systems, Springer International Publishing, Cham, pp. 323–338CrossRefGoogle Scholar
  80. 80.
    Niu W, Wang D (2008) Algebraic analysis of bifurcation and limit cycles for biological systems. In: Algebraic biology, AB ’08, Springer, Berlin, pp 156–171Google Scholar
  81. 81.
    Pelánek R (2009) Fighting state space explosion: review and evaluation. In: Formal methods for industrial critical systems (FMICS), vol 5596, LNCS, Springer, Berlin, pp 37–52CrossRefGoogle Scholar
  82. 82.
    Peled D (1988) Ten years of partial order reduction. In: Computer aided verification (CAV), LNCS, Springer, Berlin, pp 17–28CrossRefGoogle Scholar
  83. 83.
    Priami C (2009) Algorithmic systems biology. Commun ACM 52(5):80–88CrossRefGoogle Scholar
  84. 84.
    Raman V, Donzé A, Sadigh D, Murray RM, Seshia SA (2015) Reactive synthesis from signal temporal logic specifications. In: HSCC’15, ACM, New York, NY, USA, pp 239–248Google Scholar
  85. 85.
    Raue A, Karlsson J, Saccomani MP, Jirstrand M, Timmer J (2014) Comparison of approaches for parameter identifiability analysis of biological systems. BioinformaticsGoogle Scholar
  86. 86.
    Rizk A, Batt G, Fages F, Soliman S (2009) A general computational method for robustness analysis with applications to synthetic gene networks. Bioinformatics 25(12)CrossRefGoogle Scholar
  87. 87.
    Sasagawa S, Ozaki Yi, Fujita K, Kuroda S (2005) Prediction and validation of the distinct dynamics of transient and sustained ERK activation. Nat Cell Biol 7(4):365–373CrossRefGoogle Scholar
  88. 88.
    Schaub M, Henzinger T, Fisher J (2007) Qualitative networks: a symbolic approach to analyze biological signaling networks. BMC Syst Biol 1(1):4CrossRefGoogle Scholar
  89. 89.
    Schivo DS, Scholma J, Wanders, B, Urquidi Camacho R, van der PV, Karperien H, Langerak R, van de JP, Post J (2012) Modelling biological pathway dynamics with timed automata. In: IEEE international conference on bioinformatics and bioengineering (ICBB), IEEE Computer Society, pp 447–453Google Scholar
  90. 90.
    Schivo S, Scholma J, van der Vet PE, Karperien M, Post JN, van de Pol J, Langerak R (2016) Modelling with animo: between fuzzy logic and differential equations. BMC Syst Biol 10(1):56CrossRefGoogle Scholar
  91. 91.
    Schwarick M, Heiner M (2009) CSL model checking of biochemical networks with interval decision diagrams. In: Computational methods in systems biology (CMSB), vol 5688, LNCS/LNBI, Springer, Berlin, pp 296–312CrossRefGoogle Scholar
  92. 92.
    Schwarick M, Rohr C, Heiner M (2011) MARCIE - Model checking And Reachability analysis done effiCIEntly . In: Quantitative evaluation of systems (QEST 2011). IEEE Computer Society, pp 91–100Google Scholar
  93. 93.
    Siebert H, Bockmayr A (2006) Incorporating time delays into the logical analysis of gene regulatory networks. Computational Methods in Systems Biology (CMSB), vol 4210. LNCS, Springer, Berlin Heidelberg, pp 169–183CrossRefGoogle Scholar
  94. 94.
    Swat M, Kel A, Herzel H (2004) Bifurcation analysis of the regulatory modules of the mammalian G1/S transition. Bioinformatics 20(10):1506–1511CrossRefGoogle Scholar
  95. 95.
    Yamada S, Taketomi T, Yoshimura A (2004) Model analysis of difference between EGF pathway and FGF pathway. Biochem Biophys Res Commun 314(4):1113–1120CrossRefGoogle Scholar
  96. 96.
    Yovine S (1997) Kronos: a verification tool for real-time systems. Int J Softw Tools Technol Transf 1:123–133CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Nikola Beneš
    • 1
  • Luboš Brim
    • 1
  • Samuel Pastva
    • 1
  • David Šafránek
    • 1
    Email author
  1. 1.Systems Biology Laboratory at Faculty of InformaticsMasaryk UniversityBrnoCzech Republic

Personalised recommendations