Yifan Wu

Yu Heng Wu, Houman Asgari, Stefano Rini et al.

This paper studies the problem of federated training of a deep neural network (DNN) over a random access channel (RACH) such as in computer networks, wireless networks, and cellular systems. More precisely, a set of remote users participate in training a centralized DNN model using SGD under the coordination of a parameter server (PS). The local model updates are transmitted from the remote users to the PS over a RACH using a slotted ALOHA protocol. The PS collects the updates from the remote users, accumulates them, and sends central model updates to the users at regular time intervals. We refer to this setting as the RACH-FL setting. The RACH-FL setting crucially addresses the problem of jointly designing a (i) client selection and (ii) gradient compression strategy which addresses the communication constraints between the remote users and the PS when transmission occurs over a RACH. For the RACH-FL setting, we propose a policy, which we term the ''age-of-gradient'' (AoG) policy in which (i) gradient sparsification is performed using top-K sparsification, (ii) the error correction is performed using memory accumulation, and (iii) the slot transmission probability is obtained by comparing the current local memory magnitude minus the magnitude of the gradient update to a threshold. Intuitively, the AoG measure of ''freshness'' of the memory state is reminiscent of the concept of age-of-information (AoI) in the context of communication theory and provides a rather natural interpretation of this policy. Numerical simulations show the superior performance of the AoG policy as compared to other RACH-FL policies.

Zhe Chen, Yunyun Chen, Robert M. Hierons et al.

Runtime Verification (RV) is a lightweight formal technique in which program or system execution is monitored and analyzed, to check whether certain properties are satisfied or violated after a finite number of steps. The use of RV has led to interest in deciding whether a property is monitorable: whether it is always possible for the satisfaction or violation of the property to be determined after a finite future continuation. However, classical two-valued monitorability suffers from two inherent limitations. First, a property can only be evaluated as monitorable or non-monitorable; no information is available regarding whether only one verdict (satisfaction or violation) can be detected. Second, monitorability is defined at the language-level and does not tell us whether satisfaction or violation can be detected starting from the current monitor state during system execution. To address these limitations, this paper proposes a new notion of four-valued monitorability for $ω$-languages and applies it at the state-level. Four-valued monitorability is more informative than two-valued monitorability as a property can be evaluated as a four-valued result, denoting that only satisfaction, only violation, or both are active for a monitorable property. We can also compute state-level weak monitorability, i.e., whether satisfaction or violation can be detected starting from a given state in a monitor, which enables state-level optimizations of monitoring algorithms. Based on a new six-valued semantics, we propose procedures for computing four-valued monitorability of $ω$-regular languages, both at the language-level and at the state-level. We have developed a new tool that implements the proposed procedure for computing monitorability of LTL formulas.