English

# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### The Horn Mu-calculus

##### MPS-Authors
/persons/resource/persons44232

Charatonik,  Witold
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45131

Niwinski,  Damian
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45201

Podelski,  Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

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