The Horn mu-calculus
- 27 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10436871,p. 58-69
- https://doi.org/10.1109/lics.1998.705643
Abstract
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).Keywords
This publication has 18 references indexed in Scilit:
- A polynomial-time algorithm for deciding equivalence of normed context-free processesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Actions speak louder than words: proving bisimilarity for context-free processesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Logic programs as types for logic programsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and SafraTheoretical Computer Science, 1995
- Deciding Emptiness for Stack Automata on Infinite TreesInformation and Computation, 1994
- Infinite games played on finite graphsAnnals of Pure and Applied Logic, 1993
- A finite presentation theorem for approximating logic programsPublished by Association for Computing Machinery (ACM) ,1990
- Regular expressions for infinite trees and a standard form of automataPublished by Springer Nature ,1985
- The theory of ends, pushdown automata, and second-order logicTheoretical Computer Science, 1985
- Flow analysis and optimization of LISP-like structuresPublished by Association for Computing Machinery (ACM) ,1979