## Paper: The Horn Mu-calculus (at LICS 1998)

**Witold Charatonik David A. McAllester Damian Niwinski Andreas Podelski Igor Walukiewicz**

### Abstract

The Horn Mu-calculus is a logic programming language allowing arbitrary nesting of least and greatest fixed points. The Horn 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 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)

### BibTeX

@InProceedings{CharatonikMcAlleste-TheHornMucalculus, author = {Witold Charatonik and David A. McAllester and Damian Niwinski and Andreas Podelski and Igor Walukiewicz}, title = {The Horn Mu-calculus}, booktitle = {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)}, year = {1998}, month = {June}, pages = {58--69}, location = {Indianapolis, IN, USA}, publisher = {IEEE Computer Society Press} }