The Horn mu-calculus
Witold Charatonik, David McAllester, Damian Niwiński, Andreas Podelski, Igor Walukiewicz · 2002
The Horn /spl mu/-calculus is a logic programming language allowing arbitrary nesting of least and greatest fixed points. The Horn /spl mu/-programs can naturally express safety and liveness properties for reactive systems. We extend the set-based analysis of classical logic programs by mapping arbitrary /spl mu/-programs into "uniform" /spl mu/-programs. Our two main results are that uniform /spl mu/-programs express regular sets of trees and that emptiness for uniform /spl mu/-programs is EXPTIME-complete. Hence we have a nontrivial decidable relaxation for the Horn /spl 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).