We address the problem of verifying safety properties for iterative numerical programs. This problem amounts in, given a program and its specification (a pair of pre and post conditions), to find a strong enough inductive invariant allowing to establish correctness. The verification problem being undecidable in general, our aim is to provide a powerful invariant synthesis method allowing to handle automatically a large number of programs in practice. We propose such a method based on a data-driven approach that is enhanced with symbolic bounded reachability analysis. Our method builds on prior work we published in CAV'22 [6] where we defined an invariant learning procedure based on a new technique for generating relevant decision-tree attributes extracted from convex separators of samples (sets of program states seen as vectors of integers). In this work, we show that by coupling the previous method with a symbolic bounded model checker it is possible to improve significantly performances both in terms of running time and in the number of solved cases. The model checker can help in two ways: it might prove faster that a program is unsafe (by hitting error states), or more interestingly, it can provide interpolants (showing unreachability of error states) which can be used as attributes to speed-up the convergence of the learning procedure. We have implemented our new algorithm and shown that it is quite competitive with state-of-the-art tools such as Spacer, CVC4/5, solving globally more cases than these tools on the SyGuS and SV-COMP benchmarks.
Deterministic Suffix-reading Automata (DSA) were introduced recently as a concise model for regular languages. DSAs can succinctly capture formal specifications that are based on sequences of input actions (and not just single actions). For a concurrent system, specifications may further depend on combinations of input sequences seen across multiple components (ports). For such systems, DSAs consider all possible interleavings, resulting in large and unreadable automata. In this work, we enrich DSAs to include a ∥ operator in its transitions. The resulting multi-port DSAs (mDSAs) can succinctly represent concurrent suffix-based specifications. Subsequently, we extend mDSAs to produce outputs on transitions, and show that state reachability becomes PSPACE-complete in the presence of outputs. Finally, we apply our results to the formal analysis of Expressive Decision Tables (EDT) – an industry notation for specifying requirements of reactive systems.
We study the impact of restricting the class of separator problems on the look-compute-move mobile robot model hierarchy. In particular, we show that reachability specifications are sufficient to separate the semi-synchronous and the asynchronous model variants when robots agree on the unit-distance, but the two model variants are equivalent when considering terminating problems and no coordinate system agreement.
Federated learning (FL) is a distributed machine learning (ML) scheme that enables collaborative model training without compromising data privacy. In the TinyML community, communication is often prioritized over computation due to the limited bandwidth of the client devices. This paper aims to explore the rationale behind this perception by focusing on small models with approximately 1M parameters and investigating the effects of quantization and sparsification techniques for computation and communication purposes. We introduce mathematical models essential for estimating the time and energy consumption of computation and communication in an FL setup. Our research explores various configurations that impact FL efficiency, including model quantization and sparsification, processor frequency, batch sizes, and ML architecture. Notably, we demonstrate that for small models, communication energy can be negligible compared to computational energy. Consequently, contrary to existing literature, we propose that sparsification for communication may not be necessary as it introduces additional computational effort and energy consumption to achieve a target accuracy without significant gains in communication energy. This research enhances our understanding of the trade-offs between communication and computation in FL, particularly for small models like in TinyML. By emphasizing the importance of computational energy, our findings provide valuable insights for the design and optimization of FL systems.
In this paper, we consider the pattern formation problem of mobile agents in n× m dynamic grids, requiring k agents in the grid to stay at x designated (target) nodes to form some shape (pattern). We assume that at most one link is missing at each round. In this case, some agent’s movement may be always blocked and the agent cannot reach any target node. In addition, if the number k of agents is smaller than the number x of target nodes, several target nodes cannot be occupied. For this reason, focusing on the relationship between the values of k and x, we consider variants of the pattern formation problem in dynamic grids and examine how differences in these requirements and the number of agents influence the design and performance of algorithms. First, we consider the case of k ≤ x . In this case, we consider the approximate pattern formation problem, requiring at least k-1 ( x . In this case, we consider the exact pattern formation problem, requiring each of the x target nodes to be occupied. For this problem, we propose an algorithm to achieve exact pattern formation in O(kn+km+mn) rounds. In particular, when k - x is sufficiently large, we show that exact pattern formation can be achieved in (n+m) rounds.
