On the Expressive Power of Monadic Least Fixed Point Logic

Monadic least fixed point logic MLFP is a natural logic whose expressiveness lies between that of first-order logic FO and monadic second-order logic MSO. In this paper we take a closer look at the expressive power of MLFP. Our results are (1) MLFP can describe graph properties beyond any fixed level of the monadic secondorder quantifier alternation hierarchy. (2) On strings with built-in addition, MLFP can describe at least all languages that belong to the linear time complexity class DLIN. (3) Settling the question whether addition-invariant MLFP ? = addition-invariant MSO on finite strings or, equivalently, settling the question whether MLFP ? = MSO on finite strings with addition would solve open problems in complexity theory: “=” would imply that PH = PTIME whereas “=” would imply that DLIN = LINH. Apart from this we give a self-contained proof of the previously known result that MLFP is strictly less expressive than MSO on the class of finite graphs. Journal versi...

• Type: Conference
• Year: 2004
• Where: ICALP
• Authors: Nicole Schweikardt
• Keywords: ICALP 2004, Point Logic Mlfp, Second-order Logic Mso, Theoretical Computer Science, finite Strings