Parameter synthesis of polynomial dynamical systems

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.