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.
