The Horn mu-calculus

The Horn μ-calculus is a logic programming language allowing arbitrary nesting of least and greatest fixed points. The Horn μ-programs can naturally express safety and liveness properties for reactive systems. We extend the set-based analysis of classical logic programs by mapping arbitrary μ-programs into “uniform” μ-programs. Our two main results are that uniform μ-programs express regular sets of trees and that emptiness for uniform μ-programs is EXPTIME-complete. Hence we have a nontrivial decidable relaxation for the Horn μ-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)