Table of Contents
Fetching ...

Explaining Control Policies through Predicate Decision Diagrams

Debraj Chakraborty, Clemens Dubslaff, Sudeep Kanav, Jan Kretinsky, Christoph Weinhuber

TL;DR

This work tackles the explainability gap in automatically synthesized controllers by introducing Predicate Decision Diagrams (PDDs), which fuse the interpretability of decision trees with the sharing benefits of reduced ordered BDDs. The authors present a synthesis pipeline that derives PDDs from learned DTs and apply BDD-reduction techniques, including predicate encoding, consistency enforcement, variable-order optimization, and care-set reduction. Empirical results on standard benchmarks show that PDDs are often as small as DTs and substantially smaller than bit-blasted BDDs, with substantial node sharing driving improvements. Ablation studies demonstrate that consistency checks, reordering, and care-set reduction collectively reduce PDD size and enhance explainability, supporting PDDs as a practical, explainable representation for control policies. The work also outlines paths for integrating PDDs with mature BDD toolchains and extending to richer predicate theories, enabling scalable, explainable controller representations in real-world systems.

Abstract

Safety-critical controllers of complex systems are hard to construct manually. Automated approaches such as controller synthesis or learning provide a tempting alternative but usually lack explainability. To this end, learning decision trees (DTs) have been prevalently used towards an interpretable model of the generated controllers. However, DTs do not exploit shared decision-making, a key concept exploited in binary decision diagrams (BDDs) to reduce their size and thus improve explainability. In this work, we introduce predicate decision diagrams (PDDs) that extend BDDs with predicates and thus unite the advantages of DTs and BDDs for controller representation. We establish a synthesis pipeline for efficient construction of PDDs from DTs representing controllers, exploiting reduction techniques for BDDs also for PDDs.

Explaining Control Policies through Predicate Decision Diagrams

TL;DR

This work tackles the explainability gap in automatically synthesized controllers by introducing Predicate Decision Diagrams (PDDs), which fuse the interpretability of decision trees with the sharing benefits of reduced ordered BDDs. The authors present a synthesis pipeline that derives PDDs from learned DTs and apply BDD-reduction techniques, including predicate encoding, consistency enforcement, variable-order optimization, and care-set reduction. Empirical results on standard benchmarks show that PDDs are often as small as DTs and substantially smaller than bit-blasted BDDs, with substantial node sharing driving improvements. Ablation studies demonstrate that consistency checks, reordering, and care-set reduction collectively reduce PDD size and enhance explainability, supporting PDDs as a practical, explainable representation for control policies. The work also outlines paths for integrating PDDs with mature BDD toolchains and extending to richer predicate theories, enabling scalable, explainable controller representations in real-world systems.

Abstract

Safety-critical controllers of complex systems are hard to construct manually. Automated approaches such as controller synthesis or learning provide a tempting alternative but usually lack explainability. To this end, learning decision trees (DTs) have been prevalently used towards an interpretable model of the generated controllers. However, DTs do not exploit shared decision-making, a key concept exploited in binary decision diagrams (BDDs) to reduce their size and thus improve explainability. In this work, we introduce predicate decision diagrams (PDDs) that extend BDDs with predicates and thus unite the advantages of DTs and BDDs for controller representation. We establish a synthesis pipeline for efficient construction of PDDs from DTs representing controllers, exploiting reduction techniques for BDDs also for PDDs.

Paper Structure

This paper contains 25 sections, 5 theorems, 1 equation, 9 figures, 10 tables, 2 algorithms.

Key Result

lemma 1

Given a PDD $\mathcal{{P}}\xspace$, a predicate bijection $\gamma$ for $\mathcal{{P}}\xspace$ over variables $\mathit{PVar}$, and a total order $\pi$ over $\mathit{PVar}$, Pdd2Bdd$(\mathcal{{P}}\xspace,\gamma,\pi)$ (see alg:compile) returns a $\pi$-BDD that is equivalent modulo $\gamma$ to $\mathcal

Figures (9)

  • Figure 1: Examples of DT control policy representations: deterministic control policy (left) and permissive control policy with multiple actions at some states (right).
  • Figure 2: An example of a policy in the form of a lookup table (left), and the corresponding decision tree (right).
  • Figure 3: Compilation of the DT in \ref{['fig:ex-tree']} to a (predicate inconsistent) BDD (left) using \ref{['alg:compile']}. A predicate consistent BDD (right) can be created by replacing the inconsistent part by the blue edge using \ref{['alg:pconsistency']}.
  • Figure 4: PDD synthesis pipeline used in the experiments
  • Figure 5: Comparison of normalized sizes of constructed PDDs and bbBDDs. Ratios of PDD (bbBDD, respectively) sizes to the number of states in the represented controller.
  • ...and 4 more figures

Theorems & Definitions (9)

  • definition 1: Policy
  • definition 2: DT
  • definition 3: BDD
  • definition 4
  • lemma 1
  • lemma 2
  • theorem 1
  • lemma 2
  • lemma 2