The report presents a decision procedure for assertions in an extension of the mu-calculus about finite-control pi-calculus agents. The procedure is based on the classical cut-free sequent calculus and associated techniques of automatic theorem proving.