Presburger Arithmetic: From Automata To Formulas