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 notionof automatonis defined and shown, by means of a tableau technique, to capture the expressive power of fixpoint expressions. For interpretationover 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.

• Type: Conference
• Year: 1997
• Where: LICS
• Authors: David Janin
• Keywords: Arbitrary Complete Lattices, Automated Reasoning, Complete Lattices, Fixpoint Expression, LICS 1997