Evaluation of a graph distance metric to assess the diversity of timed automata

Abstract

Reliable testing and benchmarking of modelling tools require diverse inputs. However, diversity has no precise definition in this context, nor is there a given level of acceptance. While there is one diversity metric [1] that can be used to assess diversity for structural models, there is no such metric for behavioural models, like timed automata. In our research, we work on adapting the structural diversity metrics presented in [1] to behavioural models. We evaluate the structural diversity of timed automata by first transforming the models to a unified, structural format and then applying the structural diversity metric. In this paper, we present a way to adapt the distance metric to timed automata and we apply it to an existing benchmark suite. We evaluate the metric both manually – checking whether models that are similar according to the metric actually show similar behaviours –, and automatically – checking whether verification algorithms perform similarly well/poorly (with respect to other algorithms) on ’similar’ models. We show that – despite only considering structural differences – the metric can be useful for finding models with similar behaviours among timed automata.