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

Authors: 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}
  }