Eventizing Traditionally Opaque Binary Neural Networks as 1-safe Petri net Models

TL;DR

The paper addresses the opacity of Binary Neural Networks (BNNs) in safety-critical contexts by introducing a Petri net (PN) based event-driven framework that exposes the causal structure from data loading through weight updates. It develops modular PN blueprints for both inference and training, and employs the Workcraft toolset for automated structural and behavioral verification, including 1-safeness and deadlock-freeness, as well as reachability and sequencing checks. The approach is validated against a reference BNN and subjected to scalability analyses, revealing how causal transparency can be achieved at the cost of increased model size and complexity, particularly in floating-point weight updates. The work demonstrates a principled path toward explainable, formally verifiable ML models suitable for dependable deployment in hardware-constrained or safety-critical environments, while identifying challenges in scaling to larger architectures and datasets.

Abstract

Binary Neural Networks (BNNs) offer a low-complexity and energy-efficient alternative to traditional full-precision neural networks by constraining their weights and activations to binary values. However, their discrete, highly non-linear behavior makes them difficult to explain, validate and formally verify. As a result, BNNs remain largely opaque, limiting their suitability in safety-critical domains, where causal transparency and behavioral guarantees are essential. In this work, we introduce a Petri net (PN)-based framework that captures the BNN's internal operations as event-driven processes. By "eventizing" their operations, we expose their causal relationships and dependencies for a fine-grained analysis of concurrency, ordering, and state evolution. Here, we construct modular PN blueprints for core BNN components including activation, gradient computation and weight updates, and compose them into a complete system-level model. We then validate the composed PN against a reference software-based BNN, verify it against reachability and structural checks to establish 1-safeness, deadlock-freeness, mutual exclusion and correct-by-construction causal sequencing, before we assess its scalability and complexity at segment, component, and system levels using the automated measurement tools in Workcraft. Overall, this framework enables causal introspection of transparent and event-driven BNNs that are amenable to formal reasoning and verification.

Figures (19)

• Figure 1: C-element Specification. (a) Logic gate. (b) PN model.
• Figure 2: Architecture of BNN model performing 2-input XOR operation - used as an illustrative example.
• Figure 3: PN segment of data point loading with transitions representing data points, places for data vector initialization, and places for expected output.
• Figure 4: PN segment of initialization and binarization of real valued weights.
• Figure 5: Sequence of operations demonstrating weighted sums for pre-activation of a neuron.