面向卫星联邦学习编排协议形式化验证
分布式、并行与集群计算
2025-01-23 v2
摘要
Python Testbed for Federated Learning Algorithms (PTB-FLA) 是一个针对边缘系统中智能物联网的简单 FL 框架，提供通用的集中式和去中心化 FL 算法，这些算法实现了使用过程代数 CSP 形式化验证的相应 FL 编排协议。这种方法适用于节点稳定的系统，但无法应用于节点移动的系统。本文利用天体力学建模 spacecraft 运动，并使用时序自动机 (TA) 对集中式 FL 编排协议进行形式化和验证，分为两个阶段。在第一个阶段，我们创建了传统 TA 模型来证明传统属性，即死锁自由性和终止性。在第二个阶段，我们创建了随机 TA 模型来证明时序正确性并估计终止概率。
引用
@article{arxiv.2410.13429,
title = {Towards Formal Verification of Federated Learning Orchestration Protocols on Satellites},
author = {Miroslav Popovic and Marko Popovic and Miodrag Djukic and Ilija Basicevic},
journal= {arXiv preprint arXiv:2410.13429},
year = {2025}
}
备注
4 pages, 5 figures, submitted to a conference