Abstract for: Formal Behaviour Classification under Uncertainty: Applying Formal Analysis to System Dynamics

A study was performed by the author on formal analysis of deeply uncertain non-linear systems in the context of System Dynamics (SD). The objective of this study was to develop a more insightful method to classify model behaviour for exploratory modelling. The long term vision of this study is an exploration method that results in more transparent behaviour clusters with more insightful influence of uncertainties than the current sampling and clustering approaches. To achieve this, a simple predator-prey model from literature was analysed. Uncertainties were specified on the parameters and the resulting behaviour was represented in phase portraits. Through further analysis of local, linearised behaviour around equilibrium points, classes of behaviour were defined on mathematical properties of the system instead of properties of the output. No model runs are required for this classification, which makes the method computationally attractive. For the predator-prey model, these behaviour classes resulted in well-defined analytic boundaries in the uncertainty space. The major finding of the study is that formal analysis can divide the uncertainty space into regions that result in different behaviour.