Sciweavers

LICS
1997
IEEE

Automata, Tableaus and a Reduction Theorem for Fixpoint Calculi in Arbitrary Complete Lattices

14 years 1 months ago
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.
David Janin
Added 26 Aug 2010
Updated 26 Aug 2010
Type Conference
Year 1997
Where LICS
Authors David Janin
Comments (0)