Paper: Automata, tableaus and a reduction theorem for fixpoint calculi in arbitrary complete lattices (at LICS 1997)

Authors: David Janin

Abstract

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 tableau technique, to capture the expressive power of fixpoint expressions. For interpretation over continuous and complete lattices, when, moreover, meet symbol commutes in rough sense with all other functional symbols, it is shown that any closed fixpoint expressions is equivalent to a fixpoint expression built without meet symbol. This result generalize Muller and Schupp simulation theorem for alternating automata on the binary tree.

BibTeX

  @InProceedings{Janin-Automatatableausand,
    author = 	 {David Janin},
    title = 	 {Automata, tableaus and a reduction theorem for fixpoint calculi in arbitrary complete lattices},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS 1997)},
    year =	 {1997},
    month =	 {June}, 
    pages =      {172--182},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }