Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Safety Verification of Deep Neural Networks Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems

Authors : Nikola Beneš, Luboš Brim, Martin Demko, Samuel Pastva, David Šafránek

Published in: Computer Aided Verification

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We present a novel tool for parameter synthesis of piecewise multi-affine dynamical systems from specifications expressed in a hybrid branching-time temporal logic. The tool is based on the algorithm of parallel semi-symbolic coloured model checking that extends standard model checking methods to cope with parametrised Kripke structures. The tool implements state-of-the-art techniques developed in our previous research and is primarily intended to be used for the analysis of dynamical systems with uncertain parameters that frequently arise in computational systems biology. However, it can be employed for any dynamical system where the non-linear equations can be sufficiently well approximated by piecewise multi-affine equations.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
previous chapter Compositional Model Checking with Incremental Counter-Example Construction
Literature
1.
2.
Arellano, G., Argil, J., Azpeitia, E., Benítez, M., Carrillo, M., Góngora, P., Rosenblueth, D.A., Alvarez-Buylla, E.R.: “Antelope”: a hybrid-logic model checker for branching-time Boolean GRN analysis. BMC Bioinf. 12(1), 1–15 (2011)CrossRef
3.
Batt, G., Page, M., Cantone, I., Gössler, G., Monteiro, P., de Jong, H.: Efficient parameter search for qualitative models of regulatory networks using symbolic model checking. Bioinformatics 26(18), 603–610 (2010)CrossRef
4.
Batt, G., Yordanov, B., Weiss, R., Belta, C.: Robustness analysis and tuning of synthetic gene networks. Bioinformatics 23(18), 2415–2422 (2007)CrossRef
5.
ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119–135 (2011)CrossRefMATH
6.
Beneš, N., Brim, L., Demko, M., Pastva, S., Šafránek, D.: Parallel SMT-based parameter synthesis with application to piecewise multi-affine systems. In: ATVA 2016. LNCS, vol. 9936, pp. 1–17. Springer, Cham (2016)
7.
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). doi:10.​1007/​978-3-319-48989-6_​6
8.
Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: UPPAAL — a tool suite for automatic verification of real-time systems. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996). doi:10.​1007/​BFb0020949 CrossRef
9.
Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., Grosu, R.: Abstraction-based parameter synthesis for multiaffine systems. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 19–35. Springer, Cham (2015). doi:10.​1007/​978-3-319-26287-1_​2 CrossRef
10.
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). doi:10.​1007/​978-3-319-22264-6_​6 CrossRef
11.
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). doi:10.​1007/​978-3-319-23401-4_​21 CrossRef
12.
Brim, L., Demko, M., Pastva, S., Šafránek, D.: High-performance discrete bifurcation analysis for piecewise-affine dynamical systems. In: Abate, A., Šafránek, D. (eds.) HSB 2015. LNCS, vol. 9271, pp. 58–74. Springer, Cham (2015). doi:10.​1007/​978-3-319-26916-0_​4 CrossRef
13.
Brim, L., Vejpustek, T., Šafránek, D., Fabriková, J.: Robustness analysis for value-freezing signal temporal logic. In: HSB 2013, EPTCS, vol. 125, pp. 20–36 (2013)
14.
Brim, L., Yorav, K., Žídková, J.: Assumption-based distribution of CTL model checking. STTT 7(1), 61–73 (2005)CrossRef
15.
Češka, M., Pilař, P., Paoletti, N., Brim, L., Kwiatkowska, M.: PRISM-PSY: precise GPU-accelerated parameter synthesis for stochastic systems. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 367–384. Springer, Heidelberg (2016). doi:10.​1007/​978-3-662-49674-9_​21 CrossRef
16.
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)CrossRefMATH
17.
Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.-P., Ábrahám, E.: PROPhESY: a probabilistic parameter synthesis tool. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214–231. Springer, Cham (2015). doi:10.​1007/​978-3-319-21690-4_​13 CrossRef
18.
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). doi:10.​1007/​978-3-319-45177-0_​6 CrossRef
19.
Donzé, A., Fanchon, E., Gattepaille, L.M., Maler, O., Tracqui, P.: Robustness analysis and behavior discrimination in enzymatic reaction networks. PLoS ONE 6(9), e24246 (2011)CrossRef
20.
Dreossi, T.: Sapo: Reachability computation and parameter synthesis of polynomial dynamical systems. CoRR abs/1607.02200 (2016)
21.
Fisher, J., Henzinger, T.: Executable cell biology. Nat. Biotechnol. 25(11), 1239–1249 (2007)CrossRef
22.
Grosu, R., Batt, G., Fenton, F.H., Glimm, J., Guernic, C., Smolka, S.A., Bartocci, E.: From cardiac cells to genetic regulatory networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 396–411. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​31 CrossRef
23.
Hajnal, M., Šafránek, D., Demko, M., Pastva, S., Krejčí, P., Brim, L.: Toward modelling and analysis of transient and sustained behaviour of signalling pathways. In: Cinquemani, E., Donzé, A. (eds.) HSB 2016. LNCS, vol. 9957, pp. 57–66. Springer, Cham (2016). doi:10.​1007/​978-3-319-47151-8_​4
24.
Madsen, C., Shmarov, F., Zuliani, P.: BioPSy: an SMT-based tool for guaranteed parameter set synthesis of biological models. In: Roux, O., Bourdon, J. (eds.) CMSB 2015. LNCS, vol. 9308, pp. 182–194. Springer, Cham (2015). doi:10.​1007/​978-3-319-23401-4_​16 CrossRef
25.
26.
Rizk, A., Batt, G., Fages, F., Soliman, S.: A general computational method for robustness analysis with applications to synthetic gene networks. Bioinformatics 25(12), i169–i178 (2009)CrossRef
27.
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)CrossRef
28.
Streck, A.: Toolkit for reverse engineering of molecular pathways via parameter identification. Ph.D. thesis, Free University of Berlin, Germany (2016)
29.
Streck, A., Kolčák, J., Siebert, H., Šafránek, D.: Esther: introducing an online platform for parameter identification of boolean networks. In: Gupta, A., Henzinger, T.A. (eds.) CMSB 2013. LNBI, vol. 8130, pp. 257–258. Springer, Heidelberg (2013)
Metadata
Title
Pithya: A Parallel Tool for Parameter Synthesis of Piecewise Multi-affine Dynamical Systems
Authors
Nikola Beneš
Luboš Brim
Martin Demko
Samuel Pastva
David Šafránek
Copyright Year
2017
Book
Computer Aided Verification

Print ISBN: 978-3-319-63386-2

Electronic ISBN: 978-3-319-63387-9

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-63387-9_29

Premium Partner

    Image Credits