Authors: Prokić, Ivan
Ghilezan, Silvia 
Kašterović, Simona
Popović, Miroslav
Popović, Marko
Kaštelan, Ivan
Affiliations: Mathematics 
Mathematical Institute of the Serbian Academy of Sciences and Arts 
Title: Correct orchestration of Federated Learning generic algorithms: formalisation and verification in CSP
Conference: ECBS 2023 - 8th International Conference on the Engineering of Computer Based Systems, Västerås, Sweden
Issue Date: 2023
Rank: M33
DOI: 10.48550/arXiv.2306.14529
Federated learning (FL) is a machine learning setting where clients keep the
training data decentralised and collaboratively train a model either under the
coordination of a central server (centralised FL) or in a peer-to-peer network
(decentralised FL). Correct orchestration is one of the main challenges. In
this paper, we formally verify the correctness of two generic FL algorithms, a
centralised and a decentralised one, using the CSP process calculus and the PAT
model checker. The CSP models consist of CSP processes corresponding to generic
FL algorithm instances. PAT automatically proves the correctness of the two
generic FL algorithms by proving their deadlock freeness (safety property) and
successful termination (liveness property). The CSP models are constructed
bottom-up by hand as a faithful representation of the real Python code and is
automatically checked top-down by PAT.
Keywords: Decentralised intelligence | Federated learning | Python | Formal verification | CSP process calculus

Show full item record

Page view(s)

checked on May 9, 2024

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.