Logic in Computer Science (LICS 1997)

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 Symp. on Logic in Computer Science, {LICS} 1997},
    year =	 1997,
    editor =	 {Glynn Winskel},
    month =	 {June}, 
    pages =      {172--182},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }