Parametric dynamical systems emerge as a formalism for modelling natural and engineered systems ranging from biology, epidemiology, and medicine to cyber-physics. Parameter tuning is a complex task usually performed by exploiting heavy simulations having high computational complexity and not ensuring the correctness of the synthesized systems. We consider the problem of parameter synthesis for discrete-time polynomial systems. We propose a formal method based on Bernstein coefficients that allows refining the set of parameters according to a temporal specification defined as a Signal Temporal Logic formula. The synthesized system is correct with respect to the specification and we demonstrate the scalability of the approach by implementing it in the C++ library Sapo, also available within a stand-alone application and as a web application. Finally, we illustrate the tool usage and the interface through a simple yet realistic epidemiological model and consider an intriguing application enhancing the accuracy of the verification of neural networks.

Parameter synthesis of polynomial dynamical systems

Alberto Casagrande;
2022-01-01

Abstract

Parametric dynamical systems emerge as a formalism for modelling natural and engineered systems ranging from biology, epidemiology, and medicine to cyber-physics. Parameter tuning is a complex task usually performed by exploiting heavy simulations having high computational complexity and not ensuring the correctness of the synthesized systems. We consider the problem of parameter synthesis for discrete-time polynomial systems. We propose a formal method based on Bernstein coefficients that allows refining the set of parameters according to a temporal specification defined as a Signal Temporal Logic formula. The synthesized system is correct with respect to the specification and we demonstrate the scalability of the approach by implementing it in the C++ library Sapo, also available within a stand-alone application and as a web application. Finally, we illustrate the tool usage and the interface through a simple yet realistic epidemiological model and consider an intriguing application enhancing the accuracy of the verification of neural networks.
2022
nov-2022
Pubblicato
https://doi.org/10.1016/j.ic.2022.104941
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S0890540122000967-main.pdf

Accesso chiuso

Tipologia: Documento in Versione Editoriale
Licenza: Copyright Editore
Dimensione 1.71 MB
Formato Adobe PDF
1.71 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
1-s2.0-S0890540122000967-main-Post_print.pdf

Open Access dal 15/07/2023

Tipologia: Bozza finale post-referaggio (post-print)
Licenza: Creative commons
Dimensione 2.36 MB
Formato Adobe PDF
2.36 MB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11368/3025969
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 0
social impact