We consider classes of languages of overlapping tiles, i.e., subsets of the McAlister monoid: the class REG of languages definable by Kleene’s regular expressions, the class MSO of languages definable by formulas of monadic second-order logic, and th

As is already known from the work of D. Janin & I. Walukiewicz (1996), the mu-calculus is as expressive as the bisimulation-invariant fragment of monadic second-order logic. In this paper, we relate the expressiveness of levels of the fixpoint alternation depth hierarchy of the mu-calculus (the mu-calculus hierarchy) with the expressiveness of the bisimulation-invariant fragment of levels of the monadic quantifiers alternation-depth hierarchy (the monadic hierarchy). From J. van Benthem's (1976) results, we know already that the fixpoint free fragment of the mu-calculus (i.e. polymodal logic) is as expressive as the bisimulation-invariant fragment of monadic /spl Sigma//sub 0/ (i.e. first-order logic). We show that the /spl nu/-level of the mu-calculus hierarchy is as expressive as the bisimulation-invariant fragment of monadic /spl Sigma//sub 1/ and that the /spl nu//spl mu/-level of the mu-calculus hierarchy is as expressive as the bisimulation-invariant fragment of monadic /spl Sigma//sub 2/, and we show that no other level /spl Sigma//sub k/ (for k>2) of the monadic hierarchy can be related similarly with any other level of the mu-calculus hierarchy. The possible inclusion of all the mu-calculus in some level /spl Sigma//sub k/ of the monadic hierarchy, for some k>2, is also discussed.

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 /spl Lambda/ 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 /spl lambda/. This result generalizes Muller and Schupp's simulation theorem for alternating automata on the binary tree.