Modeling and Analysis of Clustering by Medoids Using Uppaal

This paper describes an approach to formal modeling of clustering algorithms based on medoids using timed automata. The approach permits to assess properties such as the minimization of the sum-of-squared-error objective cost (SSE) by exhaustive model checking. Although constrained to integer semantics and problem instances of small size, the contribution, which is mainly inspired by didactic concerns, highlights how abstract specification of and reasoning on clustering by medoids can be established through the introduction of concrete data structures and functions in the context of the timed automata (TA) of the popular Uppaal model checker. The paper describes the rationale of the proposed approach, summarizes its implementation which purposely exploits the high-level character of the TA supported by Uppaal, and demonstrates its practical application through synthetic datasets.