We present a novel approach to giving a final semantics to
pi-caculus in a category of bialgebras which capitalises on Higher Order
Abstract Syntax. Inspired by recent work on HD automata, we derive a
notion of automaton which allows for checking effectively bisimilarity of
finitary processes.