Algorithms on graphical structures play a central role in both communications technology and formal verification. Minimal trellises are graphical representations of error-correcting codes that have emerged as a unifying framework for understanding and manipulating codes of all types. Ordered binary decision diagrams and their variants are graph-based data structures for representing Boolean functions that have found widespread use in formal verification for a range of problems, including circuit checking, logic synthesis and test generation. This project builds on the close correspondence that has recently been established between the code trellis and binary decision diagram, and investigates the transfer of ideas between these previously disparate fields. The fundamental challenge that confronts both uses of graphical methods is the same: devise techniques to combat the exponential blowup in the size of the graph. The research is interdisciplinary, and can be expected to have a broad range of application, both within coding and verification, as well as to such areas as artificial intelligence, database search, and combinatorial optimization.
