Automata, tableaus and a reduction theorem for fixpoint calculi in arbitrary complete lattices

Fixpoint expressions built from functional signatures interpreted over arbitrary complete lattices are considered. A generic notion of automaton is defined and shown, by means of a tableau technique, to capture the expressive power of fixpoint expressions. For interpretation over continuous and complete lattices when, moreover, the meet symbol Λ commutes in a rough sense with all other functional symbols, it is shown that any closed fixpoint expression is equivalent to a fixpoint expression built without the meet symbol λ. This result generalizes Muller and Schupp´s simulation theorem for alternating automata on the binary tree