SynCoP 2024

Using statistical model checking in a process for evaluating and calibrating a model of tropical forest dynamics

Modeling of tropical forest dynamics is particularly challenging, notably because of the variability of plant species which tends to require additional complexity and non identifiable parameters in models. In this talk, we will describe the procedure we used to calibrate such a model and generate - using SMC - sets of parameters that closely reproduce actual data from several plots in the Amazon basin, the majority of which was subject to logging in 1988. Rather than a single set of parameters, our method returns several small cells extracted from a large parameter space, which represent possible forest dynamics while taking into account the heterogeneity of the different plots using a reduced set of non directly identifiable parameters. The results are then used to simulate various intensity and frequency of logging to assess the level of resilience of the forest ecosystem. Finally, we will offer a few perspectives on techniques which could allow for a finer integration of the domain experts in the process.

SSSmoothRazor: SynthesiS of Smooth parameters using Ockham's Razor (joint work with D. Martin Xavier and L. Chamoin)

It has been theoretically explained, through the notion of Neural Tangent Kernel, why the training error of overparameterized networks converges linearly to 0. In this letter, we focus on the case of small (or underparameterized) networks. An advantage of small networks is that they are faster to train while retaining sufficient precision to perform useful tasks in many applications. Our main theoretical contribution is to prove that the training error of small networks converges linearly to a (non-null) constant, of which we give a precise estimate. We verify this result on a neural network of 10 neurons simulating a Model Predictive Controller. We also observe that an upper bound of the generalization error follows a double-peak curve as the number of training data increases.

Rewriting Modulo SMT Techniques for Parametric Analysis (joint work with J. Arias, K. Bae, P. Ölveczky, L. Petrucci and F. Rømming).

Many computer systems today are real-time systems whose correctness depend crucially on time and on the correct values of their parameters. However, in system design we often do not know in advance the concrete values of key system parameters, and want to find those values that make the system behave as desired. Parametric timed automata (PTA) extend timed automata to the case where the values of some system parameters are unknown. Similarly, Parametric time Petri nets (PITPN) extend time Petri nets to the setting where bounds on when transitions can fire are (partially) unknown.

In this talk, we will see how the behavior of PTAs and PITPNs can be adequately captured in the framework of rewriting logic modulo SMT. The proposed rewriting semantics is correct with respect to the standard semantics of PTAs and PITPNs, and it is executable in the Maude system connected with SMT solvers. Different analyses including EF-synthesis (computing values for the parameters to reach a state satisfying a property) and AG-safety-synthesis (values for the parameters to avoid some states) can be solved by Maude. Furthermore, our approach also supports analysis combined with user-defined execution strategies and full LTL model checking.

Verification of Parametric Markov Chains

This talk presents verification approaches for parametric Markov chains in both discrete-time and continuous-time.

The first part presents an approach to synthesize optimal bias for Herman's self-stabilizing token ring algorithm. The approach uses a parametric DTMC and common parameter synthesis techniques to efficiently find optimal parameter values. The results show that biased coins lead to faster convergence than fair coins.

The second part presents an analysis for CTMC with parametric transition rates and a prior on the parameter values. Sampling the parameter values from the prior distribution yields a non-parametric CTMC which can be analysed with standard techniques. The approach employs a finite set of parameter samples and a technique called scenario-optimization to yield prediction regions. These regions contain the analysis results for any additional sample point with high probability.