# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### The Horn Mu-calculus

##### MPS-Authors

##### Locator

There are no locators available

##### Fulltext (public)

There are no public fulltexts available

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Charatonik, W., McAllester, D., Niwinski, D., Podelski, A., & Walukiewicz, I. (1998).
The Horn Mu-calculus. In V. Pratt (*Proceedings of the
13th Annual IEEE Symposium on Logic in Computer Science (LICS-98)* (pp. 58-69). Los Alamitos, USA: IEEE.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-389F-5

##### 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 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).