Relational NetKAT (RN) is a new specification language for network change validation. Engineers use RN to specify intended changes by providing
a trace relation $R$, which maps existing packet traces in the pre-change network to intended packet traces in the post-change network. The
\emph{intended} set of traces may then be checked against the
\emph{actual} post-change traces to uncover errors in implementation. Trace
relations are constructed compositionally from a language of combinators
that include trace insertion, trace deletion, and packet
transformation, as well as regular operators for concatenation, union, and iteration of relations. We provide algorithms for converting trace relations into a new form of NetKAT transducer and also for constructing
an automaton that recognizes the image of a NetKAT automaton
under a NetKAT transducer. These algorithms, together with
existing decision procedures for NetKAT automaton equivalence, suffice for
validating network changes. We provide a denotational semantics
for our specification language, prove our compilation algorithms correct, implement a tool for network change validation, and evaluate it on a
set of benchmarks drawn from a production network and
Amazon's Batfish toolkit.