An official website of the United States government
In this paper, we propose a concept of approximate bisimulation relation for feedforward neural networks. In the framework of approximate bisimulation relation, a novel neural network merging method is developed to compute the approximate bisimulation error between two neural networks based on reachability analysis of neural networks. The developed method is able to quantitatively measure the distance between the outputs of two neural networks with the same inputs. Then, we apply the approximate bisimulation relation results to perform neural networks model reduction and compute the compression precision, i.e., assured neural networks compression. At last, using the assured neural network compression, we accelerate the verification processes of ACAS Xu neural networks to illustrate the effectiveness and advantages of our proposed approximate bisimulation approach.
more »
« less
This content will become publicly available on October 19, 2026
Bisimulations and Reversibility
Concurrency and causality can be expressed within a labelled transition system by exploiting reversibility of transitions. It is natural to ask what behavioural equivalences can be captured by bisimulations in the reversible setting. In this paper we work with keyed configuration structures and CCSK, establish an operational correspondence between the two models, and give definitions of hereditary history-preserving bisimulation and history-preserving bisimulation in both models. We then present several characterisation results for the two bisimulations in terms of previously proposed, as well as new, “reverse” bisimulations.
more »
« less
- Award ID(s):
- 2242786
- PAR ID:
- 10658096
- Editor(s):
- Mezzina, Claudio Antares; Schmitt, Alan
- Publisher / Repository:
- Springer Nature Switzerland
- Date Published:
- Page Range / eLocation ID:
- 46 to 67
- Subject(s) / Keyword(s):
- Concurrency Process Algebras Configuration Structures Labelled Transition System Reversibility Bisimulation
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
We prove that every orientation-preserving homeomorphism of Euclidean space can be expressed as a commutator of two orientation-preserving homeomorphisms. We give an analogous result for annuli. In the annulus case, we also extend the result to the smooth category in the dimensions for which the associated sphere has a unique smooth structure. As a corollary, we establish that every orientation-preserving diffeomorphism of the real line is the commutator of two orientation-preserving diffeomorphisms.more » « less
-
With the proliferation of Beyond 5G (B5G) communication systems and heterogeneous networks, mobile broadband users are generating massive volumes of data that undergo fast processing and computing to obtain actionable insights. While analyzing this huge amount of data typically involves machine and deep learning-based data-driven Artificial Intelligence (AI) models, a key challenge arises in terms of providing privacy assurances for user-generated data. Even though data-driven techniques have been widely utilized for network traffic analysis and other network management tasks, researchers have also identified that applying AI techniques may often lead to severe privacy concerns. Therefore, the concept of privacy-preserving data-driven learning models has recently emerged as a hot area of research to facilitate model training on large-scale datasets while guaranteeing privacy along with the security of the data. In this paper, we first demonstrate the research gap in this domain, followed by a tutorial-oriented review of data-driven models, which can be potentially mapped to privacy-preserving techniques. Then, we provide preliminaries of a number of privacy-preserving techniques (e.g., differential privacy, functional encryption, Homomorphic encryption, secure multi-party computation, and federated learning) that can be potentially adopted for emerging communication networks. The provided preliminaries enable us to showcase the subset of data-driven privacy-preserving models, which are gaining traction in emerging communication network systems. We provide a number of relevant networking use cases, ranging from the B5G core and Radio Access Networks (RANs) to semantic communications, adopting privacy-preserving data-driven models. Based on the lessons learned from the pertinent use cases, we also identify several open research challenges and hint toward possible solutions.more » « less
-
Multi-label image recognition has been an indispensable fundamental component for many real computer vision applications. However, a severe threat of privacy leakage in multi-label image recognition has been overlooked by existing studies. To fill this gap, two privacy-preserving models, Privacy-Preserving Multi-label Graph Convolutional Networks (P2-ML-GCN) and Robust P2-ML-GCN (RP2-ML-GCN), are developed in this article, where differential privacy mechanism is implemented on the model’s outputs so as to defend black-box attack and avoid large aggregated noise simultaneously. In particular, a regularization term is exploited in the loss function of RP2-ML-GCN to increase the model prediction accuracy and robustness. After that, a proper differential privacy mechanism is designed with the intention of decreasing the bias of loss function in P2-ML-GCN and increasing prediction accuracy. Besides, we analyze that a bounded global sensitivity can mitigate excessive noise’s side effect and obtain a performance improvement for multi-label image recognition in our models. Theoretical proof shows that our two models can guarantee differential privacy for model’s outputs, weights and input features while preserving model robustness. Finally, comprehensive experiments are conducted to validate the advantages of our proposed models, including the implementation of differential privacy on model’s outputs, the incorporation of regularization term into loss function, and the adoption of bounded global sensitivity for multi-label image recognition.more » « less
-
null (Ed.)We consider abstraction-based design of output-feedback controllers for dynamical systemswith a finite set of inputs and outputs against specifications in linear-time temporal logic. The usual procedure for abstraction-based controller design (ABCD) first constructs a finite-state abstraction of the underlying dynamical system, and second, uses reactive synthesis techniques to compute an abstract state-feedback controller on the abstraction. In this context, our contribution is two-fold: (I) we define a suitable relation between the original systemand its abstractionwhich characterizes the soundness and completeness conditions for an abstract state-feedback controller to be refined to a concrete output-feedback controller for the original system, and (II) we provide an algorithm to compute a sound finite-state abstraction fulfilling this relation. Our relation generalizes feedback-refinement relations fromABCD with state-feedback. Our algorithm for constructing sound finitestate abstractions is inspired by the simultaneous reachability and bisimulation minimization algorithm of Lee and Yannakakis. We lift their idea to the computation of an observation-equivalent system and show how sound abstractions can be obtained by stopping this algorithm at any point. Additionally, our new algorithm produces a realization of the topological closure of the input/output behavior of the original system if it is finite state realizable.more » « less
