nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Parallel Parameter Synthesis for Multi-affine Hybrid Systems from Hybrid CTL Specifications

verfasst von : Eva Šmijáková, Samuel Pastva, David Šafránek, Luboš Brim

Erschienen in: Computational Methods in Systems Biology

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We consider the parameter synthesis problem for multi-affine hybrid systems and properties specified using a hybrid extension of CTL (HCTL). The goal is to determine the sets of parameter valuations for which the given hybrid system satisfies the desired HCTL property. As our main contribution, we propose a shared-memory parallel algorithm which efficiently computes such parameter valuation sets. We combine a rectangular discretisation of the continuous dynamics with the discrete transitions of the hybrid system to obtain a single over-approximating semi-symbolic transition system. Such system can be then analysed using a fixed-point parameter synthesis algorithm to obtain all satisfying parametrisations. We evaluate the scalability of the method and demonstrate its applicability in a biological case study.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel ABC(SMC): Simultaneous Inference and Model Checking of Chemical Reaction Networks

Nächstes Kapitel Core Models of Receptor Reactions to Evaluate Basic Pathway Designs Enabling Heterogeneous Commitments to Apoptosis

André, É.: IMITATOR: a tool for synthesizing constraints on timing bounds of timed automata. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 336–342. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03466-4_22CrossRef

Arellano, G., et al.: “Antelope”: a hybrid-logic model checker for branching-time Boolean GRN analysis. BMC Bioinform. 12(1), 490 (2011)CrossRef

Bartocci, E., Bortolussi, L., Nenzi, L., Sanguinetti, G.: On the robustness of temporal properties for stochastic models. In: Dang, T., Piazza, C. (eds.) Proceedings Second International Workshop on Hybrid Systems and Biology, HSB 2013, Taormina, Italy, 2nd September 2013. EPTCS, vol. 125, pp. 3–19 (2013)

Batt, G., Belta, C., Weiss, R.: Model checking genetic regulatory networks with parameter uncertainty. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 61–75. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71493-4_8CrossRef

Belta, C.: On controlling aircraft and underwater vehicles. In: Proceedings of the IEEE International Conference on Robotics and Automation, vol. 5, pp. 4905–4910 (2004)

Belta, C., Habets, L.: Controlling a class of nonlinear systems on rectangles. IEEE Trans. Autom. Control 51(11), 1749–1759 (2006)MathSciNetCrossRef

Beneš, N., Brim, L., Demko, M., Pastva, S., Šafránek, D.: A model checking approach to discrete bifurcation analysis. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 85–101. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_6CrossRef

Beneš, N., Brim, L., Demko, M., Pastva, S., Šafránek, D.: Parallel SMT-based parameter synthesis with application to piecewise multi-affine systems. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 192–208. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_13CrossRefMATH

Beneš, N., Brim, L., Demko, M., Pastva, S., Šafránek, D.: Pithya: a parallel tool for parameter synthesis of piecewise multi-affine dynamical systems. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 591–598. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_29CrossRef

10.

Beneš, N., Brim, L., Pastva, S., Šafránek, D.: Parallel parameter synthesis algorithm for hybrid CTL. Sci. Comput. Program. 185, 102321 (2019)CrossRef

11.

Beneš, N., Brim, L., Demko, M., Pastva, S., Šafránek, D.: Pithya: a parallel tool for parameter synthesis of piecewise multi-affine dynamical systems. Int. J. Struct. Stab. Dyn. (2017)

12.

Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., Grosu, R.: Abstraction-based parameter synthesis for multiaffine systems. Hardw. Softw.: Verif. Test. 11, 19–35 (2015)

13.

Bortolussi, L., Milios, D., Sanguinetti, G.: U-Check: model checking and parameter synthesis under uncertainty. In: Campos, J., Haverkort, B.R. (eds.) QEST 2015. LNCS, vol. 9259, pp. 89–104. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-22264-6_6CrossRef

14.

Bortolussi, L., Policriti, A.: Hybrid systems and biology. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 424–448. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68894-5_12CrossRef

15.

Bortolussi, L., Sanguinetti, G.: Smoothed model checking for uncertain continuous time Markov chains. CoRR abs/1402.1450 (2014)

16.

