Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

$\partial$CBDs: Differentiable Causal Block Diagrams

Thomas Beckers, Ján Drgoňa, Truong X. Nghiem

TL;DR

This work tackles the challenge of building cyber-physical systems that are simultaneously composable, learnable, and verifiable. It introduces differentiable Causal Block Diagrams ($\partial$CBDs), which integrate CBDs with assume--guarantee contracts and differentiable programming to enable end-to-end gradient-based learning while preserving formal guarantees. The framework provides five architectural layers, supports AD on rate-lifted, loop-unrolled CBD graphs, and embeds contracts as differentiable residuals to guide optimization. Through three contract-guided examples—ISS-based gain tuning, joint policy and Lyapunov learning, and Deep Koopman identification—the authors demonstrate end-to-end differentiable, certifiable learning across physics-based and data-driven components with scalable gradient-based training and verification.

Abstract

Modern cyber-physical systems (CPS) integrate physics, computation, and learning, demanding modeling frameworks that are simultaneously composable, learnable, and verifiable. Yet existing approaches treat these goals in isolation: causal block diagrams (CBDs) support modular system interconnections but lack differentiability for learning; differentiable programming (DP) enables end-to-end gradient-based optimization but provides limited correctness guarantees; while contract-based verification frameworks remain largely disconnected from data-driven model refinement. To address these limitations, we introduce differentiable causal block diagrams ($\partial$CBDs), a unifying formalism that integrates these three perspectives. Our approach (i) retains the compositional structure and execution semantics of CBDs, (ii) incorporates assume--guarantee (A--G) contracts for modular correctness reasoning, and (iii) introduces residual-based contracts as differentiable, trajectory-level certificates compatible with automatic differentiation (AD), enabling gradient-based optimization and learning. Together, these elements enable a scalable, verifiable, and trainable modeling pipeline that preserves causality and modularity while supporting data-, physics-, and constraint-informed optimization for CPS.

$\partial$CBDs: Differentiable Causal Block Diagrams

TL;DR

This work tackles the challenge of building cyber-physical systems that are simultaneously composable, learnable, and verifiable. It introduces differentiable Causal Block Diagrams (CBDs), which integrate CBDs with assume--guarantee contracts and differentiable programming to enable end-to-end gradient-based learning while preserving formal guarantees. The framework provides five architectural layers, supports AD on rate-lifted, loop-unrolled CBD graphs, and embeds contracts as differentiable residuals to guide optimization. Through three contract-guided examples—ISS-based gain tuning, joint policy and Lyapunov learning, and Deep Koopman identification—the authors demonstrate end-to-end differentiable, certifiable learning across physics-based and data-driven components with scalable gradient-based training and verification.

Abstract

Modern cyber-physical systems (CPS) integrate physics, computation, and learning, demanding modeling frameworks that are simultaneously composable, learnable, and verifiable. Yet existing approaches treat these goals in isolation: causal block diagrams (CBDs) support modular system interconnections but lack differentiability for learning; differentiable programming (DP) enables end-to-end gradient-based optimization but provides limited correctness guarantees; while contract-based verification frameworks remain largely disconnected from data-driven model refinement. To address these limitations, we introduce differentiable causal block diagrams (CBDs), a unifying formalism that integrates these three perspectives. Our approach (i) retains the compositional structure and execution semantics of CBDs, (ii) incorporates assume--guarantee (A--G) contracts for modular correctness reasoning, and (iii) introduces residual-based contracts as differentiable, trajectory-level certificates compatible with automatic differentiation (AD), enabling gradient-based optimization and learning. Together, these elements enable a scalable, verifiable, and trainable modeling pipeline that preserves causality and modularity while supporting data-, physics-, and constraint-informed optimization for CPS.
Paper Structure (26 sections, 1 theorem, 32 equations, 6 figures)

This paper contains 26 sections, 1 theorem, 32 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Methodology
  3. Causal Block Diagrams with Contracts
  4. Execution and Composition of CBDs
  5. Contracts for CBDs
  6. Differentiable Causal Block Diagrams
  7. Verifiable Optimization and Learning with Differentiable CBDs
  8. Scope and generality.
  9. Differentiability of the CBD-constrained optimization problem.
  10. Examples
  11. Example 1: Tuning of a Scalar Feedback Gain with Input to State Stability Certificate
  12. $\partial$CBD representation
  13. Stability contract.
  14. Contract-guided gain tuning.
  15. Simulation results.
  16. ...and 11 more sections

Key Result

lemma 1

Given blocks $\mathcal{B}_1$, $\mathcal{B}_2$, and $\mathcal{B}_3$, and admissible connections between them, the following properties hold.

Figures (6)

  • Figure 1: Illustrations of blocks and their compositions.
  • Figure 2: A standard feedback control loop (top) can be flattened into an equivalent block (bottom right) using the serial composition and feedback composition rules.
  • Figure 3: Closed-loop evolution of tuned vs untuned system.
  • Figure 4: Training evolution of gain and contract residual.
  • Figure 5: Closed-loop evolution of controlled Van Der Pol system with neural controller and Lyapunov contract.
  • ...and 1 more figures

Theorems & Definitions (22)

  • definition 1: Signal
  • definition 2: Block with Contract
  • Remark 1
  • definition 3: Unilateral Connection
  • definition 4: Causal Block Diagram (CBD)
  • definition 5: Parallel Composition
  • definition 6: Serial Composition
  • definition 7: Feedback Composition
  • lemma 1
  • definition 8: Assume--Guarantee Contract for a Block
  • ...and 12 more