-
Correct orchestration of Federated Learning generic algorithms: formalisation and verification in CSP
Authors:
Ivan Prokić,
Silvia Ghilezan,
Simona Kašterović,
Miroslav Popovic,
Marko Popovic,
Ivan Kaštelan
Abstract:
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 centralise…
▽ More
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.
△ Less
Submitted 26 June, 2023;
originally announced June 2023.
-
Logic of Combinatory Logic
Authors:
Simona Kašterović,
Silvia Ghilezan
Abstract:
We develop a classical propositional logic for reasoning about combinatory logic. We define its syntax, axiomatic system and semantics. The syntax and axiomatic system are presented based on classical propositional logic, with typed combinatory terms as basic propositions, along with the semantics based on applicative structures extended with special elements corresponding to primitive combinators…
▽ More
We develop a classical propositional logic for reasoning about combinatory logic. We define its syntax, axiomatic system and semantics. The syntax and axiomatic system are presented based on classical propositional logic, with typed combinatory terms as basic propositions, along with the semantics based on applicative structures extended with special elements corresponding to primitive combinators. Both the equational theory of untyped combinatory logic and the proposed axiomatic system are proved to be sound and complete w.r.t. the given semantics. In addition, we prove that combinatory logic is sound and complete w.r.t. the given semantics.
△ Less
Submitted 13 December, 2022;
originally announced December 2022.
-
L-types for resource aware languages: an implicit name approach
Authors:
Silvia Ghilezan,
Jelena Ivetić,
Simona Kašterović,
Pierre Lescanne
Abstract:
A novel formalisation of variable control in languages with implicit names based on de Bruijn indices is presented. We design and implement three languages: first, a restricted language with implicit names; then, a restricted calculus with implicit names and explicit substitution, and finally, an extended calculus with implicit names and resource control. We propose a novel concept of list types,…
▽ More
A novel formalisation of variable control in languages with implicit names based on de Bruijn indices is presented. We design and implement three languages: first, a restricted language with implicit names; then, a restricted calculus with implicit names and explicit substitution, and finally, an extended calculus with implicit names and resource control. We propose a novel concept of list types, which are used to give a simple and manageable definition of linearity. We develop an implementation in Haskell.
△ Less
Submitted 27 February, 2025; v1 submitted 21 December, 2021;
originally announced December 2021.