Brim, L., Češka, M., Demko, M., Pastva, S., Šafránek, D.: Parameter synthesis by parallel coloured CTL model checking. In: Roux, O., Bourdon, J. (eds.) CMSB 2015. LNCS, vol. 9308, pp. 251–263. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23401-4_21CrossRef

17.

Calzone, L., Fages, F., Soliman, S.: BIOCHAM: an environment for modeling biological systems and formalizing experimental knowledge. Bioinformatics 22(14), 1805–1807 (2006)CrossRef

18.

Chiang, H.K., Fages, F., Jiang, J.R., Soliman, S.: Hybrid simulations of heterogeneous biochemical models in SBML. ACM Trans. Model. Comput. Simul. 25(2), 14:1–14:22 (2015)

19.

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). https://doi.org/10.1007/10722167_15CrossRef

20.

Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)MATH

21.

Demko, M., Beneš, N., Brim, L., Pastva, S., Šafránek, D.: High-performance symbolic parameter synthesis of biological models: a case study. In: Bartocci, E., Lio, P., Paoletti, N. (eds.) CMSB 2016. LNCS, vol. 9859, pp. 82–97. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-45177-0_6CrossRef

22.

Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_17CrossRef

23.

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). https://doi.org/10.1007/978-3-642-00602-9_12CrossRefMATH

24.

Fages, F., Rizk, A.: From model-checking to temporal logic constraint solving. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 319–334. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04244-7_26CrossRef

25.

Frehse, G., Jha, S.K., Krogh, B.H.: A counterexample-guided approach to parameter synthesis for linear hybrid automata. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 187–200. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78929-1_14CrossRefMATH

26.

Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_30CrossRef

27.

Fribourg, L., Kühne, U.: Parametric verification and test coverage for hybrid automata using the inverse method. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 191–204. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24288-5_17CrossRef

28.

Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Automated Deduction - CADE-24, pp. 208–214 (2013)

29.

Grosu, R., et al.: From cardiac cells to genetic regulatory networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 396–411. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_31CrossRef

30.

Henzinger, T.A.: The theory of hybrid automata. In: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pp. 278–292, July 1996

31.

Islam, M.A., et al.: Bifurcation analysis of cardiac alternans using \(\delta \)-decidability. In: Bartocci, E., Lio, P., Paoletti, N. (eds.) CMSB 2016. LNCS, vol. 9859, pp. 132–146. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-45177-0_9CrossRef

32.

de Jong, H.: Modeling and simulation of genetic regulatory systems: a literature review. J. Comput. Biol. 9(1), 67–103 (2002)MathSciNetCrossRef

33.

Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \(\delta \)-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200–205. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_15CrossRef

34.

Lincoln, P., Tiwari, A.: Symbolic systems biology: hybrid modeling and analysis of biological networks. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 660–672. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24743-2_44CrossRefMATH

35.

Liu, B., Kong, S., Gao, S., Zuliani, P., Clarke, E.M.: Parameter synthesis for cardiac cell hybrid models using \(\delta \)–decisions. In: Mendes, P., Dada, J.O., Smallbone, K. (eds.) CMSB 2014. LNCS, vol. 8859, pp. 99–113. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12982-2_8CrossRef

36.

Liu, L., Bockmayr, A.: Formalizing metabolic-regulatory networks by hybrid automata. bioRxiv (2019)

37.

Liu, X., Stechlinski, P.: Infectious Disease Modeling. Springer, Cham (2020). https://doi.org/10.1007/978-3-319-53208-0CrossRefMATH

38.

Rizk, A., Batt, G., Fages, F., Soliman, S.: Continuous valuations of temporal logic specifications with applications to parameter optimization and robustness measures. Theor. Comput. Sci. 412(26), 2827–2839 (2011). Foundations of Formal Reconstruction of Biochemical Networks

39.

Stéphanou, A., Volpert, V.: Hybrid modelling in biology: a classification review. Math. Model. Nat. Phenom. 11(1), 37–48 (2016)MathSciNetCrossRef

Titel: Parallel Parameter Synthesis for Multi-affine Hybrid Systems from Hybrid CTL Specifications
verfasst von: Eva Šmijáková
Samuel Pastva
David Šafránek
Luboš Brim
Verlag: Springer International Publishing
Buch: Computational Methods in Systems Biology
Print ISBN: 978-3-030-60326-7

Electronic ISBN: 978-3-030-60327-4

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-60327-4_15

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner