The Horn Mu-calculus

The Horn $\mu$-calculus is a logic programming language allowing arbitrary nesting of least and greatest fixed points. The Horn $\mu$-programs can naturally expresses safety and liveness properties for reactive systems. We extend the set-based analysis of classical logic programs by mapping arbitrary $\mu$-programs into ``uniform'' $\mu$-programs. Our two main results are that uniform $\mu$-programs express regular sets of trees and that emptiness for uniform $\mu$-programs is EXPTIME-complete. Hence we have a nontrivial decidable relaxation for the Horn $\mu$-calculus. In a different reading, the results express a kind of robustness of the notion of regularity: alternating Rabin tree automata preserve the same expressiveness and algorithmic complexity if we extend them with pushdown transition rules (in the same way B\"uchi extended word automata to canonical systems)