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 Buchi extended word automata to canonical systems).